Degrees incorporating this pedagocial element :
Description
A central ingredient in many methods for symbolic and concolic executions, for finding inductive invariants, and for checking their inductiveness, is _satisfiability modulo theory_ (SMT). SMT is based on Boolean satisfiability testing (SAT), that is, checking whether a propositional formula has a solution. There exist algorithms for solving SAT and many cases of SMT, but the issue here is computational complexity: SAT is a hard problem.
Understanding the main ideas in SAT/SMT algorithmics.
Recommended prerequisite
Knowledge in a programming language (Python, C++, OCaml…) to implement the project. Fluency with programming in general. Knowledge of first-order logic and basic mathematics.
Courses offered by :
In brief
Period : Semester 9Credits : 3
Number of hours
- Lectures (CM) : 18h
Language(s) : English
Contact(s)
Program director
David Monniaux
International students
Open to exchange students