Volumes horaires
- CM 18.0
- Projet -
- TD -
- Stage -
- TP -
- DS -
Crédits ECTS
Crédits ECTS 3.0
Objectif(s)
Acquérir la théorie et la pratique des procédures de décision SAT (satisfiabilité booléenne) et SMT (enrichies avec des théories: arithmétique entière, rationnelle, etc.).
Ces procédures sont utilisables aussi bien en analyse automatique de logiciels et matériels qu'en optimisation combinatoire ou recherche de solutions en recherche opérationelle.
Responsable(s)
David MONNIAUX
Contenu(s)
- Bases de logique
- Algorithmique SAT: DPLL, CDCL
- Algorithmique BDD (binary decision diagrams)
- Algorithmique SMT (satisfiability modulo theory)
- Travaux pratiques: utilisation d'un SMT-solveur
Logique mathématique de base: opérateurs logiques, quantificateurs
Algorithmique
Programmation
Contrôle des connaissances
Mini-projet + examen écrit
70% exam at the end of the course
30% practical assignment
L'examen existe uniquement en anglais 
Calendrier
Le cours est programmé dans ces filières :
- Cursus ingénieur - Master Informatique - Semestre 9 (ce cours est donné uniquement en anglais
)
Informations complémentaires
Code de l'enseignement : WMM9MO46
Langue(s) d'enseignement :
Vous pouvez retrouver ce cours dans la liste de tous les cours.
Bibliographie
Kroening & Strichman, Decision procedures
Bradley & Manna, The calculus of computation
Biere et al, ed., The Handbook of Satisfiability