Procédures de décision et vérification de programmes

L’objectif du cours est d’étudier les différentes procédures de décision utilisées pour l’analyse de programmes. Dans ce contexte, une propriété s’exprime par une formule logique dont il faut montrer la validité, modulo une théorie modélisant le programme. On s’intéresse à la théorie de l’égalité et à des théories permettant d’utiliser de l’arithmétique et des structures de données classiques (listes et tableaux).

La preuve d’une propriété fait souvent intervenir un mélange de théories. On étudie les méthodes de combinaison de procédures de décision qui permettent de résoudre un problème exprimé dans un tel mélange. On présente également une approche par réécriture pour concevoir des procédures de décision pour des théories axiomatisées en logique équationnelle. On détaille le fonctionnement d’un solveur SMT pour la Satisfiabilité Modulo des Théories, qui intègre des procédures de décision et un solveur pour la logique propositionnelle.