Catalogue des formations

Diplômes intégrant cet élément pédagogique :

• Master Informatique

Descriptif

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.

Pré-requis recommandés

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.

Informations complémentaires

Langue(s) : Anglais