Model Checking with SAT and SMT

Seize the savings! Get 40% off 3 months of Coursera Plus and full access to thousands of courses.

Model Checking with SAT and SMT

Instructor: Hao Zheng

Included with

Learn more

3 modules

Gain insight into a topic and learn the fundamentals.

Beginner level

Recommended experience

1 week to complete

at 10 hours a week

Flexible schedule

Learn at your own pace

3 modules

Gain insight into a topic and learn the fundamentals.

Beginner level

Recommended experience

1 week to complete

at 10 hours a week

Flexible schedule

Learn at your own pace

What you'll learn

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

Skills you'll gain

Details to know

Shareable certificate

Add to your LinkedIn profile

See how employees at top companies are mastering in-demand skills

Learn more about Coursera for Business

logos of Petrobras, TATA, Danone, Capgemini, P&G and L'Oreal

There are 3 modules in this 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.

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

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.

What's included

16 videos3 readings3 assignments

16 videos Total 125 minutes

Introduction to Boolean Satisfiability Problem 9 minutes
Conjunctive Normal Form (CNF) 7 minutes
Basic Concepts of Resolution 11 minutes
Finding Satisfying Assignments 11 minutes
Introduction to the CDCL Algorithm 10 minutes
Overview of CDCL Algorithm 8 minutes
CDCL Illustration 11 minutes
Learned Clause Minimization 7 minutes
Fast Deduction - Introduction 5 minutes
Two Matched Literals 6 minutes
Computing UNSAT Cores: Part 1 6 minutes
Computing UNSAT Cores: Part 2 6 minutes
Enumerating Satisfying Assignments: Part 1 7 minutes
Enumerating Satisfying Assignments: Part 2 4 minutes
Enumerating Satisfying Assignments: Part 3 6 minutes
Tseitin's Transformation 13 minutes

3 readings Total 21 minutes

Course Updates and Accessibility Support 1 minute
Non-Credit Students: Welcome and Where to Find Help 10 minutes
Supplemental Reading 10 minutes

3 assignments Total 45 minutes

Motivation of Verification 15 minutes
Formal Verification and Model Checking 15 minutes
SAT-based Problem Solving 15 minutes

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.

What's included

12 videos1 reading3 assignments

12 videos Total 121 minutes

Introduction to Bounded Model Checking 11 minutes
Basic BMC Workflow 8 minutes
Symbolic Representation of Transition Systems: Refreshment 9 minutes
Symbolic Encoding of BMC 7 minutes
Example of Symbolic BMC 9 minutes
Bounded LTL Semantics Without a Loop 17 minutes
Encoding of LTL on Bounded Path Without a Loop 7 minutes
Encoding of LTL on Bounded Path With a Loop 14 minutes
Completeness Thresholds 9 minutes
Inductive Invariants and K-Induction 10 minutes
Interpolation-Based Model Checking 9 minutes
Preimage Computation Using SAT Enumeration 9 minutes

1 reading Total 45 minutes

Supplemental Reading 45 minutes

3 assignments Total 45 minutes

Bounded Model Checking 15 minutes
LTL for Bounded Model Checking 15 minutes
Completeness for Bounded Model Checking 15 minutes

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.

What's included

18 videos1 reading4 assignments

18 videos Total 118 minutes

Introduction to SMT Solving 4 minutes
Approaches to SMT Solving 8 minutes
Generic Architecture of Lazy SMT Solving 4 minutes
Example of SMT Solving 6 minutes
Features of Lazy SMT Solving 7 minutes
Introduction to SMT Solver Z3 8 minutes
An Example of Bounded Model Checking Using Z3 20 minutes
Introduction to Integer Difference Logic 8 minutes
Example: Integer Difference Logic 5 minutes
Introduction to Linear Integer Arithmetic 8 minutes
Example: Linear Integer Arithmetic 7 minutes
Introduction to Equality and Uninterpreted Functions 6 minutes
EUF Theory Solving 5 minutes
Introduction to Theory of Arrays 5 minutes
Example: Introduction to Theory of Arrays 2 minutes
Introduction to Combining Theories 6 minutes
Applying Nelson-Oppen to Combined Theories 4 minutes
Practical Considerations and Optimizations 6 minutes

1 reading Total 10 minutes

Supplemental Reading 10 minutes

4 assignments Total 60 minutes

Satisfiability Modulo Theories 15 minutes
Linear Integer Arithmetic 15 minutes
Theory of Equality and Uninterpreted Functions 15 minutes
Combination of Theories 15 minutes

Instructor

Hao Zheng

University of Colorado Boulder

3 Courses 773 learners

Offered by

University of Colorado Boulder

Explore more from Algorithms

Status: Free Trial
University of Colorado Boulder
Temporal Logic Model Checking
Course
Status: Free Trial
University of Colorado Boulder
Introduction to Modeling for Formal Verification
Course
28DIGITAL
Automated Reasoning: satisfiability
Course
Status: Free Trial
University of Colorado Boulder
Fundamentals of Model Checking
Specialization

Why people choose Coursera for their career

Felipe M.

Learner since 2018

"To be able to take courses at my own pace and rhythm has been an amazing experience. I can learn whenever it fits my schedule and mood."

Jennifer J.

Learner since 2020

"I directly applied the concepts and skills I learned from my courses to an exciting new project at work."

Larry W.

Learner since 2021

"When I need courses on topics that my university doesn't offer, Coursera is one of the best places to go."

Chaitanya A.

"Learning isn't just about being better at your job: it's so much more than that. Coursera allows me to learn without limits."

Open new doors with Coursera Plus

Unlimited access to 10,000+ world-class courses, hands-on projects, and job-ready certificate programs - all included in your subscription

Learn more

Advance your career with an online degree

Earn a degree from world-class universities - 100% online

Explore degrees

Join over 3,400 global companies that choose Coursera for Business

Upskill your employees to excel in the digital economy

Learn more

Frequently asked questions

To access the course materials, assignments and to earn a Certificate, you will need to purchase the Certificate experience when you enroll in a course. You can try a Free Trial instead, or apply for Financial Aid. The course may offer 'Full Course, No Certificate' instead. This option lets you see all course materials, submit required assessments, and get a final grade. This also means that you will not be able to purchase a Certificate experience.

When you purchase a Certificate you get access to all course materials, including graded assignments. Upon completing the course, your electronic Certificate will be added to your Accomplishments page - from there, you can print your Certificate or add it to your LinkedIn profile.

Yes. In select learning programs, you can apply for financial aid or a scholarship if you can’t afford the enrollment fee. If fin aid or scholarship is available for your learning program selection, you’ll find a link to apply on the description page.