Your Proof Fails? Testing Helps to Find the Reason

TL;DR

This paper introduces a methodology that combines testing with deductive verification to diagnose proof failures in program correctness, providing clearer feedback and counter-examples.

Contribution

It proposes a novel approach integrating test generation into formal verification to identify reasons for proof failures and improve diagnosis accuracy.

Findings

Effective in diagnosing proof failures

Detects non-compliance and contract weaknesses

Implemented in the STADY plugin for FRAMA-C

Abstract

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.