Generating Error Traces from Verification-Condition Counterexamples
Science of Computer Programming (SCP), 55(1-3):209-226, March 2005.
Rustan Leino, Todd Millstein, James Saxe
A technique for finding errors in computer programs is to translate a
given program and its correctness criteria into a logical formula in
mathematics and then let an automatic theorem prover check the
validity of the formula. This approach gives the tool designer much
flexibility in which conditions are to be checked, and the technique
can reason about as many aspects of the given program as the
underlying theorem prover allows. This paper describes a method for
reconstructing, from the theorem prover's mathematical output, error
traces that lead to the program errors that the theorem prover
discovers.
[PDF]