Download: PDF, Daikon implementation.
“Dynamically Discovering Likely Program Invariants”
by Michael D. Ernst.
Ph.D. dissertation, University of
Washington Department of Computer Science and Engineering, (Seattle,
Washington), Aug. 2000.
A summary appeared as
“Summary of Dynamically discovering likely program
invariants”
by Michael D. Ernst.
In ICSM 2001: Proceedings of the International Conference on Software
Maintenance, (Florence, Italy), Nov. 2001, pp. 540-544.
A short research plan appeared as
“Research summary for dynamic detection of program invariants”
by Michael D. Ernst.
In ICSE '99: Proceedings of the 21st International Conference on
Software Engineering, (Los Angeles, CA, USA), May 1999, pp.
718-719.
A longer research plan appeared as
“Research summary for dynamic detection of program invariants”
by Michael D. Ernst.
In ICSE '99 Doctoral Workshop, (Los Angeles, CA, USA), May 1999.
Expanded version of two-page summary in ICSE '99 proceedings, distributed
at workshop.
This dissertation introduces dynamic detection of program invariants, presents techniques for detecting such invariants from traces, assesses the techniques' efficacy, and points the way for future research.
Invariants are valuable in many aspects of program development, including design, coding, verification, testing, optimization, and maintenance. They also enhance programmers' understanding of data structures, algorithms, and program operation. Unfortunately, explicit invariants are usually absent from programs, depriving programmers and automated tools of their benefits.
This dissertation shows how invariants can be dynamically detected from program traces that capture variable values at program points of interest. The user runs the target program over a test suite to create the traces, and an invariant detector determines which properties and relationships hold over both explicit variables and other expressions. Properties that hold over the traces and also satisfy other tests, such as being statistically justified, not being over unrelated variables, and not being implied by other reported invariants, are reported as likely invariants. Like other dynamic techniques such as testing, the quality of the output depends in part on the comprehensiveness of the test suite. If the test suite is inadequate, then the output indicates how, permitting its improvement. Dynamic analysis complements static techniques, which can be made sound but for which certain program constructs remain beyond the state of the art.
Experiments demonstrate a number of positive qualities of dynamic invariant detection and of a prototype implementation, Daikon. Invariant detection is accurate — it rediscovers formal specifications — and useful — it assists programmers in programming tasks. It runs quickly and produces output of modest size. Test suites found in practice tend to be adequate for dynamic invariant detection.
Download: PDF, Daikon implementation.
BibTeX entry:
@phdthesis{Ernst2000:PhD,
author = {Michael D. Ernst},
title = {Dynamically Discovering Likely Program Invariants},
school = {University of Washington Department of Computer Science and
Engineering},
type = {{Ph.D.}},
address = {Seattle, Washington},
month = aug,
year = {2000}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.