title: "The Daikon system for dynamic detection of likely invariants"
authors: Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, Chen Xiao
venue: Science of Computer Programming
year: 2007
links:
- Website
tweet: Daikon finds likely program invariants, which can improve documentation, tests, and code analyses
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 != 0), being in a
range (a <= x <= b), linear relationships (y = ax+b), ordering (x <=
y), functions from a library (x = fn(y)), containment (x E y),
sortedness (x is sorted), and many more. Users can extend Daikon to
check for additional invariants.
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.
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.
Daikon is freely available in source and binary form, along with
extensive documentation, at http://pag.csail.mit.edu/daikon/.
bibtex: >
@article{ErnstDaikonSCP2007,
author = {Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and Chen Xiao},
title = {The {Daikon} system for dynamic detection of likely invariants},
journal = {Science of Computer Programming},
volume = {69},
number = {1--3},
pages = {35--45},
month = Dec,
year = {2007}
}