Model Checking with SAT and SMT

Économisez sur les compétences qui vous font briller avec 40 % de réduction sur 3 mois de Coursera Plus. Économisez maintenant

Ce cours n'est pas disponible en Français (France)

Nous sommes actuellement en train de le traduire dans plus de langues.

Model Checking with SAT and SMT

Instructeur : Hao Zheng

Inclus avec

3 modules

Obtenez un aperçu d'un sujet et apprenez les principes fondamentaux.

niveau Débutant

Expérience recommandée

1 semaine à compléter

à 10 heures par semaine

Planning flexible

Apprenez à votre propre rythme

3 modules

Obtenez un aperçu d'un sujet et apprenez les principes fondamentaux.

niveau Débutant

Expérience recommandée

1 semaine à compléter

à 10 heures par semaine

Planning flexible

Apprenez à votre propre rythme

Ce que vous apprendrez

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

Compétences que vous acquerrez

Catégorie : Graph Theory

Détails à connaître

Certificat partageable

Ajouter à votre profil LinkedIn

Récemment mis à jour !

novembre 2025

Évaluations

10 devoirs

Enseigné en Anglais

91% of learners achieved a positive career outcome

Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées

En savoir plus sur Coursera pour les affaires

logos de Petrobras, TATA, Danone, Capgemini, P&G et L'Oreal

Il y a 3 modules dans ce cours

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.

Inclus

16 vidéos3 lectures3 devoirs

16 vidéosTotal 125 minutes

Introduction to Boolean Satisfiability Problem9 minutes
Conjunctive Normal Form (CNF)7 minutes
Basic Concepts of Resolution11 minutes
Finding Satisfying Assignments11 minutes
Introduction to the CDCL Algorithm10 minutes
Overview of CDCL Algorithm8 minutes
CDCL Illustration11 minutes
Learned Clause Minimization7 minutes
Fast Deduction - Introduction5 minutes
Two Matched Literals6 minutes
Computing UNSAT Cores: Part 16 minutes
Computing UNSAT Cores: Part 2 6 minutes
Enumerating Satisfying Assignments: Part 17 minutes
Enumerating Satisfying Assignments: Part 24 minutes
Enumerating Satisfying Assignments: Part 36 minutes
Tseitin's Transformation13 minutes

3 lecturesTotal 21 minutes

Course Updates and Accessibility Support1 minute
Non-Credit Students: Welcome and Where to Find Help10 minutes
Supplemental Reading10 minutes

3 devoirsTotal 45 minutes

Motivation of Verification15 minutes
Formal Verification and Model Checking15 minutes
SAT-based Problem Solving15 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.

Inclus

12 vidéos1 lecture3 devoirs

12 vidéosTotal 121 minutes

Introduction to Bounded Model Checking11 minutes
Basic BMC Workflow8 minutes
Symbolic Representation of Transition Systems: Refreshment9 minutes
Symbolic Encoding of BMC7 minutes
Example of Symbolic BMC9 minutes
Bounded LTL Semantics Without a Loop17 minutes
Encoding of LTL on Bounded Path Without a Loop7 minutes
Encoding of LTL on Bounded Path With a Loop14 minutes
Completeness Thresholds9 minutes
Inductive Invariants and K-Induction10 minutes
Interpolation-Based Model Checking9 minutes
Preimage Computation Using SAT Enumeration9 minutes

1 lectureTotal 45 minutes

Supplemental Reading45 minutes

3 devoirsTotal 45 minutes

Bounded Model Checking15 minutes
LTL for Bounded Model Checking15 minutes
Completeness for Bounded Model Checking15 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.

Inclus

18 vidéos1 lecture4 devoirs

18 vidéosTotal 118 minutes

Introduction to SMT Solving4 minutes
Approaches to SMT Solving8 minutes
Generic Architecture of Lazy SMT Solving4 minutes
Example of SMT Solving6 minutes
Features of Lazy SMT Solving7 minutes
Introduction to SMT Solver Z38 minutes
An Example of Bounded Model Checking Using Z320 minutes
Introduction to Integer Difference Logic8 minutes
Example: Integer Difference Logic5 minutes
Introduction to Linear Integer Arithmetic 8 minutes
Example: Linear Integer Arithmetic 7 minutes
Introduction to Equality and Uninterpreted Functions6 minutes
EUF Theory Solving5 minutes
Introduction to Theory of Arrays5 minutes
Example: Introduction to Theory of Arrays2 minutes
Introduction to Combining Theories6 minutes
Applying Nelson-Oppen to Combined Theories4 minutes
Practical Considerations and Optimizations6 minutes

1 lectureTotal 10 minutes

Supplemental Reading10 minutes

4 devoirsTotal 60 minutes

Satisfiability Modulo Theories15 minutes
Linear Integer Arithmetic15 minutes
Theory of Equality and Uninterpreted Functions15 minutes
Combination of Theories15 minutes

Instructeur

Hao Zheng

University of Colorado Boulder

3 Cours937 apprenants

Offert par

University of Colorado Boulder

En savoir plus sur Algorithms

University of Colorado Boulder
Temporal Logic Model Checking
Cours
University of Colorado Boulder
Introduction to Modeling for Formal Verification
Cours
28DIGITAL
Automated Reasoning: satisfiability
Cours
University of Colorado Boulder
Fundamentals of Model Checking
Spécialisation

Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?

Felipe M.

Étudiant(e) depuis 2018

’Pouvoir suivre des cours à mon rythme à été une expérience extraordinaire. Je peux apprendre chaque fois que mon emploi du temps me le permet et en fonction de mon humeur.’

Jennifer J.

Étudiant(e) depuis 2020

’J'ai directement appliqué les concepts et les compétences que j'ai appris de mes cours à un nouveau projet passionnant au travail.’

Larry W.

Étudiant(e) depuis 2021

’Lorsque j'ai besoin de cours sur des sujets que mon université ne propose pas, Coursera est l'un des meilleurs endroits où se rendre.’

Chaitanya A.

’Apprendre, ce n'est pas seulement s'améliorer dans son travail : c'est bien plus que cela. Coursera me permet d'apprendre sans limites.’

Foire Aux 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.

Plus de questions

Visitez le Centre d'Aide pour les Étudiants

Aide financière disponible,