| Abstract | 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 \le x \le b$), linear relationships ($y = ax+b$), ordering ($x \le y$), functions from a library ($x = \mathrmfn(y)$), containment ($x \in y$), sortedness ($x \mathrmis \mathrmsorted$), and many more. Users can extend Daikon to check for additional invariants. \par 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. \par 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. \par Daikon is freely available in source and binary form, along with extensive documentation, at \urlhttps://plse.cs.washington.edu/daikon/. |
