Lectures
This page gives highlights of past lectures and links to lecture notes.
Topic 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
Topic 02 - SMT solving basics
- 14 Oct
- First-order Logic
- 16 Oct
- From SAT to SMT solving
- 21 Oct
- Laboratory: SMT introduction
Topic 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)
Topic 04 - Quantifiers
- 25, 27 Nov, 2 Dec
- Quantifiers in SMT
- 4 Dec
- Laboratory: SMT theory solvers
Topic 05 - Proofs
- Dec 9, 16
- Proofs
- Jan 8
- Laboratory: Proofs
- Jan 10
- Project check-ins
- Jan 15
- Exam 2
- Jan 20, 22, 27, 29
- Seminars