Susanne Graf et Hassen Saidi primés pour leurs travaux sur la vérification automatique de programmes

La vérification assistée par ordinateur permet de s’assurer qu’un algorithme ou un programme fonctionne comme prévu, de manière considérablement plus rapide et efficace qu’en testant à la main chaque cas de figure. Mais dès les débuts de l’informatique, Alan Turing avait montré que ce problème est impossible à résoudre dans le cas général, c’est-à-dire qu’il faudrait malheureusement vérifier chaque cas un par un alors qu’ils peuvent être d’une quantité infinie. Depuis, la communauté de la vérification assistée par ordinateur conçoit des approches algorithmiques qui combinent une complexité acceptable et des résultats satisfaisants. Les outils de vérification assistée par ordinateur sont par exemple utilisés lors de la conception de microprocesseurs, de commandes de vol d’avion ou dans d’autres contextes où un dysfonctionnement du matériel ou du logiciel aurait des conséquences graves, voire fatales.

L’une des principales conférences internationales du domaine, Computer aided verification (CAV), a récompensé les travaux fondateurs de Susanne Graf, directrice de recherche CNRS au laboratoire Verimag et de Hassen Saidi, chercheur au SRI International. Cet article, publié lors de la conférence CAV 1997, continue d’irriguer la vérification assistée par ordinateur.

Dans Construction of abstract state graphs with PVS, ils ont proposé une méthode basée sur le prouveur de théorèmes Prototype verification system (PVS), développé au SRI International, pour construire automatiquement un graphe d’états abstraits d’un système. Les états sont ici les évaluations des prédicats, qui sont des propriétés des variables et des données du système qui doivent être satisfaites pour que la prochaine instruction du système puisse s’exécuter. Répétée, cette méthode permet de construire de bonnes approximations du graphe d’état réel, qui reste quant à lui généralement inaccessible en un temps raisonnable. Notons que cette approche permet également de construire un graphe fini même pour un programme dont le graphe d’état réel est infini.

Le graphe ainsi obtenu représente une surapproximation des états effectivement accessibles et des transitions possibles. Toute propriété de sûreté satisfaite sur ce graphe abstrait l’est également sur le graphe d’état réel.

Cette technique, appelée par la suite predicate abstraction, pour abstraction basée sur les prédicats, a déclenché une véritable avalanche de travaux et trouvé d’innombrables applications.

L’abstraction basée sur les prédicats est notamment à la base de l’approche de vérification de logiciels CEGAR, mise en œuvre dans des outils tels que SLAM à Microsoft Research et Blast à l’Université de Berkley. « Normalement, le prix de CAV récompense des travaux vieux de dix à vingt ans, la fenêtre a été étendue spécialement pour nous, s’amuse Susanne Graf, qui s’est depuis orientée vers l’étude des systèmes embarqués et la vérification de systèmes temps réel. C’est une belle preuve de l’importance de notre contribution.