CVFP Conception et vérification formelle de programmes 
Software design and verification

Magistère informatique et télécommunications - ENS Rennes - Année 2016/2017

Intervenants

mardi 6 septembre 2016	Classes de complexité NP Tuiles de Wang. Problème de pavage d'un rectangle. Machine de Turing non-déterministe (normalisée). NP-dureté du problème de pavage d'un rectangle. Logique propositionnelle : syntaxe et sémantique. SAT Réduction polynomiale du problème de pavage d'un rectangle à SAT Théorème de Cook PSPACE Définition de PSPACE et NPSPACE. Pavage d'un corridor. Logique QBF : syntaxe et sémantique. TQBF dans PSPACE.
13 septembre 2016	PSPACE (suite) Pavage d'un corridor NPSPACE-dur. TQBF est NPSPACE-dur. Théorème de Savitch (PSPACE = NPSPACE). Algorithme DPLL Pourquoi on peut se restreindre aux CNF : transformation de Tseitin. Démonstration de la correction de la transformation de Tseitin (non fait en cours) DPLL avec backtracking Valuations partielles. Clause unitaire. Propagation unitaire. Version récursive. Défaut du backtrack. Backtracking explicite
20 septembre 2016	TP : installer zchaff, étudier le parseur cnf fourni, programmer un sat solveur naif (avec récursivité), discussion sur la mise en place d'une procédure de test A faire pour la fois suivante : finir le solveur (chacun fait le sien), avancer sur la procédure de test (un binôme seulement), proposer un front-end de coloration de graphe (un binôme seulement)
27 septembre 2016	TP : Discussion sur l'architecture
4 octobre 2016	DPLL avec backjumping Graphe d'implication. Apprentissage de clauses. Backjumping. Démonstration de la correction et de la terminaison. Demonstration of DPLL algorithm with backjumping and learning
11 octobre 2016	TP3 : chacun présente son code au reste du groupe - discussion A faire pour la fois suivante : tester le sat solveur avec la nouvelle procédure de test - ajouter des optims (learning ou 2-watch literal)
18 octobre 2016	Rappel sur la logique du premier ordre Arithmétique linéaire sur les réels Fourier Motzkin Combiner SAT et Fourier Motzkin Panorama about reasoning about numbers Théorie des réels
25 octobre 2016	Omega test Fonctions non-interprétées et égalité : cloture par congruence functions and equality Combinaison de théories Discussions. Motivation pourl'interpolation
	VACANCES (pas de séances le mardi 1er novembre 2016)
mardi 8 novembre 2016	TP4 : le développement devient collaboratif uniquement - discussion sur l'architecture d'un petit SMT solveur (comment tester les sous-modules, répartition des charges, planning)
	PAS DE SEANCE le mardi 15 novembre 2016
mardi 22 novembre 2016	Combinaison de théories (suite) Interpolation de Craig Algorithme non-déterministe (Nelson-Oppen) Preuve de correction de Nelson-Oppen lorsque les théories sont stablement infinies Algorithme déterministe pour les théories convexes (Nelson-Oppen)
mardi 29 novembre 2016	TP5 : discussion sur l'avancement du SMT
mardi 6 décembre 2016	TP6 : présentation oral du projet
jeudi 15 décembre 2016, 14h à 16h, salle I50	Examen sur table

References

• Sipser, M. (2012). Introduction to the Theory of Computation. Cengage Learning.
• Dasgupta, S., Papadimitriou, C. H., & Vazirani, U. (2006). Algorithms. McGraw-Hill, Inc.
• Kroening, D., & Strichman, O. (2008). Decision procedures (Vol. 5). Heidelberg: Springer.
• van Emde Boas, P. (1997). The convenience of tilings. Lecture Notes in Pure and Applied Mathematics, 331-363.