EC Aspects formels du génie logiciel

Cette UE approfondit l’UE "Logiciels sûrs" du M1 en abordant d’une part différents aspects de la vérification formelle, et d’autre part en complétant celle-ci par une étude de cas reposant sur des outils utilisés dans l’industrie du logiciel.

L'enseignement se compose de deux parties.

1) La première partie concerne les modèles formels de la programmation, de la modélisation et de la spécification. En particulier les différentes approches de la vérification formelle (vérification déductive, model-checking, interprétation abstraite) de logiciels pourront être abordés. Les systèmes formels (munis de leur système de preuve) supports des différentes méthodes formelles de vérification seront étudiés.

2) La seconde partie est axée sur l'expérimentation des outils industriels de vérification formelle des logiciels. Les outils expérimentés seront par exemple la plateforme Why3, la plateforme Frama-C d’analyse de programmes C, Key l'outil de vérification de programmes Java ou d'autres outils de vérification formelle émergeant dans ce domaine très actif.

- Maîtriser les modèles formels de la programmation, de la modélisation et de la spécification.
- Mettre en oeuvre des outils industriels de vérification formelle des logiciels.

Compétences visée : maîtriser le développement d’une vérification formelle d’un logiciel. Savoir s’orienter dans les différentes technologies disponibles. Comprendre les enjeux d’une vérification formelle et la pertinence de sa mise en oeuvre.

UE Logiciels sûrs et Génie Logiciel 1 et 2 de la première année du master d’Informatique. Notions de logique.

Maîtriser le développement d’une vérification formelle d’un logiciel. Savoir s’orienter dans les différentes technologies disponibles. Comprendre les enjeux d’une vérification formelle et la pertinence de sa mise en oeuvre.