HOME       UP       PREV       FURTHER NOTES       NEXT (ABD - Boolean Equivalence Checker)  

ABD - A Simple Model Checker

Formal checker for a state safety property:

Algorithm: 'Find reachable state space': Add successors of current set until closure.

S can be held explicitly in bit map form or symbolically as a BDD.

Variation: property to check might be a path property, so either

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.