Algorithmique avancée

Les documents de ce cours ont été rédigés par Swarat Chaudhuri Emmanuel Filiot, K. Rustan M. Leino, Bas Luttik, Antoine Miné, Rosemary Monahan, Albert Oliveras, Enric Rodriguez-Carbonell, Christine Tasson, Eric Violard.

SAT

Cours

  1. Le problème SAT, Wikipedia Fr et En
  2. Logique propositionnelle
  3. Calcul propositionnel
  4. L'algorithme DPLL - présentation abstraite
  5. L'algorithme DPLL - présentation standard
  6. Modélisation SAT - partie 1
  7. Modélisation SAT - partie 2

Exercices

  1. Logique propositionnelle
  2. Calcul propositionnel
  3. Formes normales - résolution
  4. Tuto solveurs SAT
  5. MiniSAT, version Javascript
  6. SAT4J, un solveur SAT en Java
  7. Principe des tiroirs de Dirichlet, version SAT
  8. Modélisation SAT

SMT

Cours

  1. SMT modulo théories (Wikipedia Fr et En)
  2. Introduction
  3. Un exemple : la difference logic
  4. L'algorithme de Bellman-Ford (Wikipedia Fr et En), un exemple de programmation dynamique (Wikipedia Fr et En)

Exercices

  1. Tuto solveurs SMT
  2. Z3 en ligne
  3. Exercices Z3

Vérification déductive

Cours

  1. Variants et invariants
  2. Axiomatic Semantics (page 1--24), un cours en français
  3. Résumé pour prouver la correction totale des boucles

Exercices

  1. Logique de Hoare
  2. Programmation par contrat avec Dafny, suivre le tutoriel

Evaluation

Contrôle continu : deux partiels sans document ni moyen électronique, 50% + 50%
Deuxième session : examen écrit sans document ni moyen électronique, tout est au programme, 100%.

Annales

Bibliographie


Valid HTML5