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
Conference papers

Explaining Counterexamples with Giant-Step Assertion Checking

Benedikt Becker 1 Cláudio Lourenço 1 Claude Marché 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : Identifying the cause of a proof failure during deductive verification of programs is hard: it may be due to an incorrectness in the program, an incompleteness in the program annotations, or an incompleteness of the prover. The changes needed to resolve a proof failure depend on its category, but the prover cannot provide any help on the categorisation. When using an SMT solver to discharge a proof obligation, that solver can propose a model from a failed attempt, from which a possible counterexample can be derived. But the counterexample may be invalid, in which case it may add more confusion than help. To check the validity of a counterexample and to categorise the proof failure, we propose the comparison between the run-time assertion-checking (RAC) executions under two different semantics, using the counterexample as an oracle. The first RAC execution follows the normal program semantics, and 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 :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03217393
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, May 4, 2021 - 6:18:06 PM
Last modification on : Thursday, February 3, 2022 - 11:16:27 AM
Long-term archiving on: : Thursday, August 5, 2021 - 8:12:25 PM

File

fide.pdf
Files produced by the author(s)

Identifiers

Citation

Benedikt Becker, Cláudio Lourenço, Claude Marché. Explaining Counterexamples with Giant-Step Assertion Checking. F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩. ⟨hal-03217393⟩

Share

Metrics

Record views

76

Files downloads

102