Download: PostScript.
“Selecting Predicates for Conditional Invariant Detection Using Cluster Analysis” by Nii Dodoo. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), Sep. 2002.
This thesis proposes a new technique for selecting predicates for conditional program invariants — that is, implications of the form “p ⇒ q” whose consequent is true only when the predicate is true. Conditional invariants are prevalent in recursive data structures, which behave differently in the base and recursive cases, and in many other situations.
We argue that inferring conditional invariants in programs can be reduced to the task of selecting suitable predicates from which to infer these conditional invariants. It is computationally infeasible to try every possible predicate for conditional properties, and therefore it is necessary to limit possible predicates to only those likely to give good results. This thesis describes the use of cluster analysis to select suitable predicates for conditional invariant detection from program execution traces. The primary thesis is: if “natural” clusters exist in the values of program execution traces, then invariants over these clusters should serve as good predicates for conditional invariant detection.
The conditional invariants inferred by cluster analysis can be useful to programmers for a variety of tasks. In two experiments, we show that they are useful in a static verification task and can help programmers identify bugs in software programs, and we compare the results with other methods for finding conditional invariants.
Download: PostScript.
BibTeX entry:
@mastersthesis{Dodoo02:thesis,
author = {Nii Dodoo},
title = {Selecting Predicates for Conditional Invariant Detection Using
Cluster Analysis},
school = {MIT Department of Electrical Engineering and Computer Science},
address = {Cambridge, MA},
month = sep,
year = {2002}
}