UE SAT/SMT solving

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.

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.