====Software Verification====

Responsables : [[https://labri.fr/perso/vpenelle| Vincent Penelle]], [[https://labri.fr/perso/sutre | Grégoire Sutre]] et [[https://labri.fr/perso/leroux| Jérôme Leroux]]

Ce cours du S9 est obligatoire pour VL et en option pour AM. Il vaut 6ECTS.

===Résumé===

Ce cours a pour but principal d’introduire des techniques classiques de vérification et de les implémenter dans un vérificateur de programmes (simples). L’outil réalisé au cours du semestre est capable de détecter des violation d’assertions sur des programmes dans un sous-langage du C (uniquement des entiers et pas de pointeurs) sans que l’utilisateur ait à fournir d’autres information que le programme.

La [[https://www.labri.fr/perso/vpenelle/Enseignement/VerificationDesLogiciels|partie 1]], enseignée par Vincent Penelle, présente le cadre général du vérificateur (notamment le langage vérifié et sa sémantique), vise à familiariser avec le langage utilisé (Ocaml) et le SMT-solveur utilisé (Z3), et présente la technique du Bounded Model Checking à travers deux algorithmes pour le réaliser.

La partie 2, enseignée par Grégoire Sutre, présente la technique de l’interprétation abstraite, qui consiste à regarder des abstractions de l’ensemble des exécutions d’un programme dans un domaine mathématique bien ordonné plus simple. Durant cette partie, plusieurs domaines abstraits simples sont implémentés.

La partie 3, enseignée par Jérôme Leroux, présente la technique du raffinement d’abstraction guidé par contre-exemple (CEGAR) et quelques bases sur les réseaux de Petri.