Stephen F. Siegel and George S. Avrunin, Improving the precision
of INCA by preventing spurious cycles. In Mary Jean Harrold, editor,
Proceedings of the ACM SIGSOFT International Symposium on
Software Testing and Analysis (ISSTA 2000), pages
191-200, Portland, OR, August 2000. ACM Press.
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.
@InProceedings{siegel-avrunin:2000:improving_precision-issta,
author = {Stephen F. Siegel and George S. Avrunin},
title = {Improving the Precision of {INCA} by Preventing Spurious Cycles},
crossref = {issta2000},
pages = {191--200}
}
@Proceedings{issta2000,
booktitle = {Proceedings of the ACM SIGSOFT 2000 International Symposium on Software Testing and Analysis, Portland, OR, USA, August 21--24, 2000},
title = {Proceedings of the ACM SIGSOFT 2000 International Symposium on Software Testing and Analysis, Portland, OR, USA, August 21--24, 2000},
editor = {Mary Jean Harrold},
publisher = {ACM Press},
year = 2000
}
