SAT/SMT Solving - WMM9MO46
A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail
Objectifs
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.
Contenu - Bases de logique
- Algorithmique SAT: DPLL, CDCL
- Algorithmique BDD (binary decision diagrams)
- Algorithmique SMT (satisfiability modulo theory)
- Travaux pratiques: utilisation d'un SMT-solveur
PrérequisLogique mathématique de base: opérateurs logiques, quantificateurs
Algorithmique
Programmation
Contrôles 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
)
cf.
l'emploi du temps 2022/2023
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
A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail
mise à jour le 10 mars 2020