Monthly Subscription Starting at AED 99 + VAT

Automated Reasoning: Symbolic Model Checking
  • Level Professional
  • Duration 13 hours
  • Course by EIT Digital
  • Offered by

About

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. Typically, a state space may be very large. One way to deal with this is symbolic model checking: a way in which sets of states are represented symbolically. A fruitful way to do so is by representing sets of states by BDDs (binary decision diagrams). Definitions and basic properties of BDDs are presented in this course, and also algorithms to compute them, as they are needed for doing CTL model checking.

Modules

General introduction

    • 1 Videos
Show info about module content

1 Videos

  • General introduction

Model Checking

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Size of state space

1 Videos

  • Model Checking

Computation Tree Logic

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • CTL equivalence

1 Videos

  • Computation Tree Logic

Computation Tree Logic Algorithm

    • 1 Videos
Show info about module content

1 Videos

  • Computation Tree Logic Algorithm

Computation Tree Logic Example

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • CTL example

1 Videos

  • Computation Tree Logic Example

Representing Boolean Functions

    • 1 Videos
Show info about module content

1 Videos

  • Representing Boolean Functions

Decision Trees

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Decision tree

1 Videos

  • Decision Trees

Decision Trees 2

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Reduced ordered decision tree

1 Videos

  • Decision Trees 2

BDDs

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • ROBDD

1 Videos

  • BDDs

BDD Examples

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • BDD quiz 1
  • BDD quiz 2

1 Videos

  • BDD Examples

BDD Algorithm

    • 1 Videos
Show info about module content

1 Videos

  • BDD Algorithm

BDD Algorithm 2

    • 1 Videos
Show info about module content

1 Videos

  • BDD algorithm 2

BDD Algorithm Example

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • BDD algorithm

1 Videos

  • BDD Algorithm Example

BDD Algorithm CTL

    • 1 Videos
Show info about module content

1 Videos

  • BDD Algorithm CTL

An example: foxes and rabbits

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • An example: foxes and rabbits

1 Readings

  • NuSMV source of foxes and rabbits problem

Deadlock checking in a network

    • 1 Videos
Show info about module content

1 Videos

  • Deadlock checking in a network

Networks, BMC, conclusions

    • 1 Videos
Show info about module content

1 Videos

  • Networks, BMC, conclusions

Practical assignment

    • 2 Readings
    • 3 Assignment
Show info about module content

3 Assignment

  • Problem 1: colored marbles
  • Problem 2: reaching equal values
  • Problem 3: deadlocks in packet switching networks

2 Readings

  • Introduction
  • Explanation packet switching networks and file describing routing function

Auto Summary

Explore the Automated Reasoning: Symbolic Model Checking course, designed for professionals in IT & Computer Science. Learn to automatically verify system properties using symbolic model checking and BDDs. Taught by Coursera, this comprehensive 780-minute course offers Starter and Professional subscription options. Ideal for those seeking advanced skills in computational logic and verification.

Hans Zantema
Instructor

Hans Zantema