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.
[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.