Logique

Deductive systems logic

Description: The objective is to present logic as a modeling tool, to show that it can be used to solve problems without coding in a traditional programming language, and that it can also be used to model the semantics of programs and prove correctness and termination, which leads to the third block: specification/verification/proof. We will cover SAT and SMT solvers and program proof, with practical implementation exercises.

Learning outcomes: At the end of this course, students will have made the connection between the theoretical aspects of logic and computer science, paving the way for certified computer science.

Evaluated skills:

  • Certification

Course supervisor: Benoît Valiron

Geode ID: SPM-INF-021

CM:

  1. Leçon de choses 1/2 (1.5 h)
  2. Leçon de choses 2/2 (1.5 h)
  3. Logique propositionnelle, fonctionnement d’un solveur SAT 1/2 (1.5 h)
  4. Logique propositionnelle, fonctionnement d’un solveur SAT 2/2 (1.5 h)
  5. Extension avec des types, notion de théorie, fonctionnement d’un SMT 1/2 (1.5 h)
  6. Extension avec des types, notion de théorie, fonctionnement d’un SMT 2/2 (1.5 h)
  7. Logique de Hoare: logique sur les types du langage de programmation. (1.5 h)
  8. 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)