Diplômes intégrant cet élément pédagogique :
Descriptif
Understanding how decision procedures for SAT (Boolean satisfiability) and SMT (SAT enriched with arithmetic etc.) work, and how to use them in practice.
These procedures can be used in automatic analysis of software or hardware, in combinatorial optimisation or in search for solutions in operation research.
Contents :
- SAT/SMT algorithms
- Lab classes: using a SMT solver
Pré-requis recommandés
Basic mathematical logic : Boolean operators, quantifiers
Algorithmics
Programming
Bibliographie
Kroening & Strichman, Decision procedures
Bradley & Manna, The calculus of computation
Biere et al, ed., The Handbook of Satisfiability
Informations complémentaires
Méthode d'enseignement : En présenceLangue(s) : Anglais
En bref
Période : Semestre 9Crédits : 3
Volume horaire
- TD : 18h
Contact(s)
Responsable pédagogique
David Monniaux
Etudiants internationaux
Ouvert aux étudiants en échange
Crédits : 3.0
Crédits : 3.0