Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/hal-03213438
Contributor : Claude Marché <>
Submitted on : Friday, April 30, 2021 - 1:43:21 PM
Last modification on : Sunday, May 2, 2021 - 3:29:05 AM

File

RR-9407.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03213438, version 1

Citation

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⟩

Share

Metrics

Record views

19

Files downloads

28