The Automated Reasoning: Symbolic Model Checking course presents how the properties of acting systems and programs can be verified automatically. The basic notion is a transition system: any system that can be described by states and steps. We present how in CTL (computation tree logic) properties like reach-ability can be described.
Automated Reasoning: Symbolic Model Checking
Automated Reasoning: Symbolic Model Checking
Instructor: Hans Zantema
Sponsored by Coursera Learning Team
2,714 already enrolled
Gain insight into a topic and learn the fundamentals.
4.7
(26 reviews)
Intermediate level
Recommended experience
13 hours to complete
3 weeks at 4 hours a week
Flexible schedule
Learn at your own pace
Skills you'll gain
Details to know
Shareable certificate
Add to your LinkedIn profile
Assessments
12 assignments
Taught in English
See how employees at top companies are mastering in-demand skills
Earn a career certificate
Add this credential to your LinkedIn profile, resume, or CV
Share it on social media and in your performance review
There are 4 modules in this course
After a general introduction to the MOOC, this module starts by a general description of model checking.Then Computation Tree Logic (CTL) is introduced: a language in which properties on transition systems can be described. The algorithm to check whether such a property holds is given in an abstract setting, leaving implicit how sets of states are represented.
What's included
5 videos3 assignments
In this module BDDs (binary decision diagrams) are introduced as decision trees with sharing. They represent boolean functions. Extra requirements on both decision trees and BDDs are presented from which uniqueness of the representation can be concluded.
What's included
4 videos3 assignments
After some examples of BDD, the algorithm is presented and discussed to compute the ROBDD of any propositional formula.
What's included
4 videos3 assignments
In this last module the topics of CTL model checking and BDDs are combined: it is shown how BDDs can be used to represent sets of states in a way that the abstract algorithm for CTL mode checking can be used, and much larger state spaces can be dealt with than by using explicit state based model checking. Sever examples are presented.
What's included
4 videos3 readings3 assignments
Instructor
Instructor ratings
5.0 (9 ratings)Offered by
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."
Recommended if you're interested in Computer Science
EIT Digital
EIT Digital
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
Advance your career with an online degree
Earn a degree from world-class universities - 100% online
Join over 3,400 global companies that choose Coursera for Business
Upskill your employees to excel in the digital economy