The Daikon system for dynamic detection of likely invariants
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | The Daikon system for dynamic detection of likely invariants |
| Publication Type | Journal Article |
| Year of Publication | 2007 |
| Authors | Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C |
| Volume | 69 |
| Pagination | 35–45 |
| Date or Month Published | December |
| Abstract | <p>Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. An invariant is a property that holds at a certain point or points in a program; these are often used in assert statements, documentation, and formal specifications. Examples include being constant ($x = a$), non-zero ($x \ne 0$), being in a range ($a łe x łe b$), linear relationships ($y = ax+b$), ordering ($x łe y$), functions from a library ($x = \mathrm{fn}(y)$), containment ($x \in y$), sortedness ($x \mathrm{is} \mathrm{sorted}$), and many more. Users can extend Daikon to check for additional invariants. </p> <p> Dynamic invariant detection runs a program, observes the values that the program computes, and then reports properties that were true over the observed executions. Dynamic invariant detection is a machine learning technique that can be applied to arbitrary data. Daikon can detect invariants in C, C + +, Java, and Perl programs, and in record-structured data sources; it is easy to extend Daikon to other applications. </p> <p> Invariants can be useful in program understanding and a host of other applications. Daikon's output has been used for generating test cases, predicting incompatibilities in component integration, automating theorem-proving, repairing inconsistent data structures, and checking the validity of data streams, among other tasks. </p> <p> Daikon is freely available in source and binary form, along with extensive documentation, at <a href='http://pag.csail.mit.edu/daikon/'>http://pag.csail.mit.edu/daikon/</a>.</p> |
| Downloads | Daikon implementation PDF |
| Citation Key | ErnstPGMPTX2007 |
Last changed Mon, 2013-06-03 10:27

cs.