Advanced Topics in Informatics
Satisfiability Modulo Theory
Spezielle Kapitel in Informatik (3KV)
Summer Semester 2014
OverviewSMT (Satisfiability Modulo Theories) extends logic formulas by theories of various kinds. Examples of such theories are integer arithmetic, bit vectors, arrays, etc. On this basis, many SMT solvers have been implemented which are successfully used in applications like verification, testing, program analysis and scheduling.
This lecture is about algorithms for SMT and their practical implementation.