Skip to Main content Skip to Navigation
Journal articles

Instrumenting a Weakest Precondition Calculus for Counterexample Generation

Sylvain Dailler 1 David Hauzar 1, 2 Claude Marché 1 Yannick Moy 2 
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : A major issue in the activity of deductive program verification is to understand why automated provers fail to discharge a proof obligation. 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, 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 particular piece of code and its specification to a set of proof goals given to external provers.
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, May 29, 2018 - 1:11:07 PM
Last modification on : Saturday, June 25, 2022 - 10:31:47 PM
Long-term archiving on: : Thursday, August 30, 2018 - 2:48:11 PM


Files produced by the author(s)


  • HAL Id : hal-01802488, version 1


Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy. Instrumenting a Weakest Precondition Calculus for Counterexample Generation. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2018, 99, pp.97-113. ⟨hal-01802488⟩



Record views


Files downloads