A relational framework for bounded program verification
Gregory D. Dennis · DSpace@MIT (Massachusetts Institute of Technology) · 2009
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.