Download: PDF.
“Selecting, refining, and evaluating predicates for program
analysis”
by Nii Dodoo,
Lee Lin,
and
Michael D. Ernst.
MIT Laboratory for Computer Science technical report MIT-LCS-TR-914, (Cambridge, MA), July 21, 2003.
A previous version appeared as
“Selecting predicates for implications in program analysis”
by Nii Dodoo, Alan Donovan,
Lee Lin,
and
Michael D. Ernst.
March 16, 2002.
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.
Download: PDF.
BibTeX entry:
@techreport{DodooLE2003:TR,
author = {Nii Dodoo and Lee Lin and Michael D. Ernst},
title = {Selecting, refining, and evaluating predicates for program
analysis},
institution = {MIT Laboratory for Computer Science},
number = {MIT-LCS-TR-914},
address = {Cambridge, MA},
month = {July~21,},
year = {2003}
}