PAT.BDD Library's Homepage

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:

C# interface for CUDD package (version 2.4.2) and MTBDD
An easy-to-use interface for integer variables, array with variables in the index, logic and arithmetic expression, and some programming structure like While loop, If condition
BDD-based operations including pre-image, post-image, and many searching algorithms with variety settings.
Many compositional functions to get the encoding of a hierarchical system

Our papers:

Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong and Yan Liu. Improved BDD-based Discrete Analysis of Timed Systems. The 18th International Symposium on Formal Methods (FM 2012), Paris, France, Auguest 27 - 31, 2012.
Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. Symbolic Model-Checking of Stateful Timed CSP using BDD and Digitization. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), Kyoto, Japan, November 12 - 16, 2012.
Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. A Symbolic Model Checking Framework for Hierarchical Systems. The 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011), pages 633-636, Lawrence, Kan., USA, Nov 6 - 11, 2011.