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 (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)