A Failed Proof Can Yield a Useful Test

TL;DR

This paper introduces a method to extract useful test cases from failed automated proofs by leveraging counterexamples generated during proof attempts, aiding programmers in debugging and correcting programs.

Contribution

It presents the Proof2Test tool that converts failed proof attempts into actionable test cases using SMT solver counterexamples, enhancing program verification feedback.

Findings

Proof2Test successfully generates useful tests from failed proofs.

Counterexamples provide valuable debugging information.

The approach improves the utility of failed proofs in software verification.

Abstract

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, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich internal information that some automatic provers collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses 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 and demonstrates the application of the ideas and tool to a collection of representative examples.