MDV: Méthodes Déductives pour la Vérification

• Intervenants : Thomas Genet, Vlad Rusu
• Volume : 21 heures
• Equipe de recherche : LANDE et VERTECS

Présentation

La vérification formelle de systèmes informatiques répond à un besoin croissant de sécurité de la part des utilisateurs et constitue un axe majeur dans la recherche informatique actuelle. Le but de ce cours est de présenter certains concepts communs aux méthodes formelles, en les illustrant par la vérification de programmes à l'aide de l'assistant de preuves PVS. Chacune des séances sera partagée en une partie théorique et une partie d'application sur machine. L'évaluation se fera par un examen écrit et par un projet à réaliser avec PVS.

Plan du module

1.

Introduction aux méthodes formelles: approches déductives et algorithmiques. Logique propositionnelle et des prédicats. Calcul des séquents.

2.

Indécidabilité de l'arithmétique non-linéaire. Théorème de Gödel. Arithmétique de Presburger, procédures de décision. Combinaison de procédures de décision pour les théories décidables.

3.

Termes, réécriture, preuve de propriétés non arithmétiques. Le problème de la décision dans les théories équationnelles.

4.

Fonctions récursives, mesures et preuves par induction. Ordres et principe d'induction bien fondée.

5.

Le système de types de PVS: sous-typage, typage dépendant, types abstraits. Leur utilisation pour détecter des erreurs tôt dans le processus de spécification.

6.

Spécification et preuves de programmes avec données. La méthode de renforcement systématique d'invariants. Abstractions et model-checking en PVS.

7.

Séance de récapitulation. Présentation, choix, et aide initiale pour l'élaboration des projets.

Bibliographie

• Un livre de logique, par exemple: "Logique et fondements de l'informatique" de Richard Lassaigne et Michel de Rougemont. Hermes 1993.
• A Tutorial Introduction to PVS, http://www.csl.sri.com/papers/wift-tutorial/
• J.-F. Monin. Comprendre les méthodes formelles. Masson 1996.