Counterexamples from proof failures in the SPARK program verifier

Contre-exemples issus d'échecs de preuve dans l'environnement SPARK

David Hauzar (1, 2) , Claude Marché (1, 2) , Yannick Moy (3)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
2 LRI - Laboratoire de Recherche en Informatique
3 AdaCore (FRANCE)

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

Un défi important de l’activité de vérification déductive de programmes est la compréhension de la raison pour laquelle une certaine preuve échoue. Pour aider l’utilisateur à comprendre le problème et à décider quoi modifier dans son code ou bien sa spécification, il est essentiel de fournir des moyens d’analyser l’échec de preuve. À cette fin, nous proposons une technique de génération de contre-exemples, qui exhibent des valeurs pour les variables du programme pour lesquelles une certaine partie de la spécification ne peut pas être prouvée. Pour produire un tel contre-exemple, nous exploitons la capacité des solveurs SMT (Satisfiability Modulo Theories) de proposer, quand une formule n’est pas prouvée, un contre-modèle. Transformer un tel contre-modèle en un contre-exemple pour le programme de départ n’est pas une tâche facile à cause des multiples transformations qui conduisent du code et de la spécification de départ vers une obligation de preuve. Nous présentons l’approche que nous avons suivie pour la conception et l’implémentation de la génération de contre-exemples dans le cadre de l’environnement SPARK 2014 pour le développement de programmes Ada critiques

Mots clés: Formal Specification; Deductive Verification; Formal Proof; Counterexamples; Program Ver- ifiers Why3 and SPARK

Domaines: Logique en informatique [cs.LO]; Génie logiciel [cs.SE]

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⟩