Model Checking with SAT and SMT Course
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.
By completing this course, you will learn how to:
Describe the core principles of Propositional Satisfiability and Satisfiability Modulo Theories, including key techniques used for efficient solving
Explain an encoding method to translate Boolean circuits into Conjunctive Normal Form (CNF)
Describe bounded model checking of transition systems using SAT or SMT
Describe techniques to complement SAT-based bound model checking to make it complete
This specialization 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 MS-ECE is an affordable, global master's program powered by you. Learn more about the MS-ECE program.