TitleAutomatic generation of program specifications
Publication TypeConference Paper
Year of Publication2002
AuthorsNimmer JW, Ernst MD
Conference NameISSTA 2002, Proceedings of the 2002 International Symposium on Software Testing and Analysis
Pagination232–242
Date or Month PublishedJuly
Conference LocationRome, Italy
AbstractProducing 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 precision, a measure of soundness, and on recall, a measure of completeness. \par 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.
Downloadshttps://homes.cs.washington.edu/~mernst/pubs/generate-specs-issta2002.pdf PDF
Citation KeyNimmerE02:ISSTA