Software and Computational Systems Lab

Publications about BDD

1. Dirk Beyer, Karlheinz Friedberger, and Stephan Holzner. PJBDD: A BDD Library for Java and Multi-Threading. In Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21 2021, Gold Coast (Online), Australia, October 18-22), 2021. Springer. doi:10.1007/978-3-030-88885-5_10 Keyword(s): PJBDD, BDD Funding: DFG-CONVEY Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.5070156
   Abstract

   PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.
   BibTeX Entry

   @inproceedings{ATVA21, author = {Dirk Beyer and Karlheinz Friedberger and Stephan Holzner}, title = {{PJBDD}: {A} {BDD} Library for {Java} and Multi-Threading}, booktitle = {Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21~2021, Gold Coast (Online), Australia, October 18-22)}, year = {2021}, publisher = {Springer}, doi = {10.1007/978-3-030-88885-5_10}, pdf = {https://www.sosy-lab.org/research/pub/2021-ATVA.PJBDD_A_BDD_Library_for_Java_and_Multi_Threading.pdf}, abstract = {PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.}, keyword = {PJBDD,BDD}, artifact = {10.5281/zenodo.5070156}, funding = {DFG-CONVEY}, }

1. Simon Raths. Implementation and Evaluation of TBDDs in PJBDD. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): BDD
   BibTeX Entry

   @misc{RathsTBDD, author = {Simon Raths}, title = {Implementation and Evaluation of TBDDs in PJBDD}, year = {2021}, keyword = {BDD}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
2. Stephan Holzner. Design und Implementierung einer parallelen BDD-Bibliothek. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): BDD, Software Model Checking PDF
   BibTeX Entry

   @misc{HolznerParallelBDD, author = {Stephan Holzner}, title = {{Design und Implementierung einer parallelen BDD-Bibliothek}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/msc/2019.Holzner.Design_und_Implementierung_einer_parallelen_BDD-Bibliothek.pdf}, keyword = {BDD,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }