Z3 Theorem Prover

Guest Lecture material at TU Wien October 2025

Lecture Overview

• Lecture 1 - introduction to SMT
• Lecture 2 - SMT search
• Lecture 3-4 - Theory Solvers
• Lecture 4-5 - Solving Arithmetic
• Lecture 6 - Programming Z3
• Lecture 7 - Combining Theory Solvers
• Lecture 8 - Quantifiers
• Lecture 9 - Optimization Modulo Theories
• Lecture 10 - Topics in SMT