Download: PDF, PostScript.
“Selecting predicates for implications in program analysis” by Nii Dodoo, Alan Donovan, Lee Lin, and Michael D. Ernst. March 16, 2002. Draft. https://pag.csail.mit.edu/~mernst/pubs/invariants-implications.ps.
This research proposes and evaluates techniques for selecting predicates for conditional program properties — that is, implications such as p ⇒ q whose consequent is true only when the predicate is true. Conditional properties are prevalent in recursive data structures, which behave differently in their base and recursive cases, and in many other situations. The experimental context of the research is dynamic detection of likely program invariants, but the ideas should also be applicable to other domains.
It is computationally infeasible to try every possible predicate for conditional properties, so we compare procedure return analysis, static analysis, clustering, random selection, and context-sensitive analysis for selecting predicates.
Even a simple static analysis is fairly effective, presumably because many of the important properties of a program are tested or expressed by programmers. However, important properties are implicit in the program's code or execution. We give examples of important properties discovered by each of the other analyses. We experimentally evaluate the techniques on two tasks: statically proving the absence of run-time errors with a theorem-prover, and detecting errors by separating erroneous from correct executions. We show that the techniques improve performance on both tasks, and we evaluate their costs.
Download: PDF, PostScript.
BibTeX entry:
@misc{DodooDLE02,
author = {Nii Dodoo and Alan Donovan and Lee Lin and Michael D. Ernst},
title = {Selecting predicates for implications in program analysis},
month = {March~16,},
year = {2002},
note = {Draft.
\url{https://pag.csail.mit.edu/~mernst/pubs/invariants-implications.ps}}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.