Automatic generation of program specifications

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

“Automatic generation of program specifications” by Jeremy W. Nimmer and Michael D. Ernst. In ISSTA 2002, Proceedings of the 2002 International Symposium on Software Testing and Analysis, (Rome, Italy), July 2002, pp. 232-242.
A previous version appeared as “Automatic generation and checking of program specifications” by Jeremy W. Nimmer and Michael D. Ernst. MIT Laboratory for Computer Science technical report 823, (Cambridge, MA), August 10, 2001. Revised February 1, 2002.

Abstract

Producing specifications by dynamic (runtime) analysis of program executions is potentially unsound, because the analyzed executions may not fully characterize all possible executions of the program. In practice, how accurate are the results of a dynamic analysis? This paper describes the results of an investigation into this question, determining how much specifications generalized from program runs must be changed in order to be verified by a static checker. Surprisingly, small test suites captured nearly all program behavior required by a specific type of static checking; the static checker guaranteed that the implementations satisfy the generated specifications, and ensured the absence of runtime exceptions. Measured against this verification task, the generated specifications scored over 90% on precision, a measure of soundness, and on recall, a measure of completeness.

This is a positive result for testing, because it suggests that dynamic analyses can capture all semantic information of interest for certain applications. The experimental results demonstrate that a specific technique, dynamic invariant detection, is effective at generating consistent, sufficient specifications for use by a static checker. Finally, the research shows that combining static and dynamic analyses over program specifications has benefits for users of each technique, guaranteeing soundness of the dynamic analysis and lessening the annotation burden for users of the static analysis.

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

BibTeX entry:

@inproceedings{NimmerE02:ISSTA,
   author = {Jeremy W. Nimmer and Michael D. Ernst},
   title = {Automatic generation of program specifications},
   booktitle = {ISSTA 2002, Proceedings of the 2002 International
	Symposium on Software Testing and Analysis},
   pages = {232--242},
   address = {Rome, Italy},
   month = jul,
   year = {2002}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.