Méthode de programmation : preuves et schémas
[SINF2224]
[30h + 15h] 5 crédits
Cette activité se déroule pendant le 2e quadrimestre.
Enseignants : Charles Pecheur
Langue d'enseignement : Anglais
Niveau : Second cycle
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.