Skip to Main content Skip to Navigation
Conference papers

Counterexamples from Proof Failures in SPARK

Abstract : A major issue in the activity of deductive program verification is the understanding of the reason why a proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification, it is essential to provide means to investigate such a failure. We present our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment, exhibiting values for the variables of the program where a given part of the specification fails to be validated. To produce a counterexample , we exploit the ability of SMT 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 trivial because of the many transformations leading from a given code and specification to a verification condition.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, May 12, 2016 - 12:08:30 PM
Last modification on : Thursday, July 8, 2021 - 3:46:20 AM
Long-term archiving on: : Wednesday, November 16, 2016 - 2:17:02 AM


Files produced by the author(s)


  • HAL Id : hal-01314885, version 1


David Hauzar, Claude Marché, Yannick Moy. Counterexamples from Proof Failures in SPARK. Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. ⟨hal-01314885⟩



Record views


Files downloads