Counterexamples from proof failures in the SPARK program verifier

Abstract : A major issue in the activity of deductive program verification is the understanding of the reason for why some proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification of her program, it is essential to provide means to investigate such a failure. To that mean, we propose a technique for generating counterexamples, exhibiting some values for the variables of the program where a given part of the specification fails to be validated. To produce such a counterexample, we exploit the ability of SMT (Satisfiability Modulo Theories) solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not a trivial task because of the many transformations that lead from a given code and specification to a verification condition. We report on our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment for the development of safety-critical Ada programs
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01271174
Contributor : Claude Marché <>
Submitted on : Monday, February 8, 2016 - 6:51:59 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, November 12, 2016 - 2:15:07 PM

File

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

Identifiers

  • HAL Id : hal-01271174, version 1

Citation

David Hauzar, Claude Marché, Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. [Research Report] RR-8854, Inria. 2016, pp.22. ⟨hal-01271174⟩

Share

Metrics

Record views

432

Files downloads

535