A Failed Proof Can Yield a Useful Test

A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, failed proofs leave the programmer guessing. Can we put them to good use? The work reported here takes advantage of the rich internal information that automatic provers collect about the program when attempting a proof. If the proof fails, we use the counterexample generated by the prover (specifically, the SMT solver underlying the proof environment Boogie, used in the AutoProof system to perform correctness proofs of contract-equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents the Proof2Test tool implementing these ideas and demonstrates their application to a collection of examples.