Logique

Deductive systems logic

Evaluated skills:

  • Certification

Course supervisor: Benoît Valiron

Geode ID: 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)