This course presents how 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 reachability can be described.
Offered By


Automated Reasoning: Symbolic Model Checking
EIT DigitalAbout this Course
Flexible deadlines
Reset deadlines in accordance to your schedule.
Shareable Certificate
Earn a Certificate upon completion
100% online
Start instantly and learn at your own schedule.
Coursera Labs
Includes hands on learning projects.
Learn more about Coursera Labs Intermediate Level
Basic logic and programming on a bachelor level.
Approx. 13 hours to complete
English
Could your company benefit from training employees on in-demand skills?
Try Coursera for BusinessFlexible deadlines
Reset deadlines in accordance to your schedule.
Shareable Certificate
Earn a Certificate upon completion
100% online
Start instantly and learn at your own schedule.
Coursera Labs
Includes hands on learning projects.
Learn more about Coursera Labs Intermediate Level
Basic logic and programming on a bachelor level.
Approx. 13 hours to complete
English
Could your company benefit from training employees on in-demand skills?
Try Coursera for BusinessOffered by
Syllabus - What you will learn from this course
1 hour to complete
CTL model checking
1 hour to complete
5 videos (Total 44 min)
1 hour to complete
BDDs part 1
1 hour to complete
4 videos (Total 33 min)
2 hours to complete
BDDs part 2
2 hours to complete
4 videos (Total 35 min)
9 hours to complete
BDD based symbolic model checking
9 hours to complete
4 videos (Total 39 min), 3 readings, 3 quizzes
Frequently Asked Questions
When will I have access to the lectures and assignments?
What will I get if I purchase the Certificate?
What is the refund policy?
Is financial aid available?
More questions? Visit the Learner Help Center.