Research Projects
Dynamic Invariant Detection for Program Understanding and Reliability MIT2001-01 Start date: 07/2001	Michael Ernst MIT LCS Tadashi Araragi NTT
Project summary

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

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.

The principal investigators

• Michael Ernst (email)
• Tadashi Araragi (email)

Publications

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

Proposals:

• proposal 2001: 
• proposal 2001: 

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

• project report: 
• presentation slides: 

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

• project report: 
• presentation slides: 

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

• project report: 
• presentation slides: 

• The Daikon Invariant Detector