Dynamically discovering likely program invariants to support program evolution
Top Cited Papers
- 1 February 2001
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 27 (2) , 99-123
- https://doi.org/10.1109/32.908957
Abstract
Explicitly stated program invariants can help programmers by identifying program properties that must be preserved when modifying code. In practice, however, these invariants are usually implicit. An alternative to expecting programmers to fully annotate code with invariants is to automatically infer likely invariants from the program itself. This research focuses on dynamic techniques for discovering invariants from execution traces. This article reports three results. First, it describes techniques for dynamically discovering invariants, along with an implementation, named Daikon, that embodies these techniques. Second, it reports on the application of Daikon to two sets of target programs. In programs from Gries's work (1981) on program derivation, the system rediscovered predefined invariants. In a C program lacking explicit invariants, the system discovered invariants that assisted a software evolution task. These experiments demonstrate that, at least for small programs, invariant inference is both accurate and useful. Third, it analyzes scalability issues, such as invariant detection runtime and accuracy, as functions of test suites and program points instrumented.Keywords
This publication has 59 references indexed in Scilit:
- Strongest Postcondition Semantics as the Formal Basis for Reverse EngineeringPublished by Springer Nature ,2007
- Summary of dynamically discovering likely program invariantsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A specification matching based approach to reverse engineeringPublished by Association for Computing Machinery (ACM) ,1999
- Parametric shape analysis via 3-valued logicPublished by Association for Computing Machinery (ACM) ,1999
- An empirical analysis of instruction repetitionPublished by Association for Computing Machinery (ACM) ,1998
- Static detection of dynamic memory errorsPublished by Association for Computing Machinery (ACM) ,1996
- Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in CPublished by Association for Computing Machinery (ACM) ,1996
- Inferring program specifications in polynomial-timePublished by Springer Nature ,1996
- The Science of ProgrammingPublished by Springer Nature ,1981
- Implementation of an array bound checkerPublished by Association for Computing Machinery (ACM) ,1977