Theory and Practice of SMT Solving
Course given by DCC-UFMG
- Syllabus
- Instructor:
- Haniel Barbosa, Office 4323, DCC, hbarbosa@dcc.ufmg.br
Outline
- Theory and Practice of SMT Solving
- Topic 1: SAT solving
- Topic 2: FOL and CDCL(T)
- Topic 3: Core theory solvers
- Topic 4: Quantifiers
- Topic 5: Proofs
- Topic 6: Theory solvers for BV and Strings
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.