Binary Decision Diagram (BDD) based symbolic model checking is capable of verifying systems with a large number of states. Its effectiveness was evidenced by the recent success of the Intel i7 project, where BDD techniques have been applied to verify the i7 processor. We have developed a BDD library which is designed to facilitate application of BDD techniques to fully hierarchical systems. Below are many features in our library:

Our papers: Technical Reports: Benchmarks and Experiment Results

Download PAT model checker here

Download PAT.BDD Library:

Library Manual: manual.pdf

Contact: Nguyen Truong Khanh