1) Initiation aux problèmes de vérification de logiciels : limitations fondamentales (calculabilité), principales approches, lien avec la compilation...
2) Réalisation pratique (projet) d'un logiciel de vérification ou d'un logiciel vérifié formellement.

De nos jours, de nombreux systèmes sont contrôlés par des logiciels de plus en plus complexes. De plus, les conséquences d'erreurs logicielles peuvent se révéler catastrophiques, dans le cas de systèmes embarqués (par exemple, dans le domaine aéronautique ou dans le secteur médical) ou de systèmes manipulant des informations sensibles (par exemple dans le domaine bancaire). La conception de systèmes matériels fait face à des difficultés similaires. Afin de maîtriser cette complexité on ne peut plus se contenter de méthodes manuelles ou heuristiques.

Cet EA a pour objectifs :

- d'étudier comment un programme critique peut être garanti "sans bugs" grâce à des outils logiciels spécialisés
- de mettre en oeuvre ces techniques dans la réalisation d'une application embarquée et prouvée

Plus précisément, cet EA comporte une introduction aux techniques de vérification telles que :

- l'analyse statique de programme / l'interprétation abstraite
- le model-checking (à état explicite ou implicite)
- la résolution d'obligations de preuves en logique de Hoare
- la preuve interactive dans des logiques de spécification.

Cet EA donne les clefs de compréhension de ces techniques et surtout leur mise en pratique par l'usage d'outils logiciels tels que Coq, Why/Alt-Ergo, Astrée ou Java pathfinder...

Les travaux pratiques commenceront par le traitement de quelques problèmes simples de sécurité informatique et évolueront, au fur et à mesure des séances, vers des projets. Ceux-ci pourront tourner autour de la conception d'un petit interpréteur abstrait, de la certification d'un petit compilateur pour un mini-langage fonctionnel, ou d'autres projets plus individualisés selon les envies
des élèves.

Remarque : cet EA fusionne les modules INF563 "Analyse statique de programmmes" et INF565 "Systèmes de preuve", avec un côté applicatif renforcé.

Niveau requis : Il est très fortement recommandé de savoir programmer en OCaml (il y a une remise à niveau au mois de septembre). Il est également souhaitable (mais pas obligatoire) d'avoir des notions de raisonnement automatique par ordinateur, de logique ou encore de compilation.

Modalités d'évaluation : Projet, typiquement réalisation d'un logiciel prouvé en Coq ou programmé en OCaml, avec remise des listings et soutenance orale

Dernière mise à jour : jeudi 28 mars 2013