Procédures de décision pour la preuve de programmes

Parcours IL / Orientation MFLS

Dans ce cours, on s’intéresse plus particulièrement à la preuve (de programmes) et aux moteurs de preuve basés sur la Satisfiabilité Modulo des Théories (SMT). L’objectif est de comprendre les méthodes de preuve sous-jacentes. Un moteur SMT utilise différents composants: des procédures de décision (pour différentes théories), un solveur Booléen pour le calcul propositionnel, ainsi que des méthodes de combinaison lorsque le système à prouver est spécifié grâce à plusieurs théories. Les points importants qui seront étudiés sont :

  • un panorama des différentes théories utilisées dans le cadre de la preuve de programmes: théorie de l’égalité, fragments d’arithmétique, structures de données.
  • la descriiption pour chacune de ces théories, d’une procédure de décision à l’aide d’un système d’inférence dont la correction est montrée formellement.
  • la conception de nouvelles procédures de décision de façon incrémentale en appliquant des méthodes de combinaison et du raisonnement équationnel.
  • la spécification et l’analyse formelle du fonctionnement général d’un prouveur SMT.
  • l’étude approfondie de la mise en oeuvre d’un prouveur SMT.

Prérequis

Connaissances en logique et algorithmique.

Acquis d’apprentissage

  • Logique équationnelle et théories utilisées dans le contexte de la preuve de programmes.
  • Systèmes d’inférences, procédures de saturation et de combinaison.
  • Réécriture appliquée à la conception de procédures de décision.
  • Satisfiabilité propositionnelle et modulo des théories.

Compétences visées

  • Concevoir et développer des systèmes logiciels sûrs et sécurisés, notamment avec des méthodes formelles.
  • Maîtriser et mettre en oeuvre 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.
  • Spécifier et prouver en logique du premier ordre avec égalité.
  • Développer des outils d’aide à la décision.
  • Comprendre, analyser et concevoir des outils de vérification et de preuve.

Parcours IL / Orientation MFLS