Parcours IL / Orientation MFLS
L’objectif de cette UE est d’introduire des concepts et méthodes avancés pour la preuve de programmes. Une première partie est consacrée à l’utilisation de la logique de séparation comme langage d’assertions pour prouver des programmes complexes, notamment avec des structures de données mutables. Une seconde partie traite de la preuve interactive de spécifications et de la programmation certifiée avec une mise en œuvre avec un assistant de preuve.
Prérequis
- Connaissances de base en logique, programmation et spécification.
Acquis d’apprentissage
- Logique de séparation (SL) et preuves de programmes
- SL comme langage d’assertions
- preuves de programmes avec structures de données inductives, listes et arbres
- mise en œuvre avec l’outil Smallfoot.
- Programmation certifiée en Coq
- programmation et spécification
- preuve interactive de spécifications
- extraction de programmes certifiés
- types dépendants et combinaison de la programmation et de la certification
- mise en œuvre avec l’outil CoqIDE
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 sur des structures de données mutables.
- Utiliser sur des exemples concrets des outils de preuve et de vérification pour des programmes complexes.