Vérification de logiciels

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.

Partie 1:

Cadre général du vérificateur (notamment le langage vérifié et sa sémantique), visant à familiariser avec le langage utilisé (Ocaml) et le SMT-solveur utilisé (Z3), et présentation de la technique du Bounded Model Checking à travers deux algorithmes pour le réaliser.

Partie 2:

Introduction à 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.

Partie 3:

Présentation de la technique du raffinement d’abstraction guidé par contre-exemple (CEGAR) et quelques bases sur les réseaux de Petri.