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.
Model Checking with SAT and SMT
noch 3 Tage: Holen Sie sich einen Black Friday Boost mit $160 Rabatt auf 10.000+ Programme.Sparen Sie jetzt.
Verschaffen Sie sich einen Einblick in ein Thema und lernen Sie die Grundlagen.
Stufe Anfänger
Empfohlene Erfahrung
9 Stunden zu vervollständigen
Flexibler Zeitplan
In Ihrem eigenen Lerntempo lernen
Was Sie lernen werden
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
Kompetenzen, die Sie erwerben
- Kategorie: Program Development
- Kategorie: Test Case
- Kategorie: Deductive Reasoning
Wichtige Details
Zertifikat zur Vorlage
Zu Ihrem LinkedIn-Profil hinzufügen
Kürzlich aktualisiert!
November 2025
Bewertungen
10 Aufgaben
Unterrichtet in Englisch
Erfahren Sie, wie Mitarbeiter führender Unternehmen gefragte Kompetenzen erwerben.
In diesem Kurs gibt es 3 Module
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.
Das ist alles enthalten
16 Videos2 Lektüren3 Aufgaben
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.
Das ist alles enthalten
12 Videos1 Lektüre3 Aufgaben
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.
Das ist alles enthalten
18 Videos1 Lektüre4 Aufgaben
Dozent
Mehr von Algorithms entdecken
University of Colorado Boulder
EIT Digital
University of Colorado Boulder
EIT Digital
Warum entscheiden sich Menschen für Coursera für ihre Karriere?
Felipe M.
Lernender seit 2018
„Es ist eine großartige Erfahrung, in meinem eigenen Tempo zu lernen. Ich kann lernen, wenn ich Zeit und Nerven dazu habe.“
Jennifer J.
Lernender seit 2020
„Bei einem spannenden neuen Projekt konnte ich die neuen Kenntnisse und Kompetenzen aus den Kursen direkt bei der Arbeit anwenden.“
Larry W.
Lernender seit 2021
„Wenn mir Kurse zu Themen fehlen, die meine Universität nicht anbietet, ist Coursera mit die beste Alternative.“
Chaitanya A.
„Man lernt nicht nur, um bei der Arbeit besser zu werden. Es geht noch um viel mehr. Bei Coursera kann ich ohne Grenzen lernen.“
Neue Karrieremöglichkeiten mit Coursera Plus
Unbegrenzter Zugang zu 10,000+ Weltklasse-Kursen, praktischen Projekten und berufsqualifizierenden Zertifikatsprogrammen - alles in Ihrem Abonnement enthalten
Bringen Sie Ihre Karriere mit einem Online-Abschluss voran.
Erwerben Sie einen Abschluss von erstklassigen Universitäten – 100 % online
Schließen Sie sich mehr als 3.400 Unternehmen in aller Welt an, die sich für Coursera for Business entschieden haben.
Schulen Sie Ihre Mitarbeiter*innen, um sich in der digitalen Wirtschaft zu behaupten.
Häufig gestellte Fragen
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.
Weitere Fragen
Finanzielle Unterstützung verfügbar,