SAT/SMT Solving - WMM9MO46

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail

Volumes horaires
- CM : 18.0
- TD : -
- TP : -
- Projet : -
- Stage : -
- DS : -
Crédits ECTS : 3.0
Responsables : David MONNIAUX

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érequis

Logique 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

École nationale supérieure d'informatique et de mathématiques appliquées
681, rue de la passerelle - Domaine universitaire - BP 72
38402 SAINT MARTIN D'HERES

SAT/SMT Solving - WMM9MO46

Volumes horaires

Objectifs