Model Checking with SAT and SMT

Overview

This course introduces the fundamentals of model checking techniques based on using SAT (Propositional Satisfiability) solving and SMT (Satisfiability Modulo Theories) solving. You will learn basic concepts of propositional SAT solving, including conflict-driven clause learning (CDCL), proof methods, and theory-specific solvers, and concepts of encoding a model checking problem as a SAT solving problem. Topics include introduction to modern propositional SAT solving techniques, encoding Boolean circuits to Conjunctive Normal Form (CNF), bounded and unbounded model checking, and basic introduction to SMT solving. This course is Ideal for those seeking to understand SAT-based model checking and apply it in practical scenarios. This course can be taken for academic credit as part of CU Boulder’s Master of Science in Electrical and Computer Engineering (MS-ECE) degree offered on the Coursera platform. The degree offers targeted courses, short 8-week sessions, and pay-as-you-go tuition. Admission is based on performance in three preliminary courses, not academic history. CU degrees on Coursera are ideal for recent graduates or working professionals. Learn more: MS in Electrical and Computer Engineering: https://www.coursera.org/degrees/msee-boulder

Syllabus

Propositional Satisfiability (SAT)

This module introduces basic concepts and core techniques and procedures within modern propositional satisfiability solving, including resolution, Conflict-Driven Clause Learning (CDCL), Fast Deduction, and some features of SAT useful for problem solving. By examining these strategies, students will gain a foundational understanding of how modern SAT solvers analyze, deduce, and verify propositional formulae. Each lesson builds on practical examples to demonstrate how these methods contribute to modern SAT solver efficiency, reliability, and scalability.

SAT-Based Model Checking

This module dives into SAT-based model checking techniques. Lessons cover basic concepts of bounded model checking including bounded encodings of models and LTL formulas, and methods to complement BMC to make it complete.

Introduction to Satisfiability Modulo Theories (SMT)

This module introduces the fundamental concepts and techniques of Satisfiability Modulo Theories (SMT), an extension of satisfiability solving to more expressive logical domains such as Integer Difference Logic (IDL) and Equality with Uninterpreted Functions (EUF). It also covers methods for combining different theories, including the Nelson-Oppen procedure used in SMT solving. The lessons emphasize how SMT solvers handle diverse theories to efficiently solve complex logical and mathematical problems.