RWTH Aachen University, Germany
Title: SMT Solving for Arithmetic Theories: Theory and Tool Support
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. Driven by the impressive success of SAT solvers for propositional logic, SAT-modulo-theories (SMT) solvers were developed to extend the scope also to different theories.
In this tutorial we give a short introduction to the theoretical foundations of SMT solving, discuss SMT algorithms for checking the satisfiability of arithmetic formulas, and give an overview of available tools with a special focus on the SMT solver SMT-RAT.
Erika Abraham graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Currently she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.