Logique

Logique des Systèmes Déductifs

Description : L’objectif est de présenter la logique comme un outil de modélisation, de montrer qu’on peut l’utiliser pour résoudre des problèmes sans coder dans un langage de programmation classique, et qu’on peut aussi l’utiliser pour modéliser la sémantique des programmes et faire des preuves de correction et de terminaison, ce qui mène au troisième bloc spécification/vérification/preuve. On abordera les solvers SAT et SMT, la preuve de programme, avec des mise en oeuvre en travaux pratiques.

Acquis d’apprentissage : À l’issue de ce cours, les élèves auront fait le lien entre les aspects théoriques de la logique et l’informatique, ouvrant la voie à l’informatique certifiée.

Modalités d’évaluation : Evaluation à partir des participations aux manipulations (TD/TP) et des résultats rendus

Compétences évaluées :

  • Certification

Responsable de cours : Benoît Valiron

Identifiant Geode : SPM-INF-021

CM :

  1. Leçon de choses (3.0 h)
  2. Logique propositionnelle, fonctionnement d’un solveur SAT (3.0 h)
  3. Extension avec des types, notion de théorie, fonctionnement d’un SMT (3.0 h)
  4. Logique de Hoare: logique sur les types du langage de programmation. (1.5 h)
  5. Calcul des plus faibles préconditions (WP), chainage, obligations de preuves. (1.5 h)

TD :

  1. Logique de Hoare (1.5 h)
  2. Exemple de dérivation (1.5 h)

TP :

  1. Ecriture d’un solveur SAT (3.0 h)
  2. Utilisation de Z3 (3.0 h)
  3. Outil Why3, exemple avec un calcul sur des entiers. (3.0 h)