During the past five years, we’ve been developing yet another implementation of Binary Decision Diagrams (BDDs). What sets our implementation apart from others is its non-recursive algorithms. This allows it to efficiently compute on BDDs larger than the RAM of your machine – this potentially pushes the limits of symbolic model checking.
In this talk, I will show how to process BDDs that are so large that they have to be stored on the disk. Furthermore, I will provide an overview of the additional work and research results needed to make this algorithmic approach usable in practice.