{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:22:14Z","timestamp":1768285334164,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We follow up on the idea of Lars Arge to rephrase the Reduce and Apply operations of Binary Decision Diagrams (BDDs) as iterative I\/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone. We provide asymptotic improvements to the few procedures that can be derived using Apply.<\/jats:p><jats:p>Our work has culminated in a BDD package named Adiar that is able to efficiently manipulate BDDs that outgrow main memory. This makes Adiar surpass the limits of conventional BDD packages that use recursive depth-first algorithms. It is able to do so while still achieving a satisfactory performance compared to other BDD packages: Adiar, in parts using the disk, is on instances larger than 9.5\u00a0GiB only 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, Adiar is able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_16","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"295-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Adiar Binary Decision Diagrams in External Memory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0963-6569","authenticated-orcid":false,"given":"Steffan Christ","family":"S\u00f8lvsten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-0625","authenticated-orcid":false,"given":"Jaco van","family":"de Pol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna Blume","family":"Jakobsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias Weller Berg","family":"Thomasen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Aggarwal, A., Vitter, Jeffrey, S.: The input\/output complexity of sorting and related problems. Communications of the ACM 31(9), 1116\u20131127 (1988). https:\/\/doi.org\/10.1145\/48529.48535","DOI":"10.1145\/48529.48535"},{"key":"16_CR2","unstructured":"Amar\u00fa, L., Gaillardon, P.E., De\u00a0Micheli, G.: The EPFL combinational benchmark suite. In: 24th International Workshop on Logic & Synthesis (2015)"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Amparore, E., Donatelli, S., Gall\u00e0, F.: A CTL* model checker for Petri nets. In: Application and Theory of Petri Nets and Concurrency. Lecture Notes in Computer Science, vol. 12152, pp. 403\u2013413. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51831-8_21","DOI":"10.1007\/978-3-030-51831-8_21"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Arge, L.: The buffer tree: A new technique for optimal I\/O-algorithms. In: Workshop on Algorithms and Data Structures (WADS). Lecture Notes in Computer Science, vol.\u00a0955, pp. 334\u2013345. Springer, Berlin, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60220-8_74","DOI":"10.1007\/3-540-60220-8_74"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Arge, L.: The I\/O-complexity of ordered binary-decision diagram manipulation. In: 6th International Symposium on Algorithms and Computations (ISAAC). Lecture Notes in Computer Science, vol.\u00a01004, pp. 82\u201391 (1995). https:\/\/doi.org\/10.1007\/BFb0015411","DOI":"10.1007\/BFb0015411"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Arge, L.: The I\/O-complexity of ordered binary-decision diagram. In: BRICS RS preprint series. vol.\u00a029. Department of Computer Science, University of Aarhus (1996). https:\/\/doi.org\/10.7146\/brics.v3i29.20010","DOI":"10.7146\/brics.v3i29.20010"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Arge, L.: External geometric data structures. In: 10th International Computing and Combinatorics Conference (COCOON). Lecture Notes in Computer Science, vol.\u00a03106 (2004). https:\/\/doi.org\/10.1007\/978-3-540-27798-9_1","DOI":"10.1007\/978-3-540-27798-9_1"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Ashar, P., Cheong, M.: Efficient breadth-first manipulation of binary decision diagrams. In: IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). pp. 622\u2013627. IEEE Computer Society Press (1994). https:\/\/doi.org\/10.1109\/ICCAD.1994.629886","DOI":"10.1109\/ICCAD.1994.629886"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: 27th Design Automation Conference (DAC). pp. 40\u201345. Association for Computing Machinery (1990). https:\/\/doi.org\/10.1109\/DAC.1990.114826","DOI":"10.1109\/DAC.1990.114826"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","DOI":"10.1145\/136035.136043"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Binary decision diagrams. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 191\u2013217. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"16_CR13","unstructured":"Chen, J., Revels, J.: Robust benchmarking in noisy environments. arXiv (2016), https:\/\/arxiv.org\/abs\/1608.04295"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a02404, pp. 359\u2013364. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer 2, 410\u2013425 (2000). https:\/\/doi.org\/10.1007\/s100090050046","DOI":"10.1007\/s100090050046"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Van Dijk, T., Van de Pol, J.: Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer 19, 675\u2013696 (2016). https:\/\/doi.org\/10.1007\/s10009-016-0433-2","DOI":"10.1007\/s10009-016-0433-2"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Gammie, P., Van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a03114, pp. 479\u2013483. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_41","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"16_CR18","unstructured":"He, L., Liu, G.: Petri net based symbolic model checking for computation tree logic of knowledge. arXiv (2020), https:\/\/arxiv.org\/abs\/2012.10126"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Kant, G., Laarman, A., Meijer, J., Van de Pol, J., Blom, S., Van Dijk, T.: LTSmin: High-performance language-independent model checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol.\u00a09035, pp. 692\u2013707. Springer, Berlin, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"16_CR20","unstructured":"Karplus, K.: Representing Boolean functions with if-then-else DAGs. Tech. rep., University of California at Santa Cruz, USA (1988)"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Klarlund, N., Rauhe, T.: BDD algorithms and cache misses. In: BRICS Report Series. vol.\u00a026 (1996). https:\/\/doi.org\/10.7146\/brics.v3i26.20007","DOI":"10.7146\/brics.v3i26.20007"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Kunkle, D., Slavici, V., Cooperman, G.: Parallel disk-based computation for large, monolithic binary decision diagrams. In: 4th International Workshop on Parallel Symbolic Computation (PASCO). pp. 63\u201372 (2010). https:\/\/doi.org\/10.1145\/1837210.1837222","DOI":"10.1145\/1837210.1837222"},{"key":"16_CR23","unstructured":"Lind-Nielsen, J.: BuDDy: A binary decision diagram package. Tech. rep., Department of Information Technology, Technical University of Denmark (1999)"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer 19, 9\u201330 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","DOI":"10.1007\/s10009-015-0378-x"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Long, D.E.: The design of a cache-friendly BDD library. In: Proceedings of the 1998 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). pp. 639\u2013645. Association for Computing Machinery (1998)","DOI":"10.1145\/288548.289102"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Minato, S.i., Ishihara, S.: Streaming BDD manipulation for large-scale combinatorial problems. In: Design, Automation and Test in Europe Conference and Exhibition. pp. 702\u2013707 (2001). https:\/\/doi.org\/10.1109\/DATE.2001.915104","DOI":"10.1109\/DATE.2001.915104"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Minato, S.i., Ishiura, N., Yajima, S.: Shared binary decision diagram with attributed edges for efficient Boolean function manipulation. In: 27th Design Automation Conference (DAC). pp. 52\u201357. Association for Computing Machinery (1990). https:\/\/doi.org\/10.1145\/123186.123225","DOI":"10.1145\/123186.123225"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Ochi, H., Yasuoka, K., Yajima, S.: Breadth-first manipulation of very large binary-decision diagrams. In: International Conference on Computer Aided Design (ICCAD). pp. 48\u201355. IEEE Computer Society Press (1993). https:\/\/doi.org\/10.1109\/ICCAD.1993.580030","DOI":"10.1109\/ICCAD.1993.580030"},{"key":"16_CR29","unstructured":"Petersen, L.H.: External Priority Queues in Practice. Master\u2019s thesis, Department of Computer Science, University of Aarhus (2007)"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Sanders, P.: Fast priority queues for cached memory. ACM Journal of Experimental Algorithmics 5, 7\u201332 (2000). https:\/\/doi.org\/10.1145\/351827.384249","DOI":"10.1145\/351827.384249"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Sanghavi, J.V., Ranjan, R.K., Brayton, R.K., Sangiovanni-Vincentelli, A.: High performance BDD package by exploiting memory hierarchy. In: 33rd Design Automation Conference (DAC). pp. 635\u2013640. Association for Computing Machinery (1996). https:\/\/doi.org\/10.1145\/240518.240638","DOI":"10.1145\/240518.240638"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"S\u00f8lvsten, S.C., Van de Pol, J.: Adiar v1.0.1 : TACAS 2022 artifact. Zenodo (2021). https:\/\/doi.org\/10.5281\/zenodo.5638335","DOI":"10.5281\/zenodo.5638335"},{"key":"16_CR33","unstructured":"S\u00f8lvsten, S.C., Van de Pol, J., Jakobsen, A.B., Thomasen, M.W.B.: Efficient binary decision diagram manipulation in external memory. arXiv (2021), https:\/\/arxiv.org\/abs\/2104.12101"},{"key":"16_CR34","unstructured":"Somenzi, F.: CUDD: CU decision diagram package, 3.0. Tech. rep., University of Colorado at Boulder (2015)"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Velev, M.N., Gao, P.: Efficient parallel GPU algorithms for BDD manipulation. In: 19th Asia and South Pacific Design Automation Conference (ASP-DAC). pp. 750\u2013755. IEEE Computer Society Press (2014). https:\/\/doi.org\/10.1109\/ASPDAC.2014.6742980","DOI":"10.1109\/ASPDAC.2014.6742980"},{"key":"16_CR36","unstructured":"Vengroff, D.E.: A Transparent Parallel I\/O Environment. In: DAGS Symposium on Parallel Computation. pp. 117\u2013134 (1994)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:48:05Z","timestamp":1710233285000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}