VSL Publications

Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles

Cite
Stephen F. Siegel and George S. Avrunin, Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles. IEEE Transactions on Software Engineering 28 (2002), no. 2, 115–128
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.
Downloads
  1. Paper on publisher's web site
  2. cycles_tse_2002.pdf (preprint)
BibTeX 
@article{siegel-avrunin:2002:improving_precision-tse,
	Author = {Stephen F. Siegel and George S. Avrunin},
	Journal = {IEEE Transactions on Software Engineering},
	Number = {2},
	Pages = {115--128},
	Title = {Improving the Precision of {INCA} by Eliminating Solutions with Spurious Cycles},
	Volume = {28},
	Year = {2002}}
VSL | Publications