Counterexamples from Proof Failures in SPARK - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

Counterexamples from Proof Failures in SPARK

(1, 2) , (1, 2) , (3)
1
2
3

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.
Fichier principal
Vignette du fichier
article.pdf (226.44 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01314885 , version 1 (12-05-2016)

Identifiers

  • HAL Id : hal-01314885 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More