> Formation > Cursus ingénieur
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.
Basic mathematical logic: Boolean operators, quantifiersAlgorithmicsProgramming
Small practical development work + written final exam
70% exam at the end of the course30% practical assignment
The exam is given in english only
The course exists in the following branches:
Course ID : WMM9MO46Course language(s):
You can find this course among all other courses.
Kroening & Strichman, Decision proceduresBradley & Manna, The calculus of computationBiere et al, ed., The Handbook of Satisfiability
Date of update March 10, 2020