HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Giant-step Semantics for the Categorisation of Counterexamples

Abstract : Deductive Verification aims at verifying that a given program code conforms to a formal specification of its intended behaviour. That approach proceeds by generating mathematical statements whose validity entails the conformance of the program. Such statements are typically given to automated theorem provers. This work aims at providing help to the programmer in the case when the proofs fail. Indeed, identifying the cause of a proof failure during deductive verification of a program is hard: it may be due either to an incorrectness in the program, to an incompleteness in the program annotations, or to an incompleteness of the prover itself. The kind of modifications to perform so as to fix the proof failure depends on its category, but the prover alone cannot provide any help on the categorisation. In practice, when using an SMT solver to discharge a proof obligation, such a solver can propose a model from a failed proof attempt, from which a candidate counterexample can be derived. But it appears that such a counterexample may be invalid, in which case it may add more confusion than help to the programmer. The goal of this work is both to check for the validity of a counterexample and to categorise the proof failure. We propose an approach that builds upon the comparison between the run-time assertion checking (RAC) executions of the program (and its specifications) under two different semantics, using the counterexample as an oracle. The first RAC execution follows the normal program semantics, so that a violation of a program annotation indicates an incorrectness in the program. The second RAC execution follows a novel "giant-step'' semantics that does not execute loops nor function calls but instead retrieves return values and values of modified variables from the oracle. A violation of the program annotations only observed under giant-step execution characterises an incompleteness of the program annotations. We implemented this approach in the Why3 platform for deductive program verification and evaluated it using examples from prior literature.
Document type :
Complete list of metadata

Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Friday, April 30, 2021 - 1:43:21 PM
Last modification on : Friday, February 4, 2022 - 3:08:33 AM
Long-term archiving on: : Saturday, July 31, 2021 - 6:55:54 PM


Files produced by the author(s)


  • HAL Id : hal-03213438, version 1


Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. Giant-step Semantics for the Categorisation of Counterexamples. [Research Report] RR-9407, Inria. 2021, pp.43. ⟨hal-03213438⟩



Record views


Files downloads