Parcours IL / Orientation IL & MFLS
L’objectif de cette UE est d’introduire les principaux concepts et méthodes en vue de maîtriser la preuve de programmes fonctionnels ou impératifs. Dans le premier cas on se focalise sur les preuves par induction à partir de structures de données inductives simples. Dans le second on considére l’utilisation des sémantiques formelles pour la preuve de propriétés de programmes mais surtout la sémantique axiomatique (Logique de Hoare) et sa mise en oeuvre.
L’UE inclut l’étude de la mécanisation des preuves et la mise en oeuvre à l’aide d’un assistant de preuve.
Prérequis
- Connaissances de base en logique, sémantique et programmation.
Acquis d’apprentissage
- Logique d’ordre supérieur.
- Types de données abstraits et prédicats inductifs.
- Preuves sur les structures de données récursives simples (listes).
- Sémantiques formelles et preuves de programmes.
- Logique de Floyd-Hoare:
- Triplets, pre- et post-conditions;
- Invariants, preuves de correction.
- Mécanisation des preuves.
Compétences visées
- Intégrer des méthodes et techniques formelles de modélisation, d’analyse, de vérification et de validation dans le processus de développement de logiciels critiques.
- Maîtriser et mettre en œuvre les méthodes formelles pour la spécification ou modélisation d’un problème donné, la preuve et la vérification de propriétés dans le contexte de la sûreté et la sécurité logicielle.
- Concevoir et développer des approches formelles adaptées, leur combinaison et des outils associés, pour la certification de systèmes complexes.
- Développer des preuves de programmes.
- Utiliser sur des exemples concrets un assistant de preuve pour prouver des programmes.