Steffan Christ Sølvsten: Decision Diagrams in External Memory


Event Details


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.