Generating Error Traces from Verification-Condition Counterexamples

  • Rustan Leino ,
  • Todd Millstein ,
  • James B. Saxe

Science of Computer Programming - Formal methods for components and objects pragmatic aspects and applications | , Vol 55(1-3): pp. 209-226

Publication

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.