## Agile development of a theory solver for SMT

*Satisfiability Checking* is the task of checking the existence of a satisfying solution for a logical formula. For propositional logic formulas, being Boolean combinations of propositions such as , SAT solvers can be used to determine whether there is an assignment mapping to each proposition a value either *true* or *false*, such that substituting these values into the formula, the formula evaluates to *true*.

For the satisfiability check of quantifier-free first-order logic formulas over different *theories*, SAT solvers can be extended with theory solver modules, resulting in *SAT-modulo-theories (SMT) solvers*. Thereby we move from checking satisfiability for propositional logic formulas, such as , towards checking satisfiability for formulas such as . Such logics can be syntactically more rich as well as semantically more expressive than propositional logic, and allow the natural formalisation of a wide range of practical problems, e.g., in scheduling, planning, software verification, or controller synthesis. This practical course aims at the design, implementation, and optimization of state-of-the-art decision procedures for SMT solving for the theories of *equality logic and uninterpreted functions*. The practical course is organized to follow an agile development process.

The implementation will take place within the SMT-RAT project and can benefit from its manifold features. The resulting SMT solver will be tested on the official SMT-LIB benchmarks and be compared to state-of-the-art SMT solvers. Furthermore, we will form at least two teams and compare their solvers within a competition.

## Slides

## Tasks