Quickly detecting relevant program invariants

Download: PDF, slides (PDF), slides (PowerPoint), Daikon implementation.

“Quickly detecting relevant program invariants” by Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, (Limerick, Ireland), June 2000, pp. 449-458.
A previous version appeared as University of Washington Department of Computer Science and Engineering technical report UW-CSE-99-11-01, (Seattle, WA), November 15, 1999.

Abstract

Explicitly stated program invariants can help programmers by characterizing certain aspects of program execution and identifying program properties that must be preserved when modifying code. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically detect invariants from program traces by looking for patterns in and relationships among variable values. A prototype implementation, Daikon, accurately recovered invariants from formally-specified programs, and the invariants it detected in other programs assisted programmers in a software evolution task. However, Daikon suffered from reporting too many invariants, many of which were not useful, and also failed to report some desired invariants.

This paper presents, and gives experimental evidence of the efficacy of, four approaches for increasing the relevance of invariants reported by a dynamic invariant detector. One of them — exploiting unused polymorphism — adds desired invariants to the output. The other three — suppressing implied invariants, limiting which variables are compared to one another, and ignoring unchanged values — eliminate undesired invariants from the output and also improve runtime by reducing the work done by the invariant detector.

Download: PDF, slides (PDF), slides (PowerPoint), Daikon implementation.

BibTeX entry:

@inproceedings{ErnstCGN2000:Relevance,
   author = {Michael D. Ernst and Adam Czeisler and William G. Griswold
	and David Notkin},
   title = {Quickly detecting relevant program invariants},
   booktitle = {ICSE 2000, Proceedings of the 22nd International
	Conference on Software Engineering},
   pages = {449--458},
   address = {Limerick, Ireland},
   month = jun,
   year = {2000}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.