Une sémantique à pas de géant pour la catégorisation des contre-exemples

Autor: Benedikt Becker, Cláudio Belo Lourenço, Claude Marché
Přispěvatelé: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), This work has been partially supported by the bilateral contract ProofInUse-AdaCore between Inria team Toccata and AdaCore company, Paris, France, and by the bilateral contract ProofInUse-MERCE between Toccata and Mitsubishi Electric R&D Centre Europe, Rennes, France., Inria
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: [Research Report] RR-9407, Inria. 2021, pp.43
HAL
Popis: Deductive Verification aims at verifying that a given program code conforms to a formal specification of its intended behaviour. That approachproceeds by generating mathematical statements whose validity entails the conformance of the program. Such statements are typically given to automated theorem provers. This work aims at providing help to the programmer in the case when the proofs fail. Indeed, identifying the cause of a proof failure during deductive verification of a program is hard: it may be due either to an incorrectness in the program, to an incompleteness in the program annotations, or to an incompleteness of the prover itself. The kind of modifications to perform so as to fix the proof failure depends on its category, but the prover alone cannot provide any help on the categorisation. In practice, when using an SMT solver to discharge a proof obligation, such a solver can propose a model from a failed proof attempt, from which a candidate counterexample can be derived. But it appears that such acounterexample may be invalid, in which case it may add more confusion than help to the programmer. The goal of this work is both to check for the validity of a counterexample and to categorise the proof failure. We propose an approach that builds upon the comparison between the run-time assertion checking (RAC) executions of the program (and its specifications) under two different semantics, using the counterexample as an oracle. The first RAC execution follows the normal program semantics, so that a violation of a program annotation indicates an incorrectness in the program. The second RAC execution follows a novel "giant-step'' semantics that does not execute loops nor function calls but instead retrieves return values and values of modified variables from the oracle. A violation of the program annotations only observed under giant-step execution characterises an incompleteness of the program annotations. We implemented this approach in the Why3 platform for deductive program verification and evaluated it using examples from prior literature.; La vérification déductive cherche à vérifier que le code d'un programme donné est conforme à une spécification formelle de son comportement prévu. Cette approche procède en générant des énoncés mathématiques dont la validité implique la conformité du programme. De tels énoncés sont généralement transmis à des prouveurs automatiques de théorèmes. Le travail présenté dans ce rapport vise à fournir une aide au programmeur dans le cas où les preuves échouent. En effet, identifier la cause d'un échec de preuve lors de la vérification déductive d'un programme est difficile: cela peut être dû soit à une erreur dans le programme, soit à une incomplétude dans les annotations du programme, ou encore à une incomplétude du prouveur lui-même. Le type de modification à effectuer pour corriger l'échec de la preuve dépend de sa catégorie, mais le prouveur ne peut à lui seul fournir de l'aide à cette catégorisation. En pratique, lors de l'utilisation d'un solveur de type SMT pour prouver une obligation de preuve, un tel solveur peut proposer un modèle à partir d'une tentative de preuve ratée, à partir duquel un contre-exemplepotentiel peut être dérivé. Mais il s'avère qu'un tel contre-exemple peut être invalide, auquel cas il peut apporter plus de confusion que d'aide auprogrammeur. Le but de ce travail est à la fois de vérifier la validité d'un contre-exemple et de catégoriser l'échec de la preuve. Nous proposons une approche qui s'appuie sur la comparaison entre des exécutions «~RAC~» (Run-time Assertion Checking) du programme (et de ses spécifications) sous deux sémantiques différentes, en utilisant le contre-exemple comme un oracle. La première exécution RAC suit la sémantique habituelle du programme, de sorte qu'une violation d'une annotation du code indique une erreur dans le programme. La deuxième exécution RAC suit une sémantique originale dite «~à pas de géant~» qui n'exécute ni les boucles ni les appels de fonction, mais récupère à la place depuis l'oracle les valeurs de retour et les valeurs des variables modifiées. Une violation des annotations du programme observée uniquement sous l'exécution à pas de géant caractérise une incomplétude des annotations du programme. Nous avons implémenté cette approche dans la plateforme Why3 pour lavérification déductive, et nous l'avons évalué sur une base d’exemples tirés de la littérature antérieure.
Databáze: OpenAIRE
Externí odkaz: