Program Verification

Program verification aims to use formal proofs to demonstrate that programs behave according to formal specifications. Proving programs correct or even partially correct has been a hot topic for decades. My masters thesis at CWRU under George Ernst was in the area of program verification. I abandoned this work when I came to CMU.

Back to Bibliography by Subject

Dannenberg and Ernst, “Formal Program Verification Using Symbolic Execution,” IEEE Transactions on Software Engineering, SE-8, (Jan 1982), pp. 43-52.

A good summary of my masters work at CWRU. The basic idea is to use symbolic execution and some Hoare-style proof rules to generate verification conditions.
ABSTRACT: Symbolic execution provides a mechanism for formally proving programs correct. A notation is introduced which allows a concise presentation of rules of inference based on symbolic execution. Using this notation, rules of inference are developed to handle a number of language features, including loops and procedures with multiple exits. An attribute grammar is used to formally describe symbolic expression evaluation, and the treatment of function calls with side effects is shown to be straightforward. Because symbolic execution is related to program interpretation, it is an easy-to-comprehend, yet powerful technique. The rules of inference are useful in expressing the semantics of a language and form the basis of a mechanical verification condition generator.

[Adobe (PDF) Version]

Dannenberg, “An Extended Verification Condition Generator,” CWRU Report CES-79-3, May 1979 (M.S. Thesis).

This has a lot of detail, but the IEEE paper came later, covers the same material, and is the one to read.