# Theory and Practice of SMT Solving

Course given by DCC-UFMG

- Syllabus
- Instructor:
- Haniel Barbosa, Office 4323, DCC, hbarbosa@dcc.ufmg.br

## Outline

A deep dive into how SMT solvers work.

There is no required textbook for the course. We will use a variety of reading materials which will be linked from the lecture notes. That said, the following books provide important background:

- H.B. Enderton. A Mathematical Introduction to Logic (Second Edition), Academic Press.
- D. Kroening, O. Strichman. Decision Procedures, Springer.
- A. Bradley, Z. Manna. The Calculus of Computation, Springer-Verlag.
- A. Biere, M. Heule, H. van Maaren, T. Walsh. Handbook of Satisfiability (Second Edition), IOS Press.