CS-E3220: SMT — Satisfiability Modulo Theories

These are the lecture notes for the rounds 9 (Part I) and 10 (Part II) in the Aalto University course CS-E3220 Declarative Programming organized in Autumn \(2020\).

Note: the Part III is not included in the course material in Autumn 2020 but is only included here as an extra material for the interested reader.

The lecture notes and slides for other rounds are given elsewhere, please see the MyCourses page of the course.

Contents:

• Part I: Basic Definitions
  • Many-Sorted First-Order Logic
  • Some Theories and Logics
  • Practical Use: Formats and Tools
  • Some tutorial papers on SMT
• Part II: Solving Satisfiability of Quantifier-Free Formulas
  • The Eager Approach
  • The Lazy Approach CDCL(T)
  • A Theory Solver for Equality with Uninterpreted Functions
  • A Theory Solver for Difference Logic
  • Theory Solvers for Other Theories
• Part III: Some further topics (NOT INCLUDED IN THE AUTUMN 2020 VERSION)
  • Theory Combination
  • Quantified Formulas

Indices and tables

• Index

• Module Index

• Search Page