Petiot et al. present testing software components that help optimize the effort of “applying deductive verification to formally prove that a [computer] program respects its formal specification.”
The purpose of the proposed research is to deliver a methodology that exploits test cases “to identify the reason of a proof failure and to produce a counterexample clearly illustrating the issue.” For this, the authors define categories of proof failures, for example, non-compliance, subcontract weakness (after discussing the notions of contract and subcontract), and prover incapacity, and subsequently provide detailed examples with code excerpts of how these failures get detected by applying tests. After outlining the testing cases and methodology for detecting these failures, the authors introduce a method of structural testing that identifies the failure type and suggests the most suitable actions related to the verification task.
The described method is implemented as a FRAMA-C plugin, called STADY. The reported experiments with STADY, based on 26 annotated programs, show that the proposed method is able to correctly classify most of the proof failures.
A very thoroughly presented account with many technical details and a solid related work analysis, this paper is a good read for theoretical computer scientists and programmers looking to optimize the performance of their programming practices or to design methods to automate the detection of proof failures.