The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (2002 vol.28)
pp: 115-128
ABSTRACT
<p>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.</p>
INDEX TERMS
INCA, finite-state verification, cycles, integer programming.
CITATION
S.F. Siegel, G.S. Avrunin, "Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles", IEEE Transactions on Software Engineering, vol.28, no. 2, pp. 115-128, February 2002, doi:10.1109/32.988494
342 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool