A relational framework for bounded program verification

Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009.Cataloged from PDF version of thesis.Includes bibliographical references (p. 131-138).All software verification techniques, from theorem proving to testing, share the common goal of establishing a program's correctness with both (1) a high degree of confidence and (2) a low cost to the user, two criteria in tension with one another. Theorem proving offers the benefit of high confidence, but requires significant expertise and effort from the user. Testing, on the other hand, can be performed for little cost, but low-cost testing does not yield high confidence in a program's correctness. Although many static analyses can quickly and with high confidence check a program's conformance to a specification, they achieve these goals by sacrificing the expressiveness of the specification. To date, static analyses have been largely limited to the detection of shallow properties that apply to a very large class of programs, such as absence of array-bound errors and conformance to API usage conventions. Few static analyses are capable of checking strong specifications, specifications whose satisfaction relies upon the program's precise behavior. This thesis presents a new program-analysis framework that allows a procedure in an object-oriented language to be automatically checked, with high confidence, against a strong specification of its behavior. The framework is based on an intermediate relational representation of code and an analysis that examines all executions of a procedure up to a bound on the size of the heap and the number of loop unrollings. If a counterexample is detected within the bound, it is reported to the user as a trace of the procedure, though defects outside the bound will be missed.(cont.) Unlike testing, many static analyses are not equipped with coverage metrics to detect which program behaviors the analysis failed to exercise. Our framework, in contrast, includes such a metric. When no counterexamples are found, the metric can report how thoroughly the code was covered. This information can, in turn, help the user change the bound on the analysis or strengthen the specification to make subsequent analyses more comprehensive.by Gregory D. Dennis.Ph.D