Titre:
Validation automatique de programmes
Conférencier:
Adel Bouhoula ,
Chargé de Recherche INRIA, INRIA Lorraine
615 rue du Jardin Botanique - B.P. 10154602 Villers-lès-Nancy Cedex, France
Lieu:
Université de Montréal, Pavillon André-Aisenstadt ,
Salle 3195
Date et heure:
mardi le 13 octobre 1998 de
15:00 à 00:00
Résumé:
Il existe essentiellement deux approches pour la validation de programmes: d'une part, se trouvent les approches du type "model checking" qui ont été rendues effectives par l'im- plantation effcace du calcul booléen par des diagrammes de décision binaires (BDD). Ces approches ont l'avantage d'avoir été complètement automatisées et elles ont remporté un vif succès pour la vérification des systèmes d'états finis. Cependant elles demeurent restreintes à cette classe et peuvent même se heurter à des difficultés d'explosion combinatoire.
D'autre part se trouvent les outils fondés sur des logiques puissantes. Ces logiques ont une grande expressivité et prennent en compte aisément des aspects génériques non traitables par les approches précédentes. Par contre leur automatisation est souvent faible et l'interaction avec l'utilisateur primordiale pour guider une preuve. Ceci demande une bonne culture mathématique de la part de l'utilisateur, voire une expertise de logicien. Notre objectif se place dans le cadre de travaux se situant entre ces deux extrêmes. Les raisons qui nous motivent sont issues du constat qu'aucune de ces deux approches n'est complètement satisfaisante et qu'il nous semble possible, sur des problèmes particuliers, d'obtenir un compromis efficace. Nous voulons limiter les interventions de l'utilisateur en offrant un maximum d'automatisation des preuves. Il est clair qu'il faut pour cela se restreindre à une classe de problèmes raisonnable. Mais il s'agit de ne pas se limiter à des domaines finis, pour pouvoir prendre en compte des problèmes génériques et paramétrés, tout en restant dans le cadre de méthodes automatiques ou semi-automatiques. Je présenterai au cours de ce séminaire mes derniers travaux sur la validation auto- matique de programmes.