Vérification déductive via débogage fantôme

We present a verification approach based on auxiliary programs, which we call ghost debuggers.This approach leads to notable verification gains when the structure of the program does not match theexecution structure, notably when that latter structure is recursive. We present a theoretical foundationof our approach over a flavor of transfinite games, which let us specify and prove fine-grained propertiesabout infinite behaviors of programs. By making use of the game structure, we also show that our approachcan be applied to relational properties like simulation between programs. Our approach is backed by amechanized development in the Why3 tool, which formally proves sound the Hoare-style logic backboneof our approach.Nous présentons une nouvelle approche de vérification de programmes que nous appelonsDébogage Fantôme. Cette approche apporte des gains notables lorsque la structure syntaxique du codesource du programme à vérifier ne correspond pas à la structure de son exécution, notamment lorsque cettedernière est récursive. Nous présentons un fondement théorique de notre approche sur une variante dejeux transfinis, qui nous permet de spécifier et prouver des propriétés fines sur les comportements infinisdes programmes. En utilisant la structure du jeu, nous montrons également que notre approche peut êtreappliquée à des propriétés relationnelles comme la simulation entre les programmes. Notre approcheest formalisée par un développement dans l’outil Why3, qui nous permet de valider mécaniquement lacorrection de la logique à la Hoare qui sous-tend notre approche