Combining Tests and Proofs for Better Software Verification
Li Huang, Bertrand Meyer, Manuel Oriol
TL;DR
The paper reframes software verification as a complementarity between testing and proving, leveraging SMT-based counterexample generation and Design by Contract to convert proof failures into actionable artifacts such as tests, regression suites, and automated repairs. It introduces three core contributions: Proof2Test, which turns failed proofs into minimal counterexamples and executable tests; Proof2Fix, which uses counterexample invariants to automatically generate and validate fixes; and Seeding Contradiction (SC), a static method for producing high-coverage test suites, including MC/DC and loop unrolling enhancements. Empirical results on Eiffel programs show that this integrated approach can produce meaningful fixes with formal validation in about a minute per session, and generate regression tests with significant coverage improvements at speeds far surpassing many dynamic test-generation tools. Overall, the work demonstrates that proof-driven tests and repair mechanisms, grounded in contract-based specifications, offer a scalable path toward more reliable software verification and maintenance.
Abstract
Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on ``Satisfiability Modulo Theories'' (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.