23/10/2008 Jean-Christophe Filliâtre (LRI, Orsay)

La plateforme Why de vérification déductive de programmes C et Java

Cet exposé présente la plateforme Why (http://why.lri.fr/), un ensemble de techniques et d'outils développés dans le projet ProVal pour la vérification de propriétés fonctionnelles de codes C et Java. La plateforme Why s'appuie sur plusieurs principes : (1) la spécification des programmes par l'intermédiaire d'annotations dans le source, en utilisant des langages inspirés de JML ; (2) un calcul de plus faibles préconditions reposant sur un modèle mémoire de type Burstall-Bornat raffiné par une analyse statique de séparation ; et enfin (3) la possibilité d'utiliser un grand nombre d'outils de preuve existants, tant automatiques qu'interactifs, pour décharger les obligations de preuve.