Your Proof Fails? Testing Helps to Find the Reason
This addresses the challenge of lack of feedback in formal verification for software developers, though it is incremental as it builds on existing verification tools.
The paper tackles the problem of diagnosing proof failures in deductive verification by proposing a methodology that uses test generation to identify the cause and provide counter-examples, with initial experiments showing it can precisely diagnose most failures.
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a new methodology where test generation helps to identify the reason of a proof failure and to exhibit a counter-example clearly illustrating the issue. We describe how to transform an annotated C program into C code suitable for testing and illustrate the benefits of the method on comprehensive examples. The method has been implemented in STADY, a plugin of the software analysis platform FRAMA-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.