Explaining Counterexamples with Giant-Step Assertion Checking
| Autor: | Becker, Benedikt, Lourenço, Cláudio Belo, Marché, Claude |
|---|---|
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | EPTCS 338, 2021, pp. 82-88 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.338.10 |
| Popis: | 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. Comment: In Proceedings F-IDE 2021, arXiv:2108.02369 |
| Databáze: | arXiv |
| Externí odkaz: |
|