UE SAT / SMT solving

User information

Please note that you are curently looking at the ongoing Academic Programs. Applications are now closed for this academic year (2020-2021) for licences, professional licences, masters, DUT and regulated health training. If you are interested for an application in 2021-2022, please click on this link for the appropriate Academic Programs.

Degrees incorporating this pedagocial element :

Description

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

Recommended prerequisite

  • Basic mathematical logic : Boolean operators, quantifiers
  • Algorithmics
  • Programming