Objectifs (en termes de compétences)

- Approfondir et formaliser les méthodes d'analyse et de preuve de programmes abordées lors de cours précédents.
- Connaître et comprendre les techniques d'automation qui permettent d'appliquer ces méthodes à des systèmes complexes.
- Apprécier par la pratique le potentiel et les limites de ces techniques.

Objet de l'activité (principaux thèmes à aborder)

- Approfondissement et formalisation des méthodes d'analyse déductives (logique de Hoare, calcul wp).

- Application aux programmes séquentiels, récursifs, aux structures de données, aux programmes réactifs.

- Automatisation de preuves déductives (annotations de programmes, conditions de vérification).

- Méthodes d'analyse comportementales (machine d'états et logique temporelle, model checking, approches symboliques).

Résumé : Contenu et Méthodes

Cours en auditoire et travail pratique individuel.

Autres informations (Pré-requis, Evaluation, Support, ...)

Références

K. R. Apt, E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer Verlag, 1991.

Autres crédits de l'activité dans les programmes