Teaching Satisfiability Checking
Held by Erika Abraham in 14 May 2020 on Zoom
Abstract:
In this presentation I would like to give some insights into the contents, the teaching materials and the evaluation methods for my annual lecture for both Bachelor and Master students on satisfiability checking. Content wise, we deal with methods and tools for checking the satisfiability of (mostly quantifier-free) first-order logic formulas.
After propositional logic and some easier theories like equality logic and uninterpreted functions or array theory, the main focus lies on arithmetic theories for linear as well as non-linear integer and real arithmetic via SAT and SAT-modulo-theories (SMT) techniques.