[ Home | FAQ | Download | Documentation | Publications | Mailing lists ]

# Daikon-related invariant detection publications

This page lists publications related to the technique of invariant detection and to the Daikon invariant detector tool that implements it. The page is separated into four parts:

Invariant detection technique
  This section describes the technique of invariant detection and the implementation of the Daikon invariant detector.
Methodology using invariant detection
  This section lists publications whose research methodology depends on running the Daikon tool. The research uses Daikon's invariant detection as one step of its technique. (Research that uses other invariant detection tools is not listed here.)
Daikon as test subject
  This section lists publications that use the Daikon invariant detector as a test subject. For instance, Daikon has been used as a subject when evaluating regression testing tools, since it has both a version control repository and a test suite.
Other invariant detection tools
  This section briefly lists some other invariant detection tools (besides Daikon).

The lists of papers and tools are undoubtedly incomplete. If you know of other work that should be listed here, or discover an error, please send mail to mernst@cs.washington.edu. Thanks.

# Invariant detection technique

BODY-INVARIANTDETECTION

# Methodology using invariant detection

BODY-METHODOLOGYUSINGDAIKON

# Daikon as test subject

BODY-DAIKONTESTSUBJECT

# Other invariant detection tools

Other researchers and commercializers have adopted the idea of invariant detection, extending the technique and building new tools. This section is a selected list of some of those industrial and academic efforts. This is a partial list; please let me know of any others that are not industrial or academic secrets.

## Industrial invariant detection implementations

Sun Microsystems
  IODINE is an invariant detector for hardware designs, built by Sudheendra Hangal (who is also responsible for the DIDUCE invariant detector, described below) and colleagues. The goal is to execute test vectors or real loads on a simulator in order to learn emergent properties of the design. See the paper "IODINE: A tool to automatically infer dynamic invariants for hardware designs" in the Design Automation Conference, DAC 2005.
Microsoft
  Trishul Chilimbi is building a high-performance dynamic invariant detector that operates at garbage collection (GC) time. Since all of memory must be scanned then anyway, the invariant detector imposes relatively little additional cost for its memory accesses. The invariant detector's grammar includes run-time types (for checking what types a collection contains), immutability, and cycles in the object reference graph (the heap).
Agitar
  Agitar's product, Agitator, was inspired by Daikon. Agitar performs dynamic invariant detection in order to inform users about tests, and to improve those tests. The results are called "observations", they include equality (x = y), range (-10 <= x <= 10), non-null (x != null), equality (.equals), and properties gleaned from the user's source code. Agitar won the Wall Street Journal's 2005 Software Technology Innovation Award. Regarding Agitar's work and its connection to Daikon, see the ISSTA 2006 paper ``From Daikon to Agitator: Lessons and Challenges in Building a Commercial Tool for Developer Testing'', by Marat Boshernitsan, Roongko Doong, and Alberto Savoia.
Microsoft
  The Axiom Meister tool (built by Wolfram Schulte and colleagues) infers specifications from code by performing exhaustive symbolic execution (similar to model checking). The tool generalizes over the results of user-specified observer methods. The output can be used for test generation and program verification.
Rebert Bosch RTC and University of Maryland
  The Magnum Opus tool generates invariants from Simulink models, then other tools generate test cases to expand the test suite. See the paper "Automatic Requirement Extraction from Test Cases" (appears in RV 2010).

## Academic invariant detection implementations

Stanford
  The DIDUCE tool (DIDUCE stands for "Dynamic Invariant Detection Union Checking Engine") checks one invariant: the bitwise or of the values of a variable. DIDUCE performs dynamic invariant detection online -- while the target program is running. DIDUCE is described in the paper "Tracking down software bugs using automatic anomaly detection", by Sudheendra Hangal and Monica S. Lam (appears in ICSE 2002).
Wisconsin and Microsoft
  The paper "Mining specifications" by Glenn Ammons, Rastislav Bodík, and James R. Larus (appears in POPL 2002) describes a system for inferring temporal specifications, such as "method `open` must be called before method `close`". The sequence of observed method calls is fed to a machine learner in order to obtain a grammar of permitted call sequences.
Stanford
  The paper "Automatic extraction of object-oriented component interfaces" by John Whaley, Michael C. Martin, and Monica S Lam (appears in ISSTA 2002) has the same goal as that of the "Mining specifications" paper: determining the legal sequences of procedure calls (in the paper, called "interfaces"). The paper proposes a combination of static and dynamic methods.
Berkeley
  Ben Liblit's statistical debugging project, described in a variety of publications, aims to permit collecting a small amount of information from a large number of executions in the field (some faulty, some not) in order to determine which properties of an execution are most relevant to errors. Its mechanism for collecting the information is a type of invariant detection.
Brown
  The Carrot dynamic invariant detection system is described in the paper "Automated fault localization using potential invariants", by Brock Pytlik, Manos Renieris, Shriram Krishnamurthi, and Steven P. Reiss (appears in AADEBUG 2003). It is built partly upon the Daikon infrastructure, but investigates other implementation strategies.
Colorado
  Two papers by Johannes Henkel and Amer Diwan -- "Discovering algebraic specifications from Java classes" (appears in ECOOP 2003) and "A tool for writing and debugging algebraic specifications" (appears in ICSE 2004) -- describe an application of dynamic invariant detection to algebraic specifications. Algebraic specifications are equations between terms, such as "pop(push(s,i).state).retval = i" and "pop(push(s,i).state).state = s".
Virginia and Microsoft
  David Evans and Jinlin Yang are building Terracotta, a dynamic analysis tool for automatically inferring temporal properties. It takes the program's execution traces as input and outputs a set of likely temporal properties. It is reported in "Automatically Inferring Temporal Properties for Program Evolution" (appears in ISSRE 2004). Jinlin Yang applied the techniques to the Windows Kernel while at Microsoft.
SUNY at Stony Brook
  "Type discovery" can be thought of as dynamic invariant detection for ownership (locks held when a field is accessed). It is a dynamic analysis that observes run-time types and forms hypotheses based on those observations. Two papers describe the technique and the analyses that can be built upon it: "Type discovery for Parameterized Race-Free Java" (appears at VMCAI 2005) and "Automated type-based analysis of data races and atomicity" (appears at PPOPP 2005).
Purdue
  C-DIDUCE is a re-implementation, for C, of Stanford's DIDUCE tool (which works on Java). DIDUCE is described in the paper "Artemis: Practical runtime monitoring of applications for execution anomalies", by Long Fei and Samuel P. Midkiff (appears in PLDI 2006).

[ Home | FAQ | Download | Documentation | Publications | Mailing lists ]