Bddl: A Type System for Binary Decision Diagrams

Binary Decision Diagrams (BDDs) are compact data structures used to efficiently store and process boolean functions. BDDs have many uses, from system design to model checking to efficiently storing context information for context-sensitive analysis. The use of BDDs in verification and program analysis has been facilitated by the recent emergence of many open source BDD libraries. The correctness of BDD-based system design and verification hinges upon the correctness of the BDD library implementations, and the correct use of these libraries. Surprisingly, for a technology so prevalent in system design and formal verification, there has been little research effort on formally verifying the correctness of BDD library implementations or their use. For BDD libraries that do perform some correctness checks, these are mostly confined to runtime assertion checking, which slows down BDD operations and might still be unable to reveal errors until deployment. To address these issues and take a step toward provably correct, yet efficient, BDD-handling code, we propose a formal system called Bddl to describe, reason about, and prove the correctness of BDD operations. Bddl extends lambda calculus with support for BDD operations (e.g., creation, manipulation), expressing BDD structural properties (e.g., canonicity, proper ordering), and BDD semantics (e.g., sets, relations). Bddl uses a type system based on refinement types to statically check BDD manipulation. We have proved our system correct using a small-step semantics and standard notions of progress and preservation. Bddl is the first attempt to provide a well-defined syntax and semantics to BDD operations; we show how it could prevent bugs and semantic errors in the implementation and use of three mature DD libraries.