Symbolic model checking
An Example
Checking invariants
Checking liveness
Finding bugs
Back to the tutorial pages