Lectures
This page gives highlights of past lectures and links to lecture notes.
Tópico 01 - SAT solving
- 25 Sep
- Course Introduction
- An SMT problem. How does cvc5 solve it? What are the reasoning components in the solver?
- 30 Sep
- Propositional Logic
- 2 Oct
- Clausification and Resolution
- 7 Oct
- DPLL and CDCL
- 9 Oct
- Efficient SAT solving
Tópico 02 - SMT solving basics
- 14 Oct
- First-order Logic
- 16 Oct
- From SAT to SMT solving
- 21 Oct
- Laboratory: SMT introduction
Tópico 03 - Theory Solvers
- 23 Oct
- Theoly Solvers: EUF
- 04 Nov
- Theory Solvers: Difference Logic, Arrays
- 06, 11 Nov
- Theory Solvers: Linear Arithmetic
- 13 Nov
- Theory Solvers: Bit-vectors
- 18 Nov
- Exam 1
- 20 Nov
- No class (holiday)
Tópico 03 - Theory Solvers
- 25, 27 Oct, 2 Nov
- Quantifiers in SMT
- 4 Nov
- : Laboratory: SMT theory solvers