Combining Tests and Proofs for Better Software Verification

TL;DR

This paper explores integrating testing and proving techniques in software verification, leveraging Design by Contract and SMT-based counterexample generation to improve testing, fault detection, and automatic repair.

Contribution

It introduces a unified approach combining testing and proving using Eiffel's Design by Contract and SMT tools, enabling automatic test generation and verified program fixes.

Findings

Counterexamples can be used for automatic test generation.

Faults can be introduced and fixed with guarantees of correctness.

Counterexample-based methods improve testing and repair processes.

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.