A new structural coverage criterion for dynamic detection of program invariants

“A new structural coverage criterion for dynamic detection of program invariants” by Neelam Gupta and Zachary V. Heidepriem. In ASE 2003: Proceedings of the 18th Annual International Conference on Automated Software Engineering, (Montreal, Canada), Oct. 2003, pp. 49-58.
A previous version appeared as “Generating test data for dynamically discovering likely program invariants” by Neelam Gupta. In WODA 2003: Workshop on Dynamic Analysis, (Portland, OR, USA), May 2003, pp. 21-24.

Abstract

Dynamic detection of program invariants is emerging as an important research area with many challenging problems. Generating suitable test cases that support accurate detection of program invariants is crucial to the dynamic approach for invariant detection. In this paper, we propose a new structural coverage criterion called Invariant-coverage criterion for dynamic detection of program invariants. We also show how the invariant-coverage criterion can be used to improve the accuracy of dynamically detected invariants. We first used the Daikon tool to report likely program invariants using the branch coverage and all definition-use pair coverage test suites for several programs. We then generated invariant-coverage suites for these likely invariants. When Daikon was run with the invariant-coverage suites, several spurious invariants reported earlier by the branch coverage and definition-use pair coverage test suites were removed from the reported invariants. Our approach also produced more meaningful invariants than randomly generated test suites.

BibTeX entry:

@inproceedings{GuptaH2003,
   author = {Neelam Gupta and Zachary V. Heidepriem},
   title = {A new structural coverage criterion for dynamic detection of
	program invariants},
   booktitle = {ASE 2003: Proceedings of the 18th Annual International
	Conference on Automated Software Engineering},
   pages = {49--58},
   address = {Montreal, Canada},
   month = oct,
   year = {2003}
}

Back to Publications whose methodology uses invariant detection.