Research Projects NTT-MIT Research Collaboration: a partnership in the future of communication and computation

Dynamic Invariant Detection for Program Understanding and Reliability


Start date: 07/2001

Michael Ernst

Tadashi Araragi

Project summary

This project investigates the possibility of automatically determining, from program executions, temporal invariants that are true of the program.

Project description


Temporal invariants relate properties or facts at multiple points in time. As a simple example, consider a traffic signal. A temporal invariant might state, "if a car arrives at the intersection, then the light will eventually turn green." By contrast, a static or data invariant might state, "no two directions show green simultaneously." Temporal invariants are typically written in a temporal logic such as LTL. They relate events with operators such as "eventually" or "always". Temporal invariants are useful for a variety of tasks such as program understanding, making modifications without introducing errors, proving correctness, and more. This research automatically determines which temporal invariants are true of a program by running the program and examining its executions. The results of the analysis are not guaranteed to hold in every possible situation, but the information tends to be useful nonetheless. This projects aims to both advance the state of the art in temporal invariant detection and to assist NTT in evaluating the technology and putting it to productive use.

Demos, movies and other examples

The principal investigators

Presentations and posters


Jeremy W. Nimmer and Michael D. Ernst, "Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java'', Proceedings of RV'01, First Workshop on Runtime Verification, July 23, 2001, Paris, France.

Yoshio Kataoka, Michael D. Ernst, William G. Griswold, and David Notkin, "Automated Support for Program Refactoring using Invariants'', Proceedings of ICSM'01, International Conference on Software Maintenance, Florence, Italy, November 6-10, 2001.

Michael D. Ernst, "Dynamically Detecting Likely Program Invariants'', PhD dissertation, University of Washington, Department of Computer Science and Engineering, August, 2000.

Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin, "Quickly Detecting Relevant Program Invariants'', Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 7-9, 2000, pp. 449-458.

Michael D. Ernst, Yoshio Kataoka, William G. Griswold, and David Notkin, "Dynamically Discovering Pointer-Based Program Invariants'', University of Washington technical report UW-CSE-99-11-02, November 16, 1999.

Proposals and progress reports


NTT Bi-Annual Progress Report, July to December 2001:

NTT Bi-Annual Progress Report, January to June 2002:

NTT Bi-Annual Progress Report, July to December 2002:

For more information