Abstract. The Inequality Necessary Condition Analyzer (INCA) is a finite-state verification tool that has been able to check properties of some very large concurrent systems. INCA checks a property of a concurrent system by generating a system of inequalities that must have integer solutions if the property can be violated. There may, however, be integer solutions to the inequalities that do not correspond to an execution violating the property. INCA thus accepts the possibility of an inconclusive result in exchange for greater tractability. We describe here a method for eliminating one of the two main sources of these inconclusive results.This paper appeared in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA '00), Portland, OR, August 2000, M. J. Harrold, editor, 191-200.
You may download the paper in one of the following formats: