LCS Publication Details
Publication Title: Selecting Refining and Evaluating Properties for Program Analysis
Publication Author: Dodoo, Nii
Additional Authors: Lee Lin, Michael D. Ernst
LCS Document Number: MIT-LCS-TR-914
Publication Date: 7-21-2003
LCS Group: Program Analysis
Additional URL:
This research proposes and evaluates techniques for selecting predicates for conditional program properties—that is, implications such as p ) q whose consequent must be true whenever the predicate is true. Conditional properties are prevalent in recursive data structures, which behave differently in their base and recursive cases, in programs that contain branches, in programs that fail only on some inputs, and in many other situations. The experimental context of the research is dynamic detection of likely program invariants, but the ideas are applicable to other domains. Trying every possible predicate for conditional properties is computationally infeasible and yields too many undesirable properties. This paper compares four policies for selecting predicates: procedure return analysis, code conditionals, clustering, and random selection. It also shows how to improve predicates via iterated analysis. An experimental evaluation demonstrates that the techniques improve performance on two tasks: statically proving the absence of run-time errors with a theorem-prover, and separating faulty from correct executions of erroneous programs.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.