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.