{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T11:54:09Z","timestamp":1777895649293,"version":"3.51.4"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_7","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"191-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":45,"title":["Binary Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"6","key":"7_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR2","series-title":"LNCS","first-page":"395","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Parker, G.N.D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01785, pp.\u00a0395\u2013410. Springer, Heidelberg (2000)"},{"key":"7_CR3","first-page":"443","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"F.A. Aloul","year":"2001","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Faster SAT and smaller BDDs via common function structure. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0443\u2013448. IEEE, Piscataway (2001)"},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR5","first-page":"622","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"P. Ashar","year":"1994","unstructured":"Ashar, P., Cheong, M.: Efficient breadth-first manipulation of binary decision diagrams. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0622\u2013627. IEEE, Piscataway (1994)"},{"key":"7_CR6","first-page":"283","volume-title":"Proc. of the 31st ACM\/IEEE Design Automation Conf. (DAC)","author":"A. Aziz","year":"1994","unstructured":"Aziz, A., Ta\u015firan, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: Proc. of the 31st ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0283\u2013288. ACM\/IEEE, New York\/Piscataway (1994)"},{"key":"7_CR7","first-page":"188","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"R.I. Bahar","year":"1993","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0188\u2013191. IEEE, Piscataway (1993)"},{"key":"7_CR8","volume-title":"Handbook of Model Checking","author":"C.W. Barrett","year":"2018","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"9","key":"7_CR9","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR10","first-page":"759","volume-title":"Proc. of the IMEC-IFIP Intl. Workshop on Applied Formal Methods for Correct VLSI Design","author":"S. Bose","year":"1989","unstructured":"Bose, S., Fisher, A.L.: Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic. In: Claesen, L. (ed.) Proc. of the IMEC-IFIP Intl. Workshop on Applied Formal Methods for Correct VLSI Design, pp.\u00a0759\u2013764 (1989)"},{"key":"7_CR11","volume-title":"Handbook of Model Checking","author":"P. Bouyer","year":"2018","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/123186.123222","volume-title":"Proc. of the 27th ACM\/IEEE Design Automation Conf. (DAC)","author":"K.S. Brace","year":"1990","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proc. of the 27th ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a040\u201345. ACM\/IEEE, New York\/Piscataway (1990)"},{"key":"7_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"R.K. Brayton","year":"1984","unstructured":"Brayton, R.K., Hachtel, G.D., McMullen, C.T., Sangiovanni-Vincentelli, A.L.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic, Norwell (1984)"},{"key":"7_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2078-5","volume-title":"Boolean Reasoning","author":"F.M. Brown","year":"1990","unstructured":"Brown, F.M.: Boolean Reasoning. Kluwer Academic, Norwell (1990)"},{"issue":"8","key":"7_CR15","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"7_CR16","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205\u2013213 (1991)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"7_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"7_CR18","first-page":"236","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"R.E. Bryant","year":"1995","unstructured":"Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0236\u2013243. IEEE, Piscataway (1995)"},{"key":"7_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-69850-0_9","volume-title":"25 Years of Model Checking","author":"R.E. Bryant","year":"2008","unstructured":"Bryant, R.E.: A view from the engine room: Computational support for symbolic model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0145\u2013149. Springer, Heidelberg (2008)"},{"issue":"4","key":"7_CR20","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"2","key":"7_CR21","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020$10^{20}$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"7_CR22","volume-title":"Handbook of Model Checking","author":"S. Chaki","year":"2018","unstructured":"Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"7_CR23","first-page":"53","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"S. Chaki","year":"2009","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer-Aided Design (FMCAD), pp.\u00a053\u201360. IEEE, Piscataway (2009)"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf. 8, 4\u201325 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","volume-title":"Proc. of the Workshop on Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) Proc. of the Workshop on Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp.\u00a0365\u2013373. Springer, Heidelberg (1989)"},{"key":"7_CR26","doi-asserted-by":"crossref","first-page":"818","DOI":"10.1145\/775832.776039","volume-title":"Proc. of the 40th ACM\/IEEE Design Automation Conf. (DAC)","author":"R. Damiano","year":"2003","unstructured":"Damiano, R., Kukula, J.: Checking satisfiability of a conjunction of BDDs. In: Proc. of the 40th ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0818\u2013923. ACM\/IEEE, New York\/Piscataway (2003)"},{"issue":"7","key":"7_CR27","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"3","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 3, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"7_CR29","volume-title":"11th Intl. Workshop on Parallel and Distributed Methods in Verification (PDMC)","author":"T. Dijk van","year":"2012","unstructured":"van Dijk, T., Laarman, A.W., van de Pol, J.C.: Multi-core BDD operations for symbolic reachability. In: 11th Intl. Workshop on Parallel and Distributed Methods in Verification (PDMC) (2012)"},{"issue":"1","key":"7_CR30","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/43.905674","volume":"20","author":"R. Drechsler","year":"2001","unstructured":"Drechsler, R., G\u00fcnther, W., Somenzi, F.: Using lower bounds during dynamic BDD minimization. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 20(1), 51\u201357 (2001)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"2","key":"7_CR31","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/s100090100056","volume":"3","author":"R. Drechsler","year":"2001","unstructured":"Drechsler, R., Sieling, D.: Binary decision diagrams in theory and practice. Int. J. Softw. Tools Technol. Transf. 3(2), 112\u2013136 (2001)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5","key":"7_CR32","doi-asserted-by":"publisher","first-page":"710","DOI":"10.1109\/12.53586","volume":"39","author":"S.J. Friedman","year":"1990","unstructured":"Friedman, S.J., Supowit, K.J.: Finding the optimum variable ordering for binary decision diagrams. IEEE Trans. Comput. 39(5), 710\u2013713 (1990)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR33","first-page":"2","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"M. Fujita","year":"1988","unstructured":"Fujita, M., Fujisawa, H., Kawato, N.: Evaluation and improvements of Boolean comparison method based on binary decision diagrams. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a02\u20135. IEEE, Piscataway (1988)"},{"key":"7_CR34","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M. Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10, 149\u2013169 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"7_CR35","volume-title":"Computers and Intractability","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability. Freeman, New York (1979)"},{"key":"7_CR36","first-page":"323","volume-title":"Proc. of the 1999 Conf. on Asia South Pacific Design Automation (ASP-DAC)","author":"W. Gunther","year":"1999","unstructured":"Gunther, W., Drechsler, R.: Minimization of free BDDs. In: Proc. of the 1999 Conf. on Asia South Pacific Design Automation (ASP-DAC), pp.\u00a0323\u2013326. IEEE, Piscataway (1999)"},{"key":"7_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Proc. of the 12th Intl. Conf. of Computer Aided Verification (CAV)","author":"T. Heyman","year":"2000","unstructured":"Heyman, T., Geist, D., Grumberg, O., Shuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) Proc. of the 12th Intl. Conf. of Computer Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a020\u201335. Springer, Heidelberg (2000)"},{"key":"7_CR38","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11527695_13","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"J. Huang","year":"2005","unstructured":"Huang, J., Darwiche, A.: Using DPLL for efficient OBDD construction. In: Hoos, H.H., Mitchell, D.G. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a03542, pp.\u00a0157\u2013172. Springer, Heidelberg (2005)"},{"key":"7_CR39","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"S.W. Jeong","year":"1991","unstructured":"Jeong, S.W., Plessier, B., Hachtel, G.D., Somenzi, F.: Variable ordering and selection of FSM traversal. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD). IEEE, Piscataway (1991)"},{"issue":"1\u20132","key":"7_CR40","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Multi-valued decision diagrams: theory and applications. Mult. Valued Log. 4(1\u20132), 9\u201362 (1998)","journal-title":"Mult. Valued Log."},{"key":"7_CR41","volume-title":"The Art of Computer Programming, vol.\u00a04: Combinatorial Algorithms","author":"D.S. Knuth","year":"2011","unstructured":"Knuth, D.S.: The Art of Computer Programming, vol.\u00a04: Combinatorial Algorithms. Addison-Wesley, Reading (2011)"},{"key":"7_CR42","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1837210.1837222","volume-title":"Proc. of the 4th Intl. Workshop on Parallel and Symbolic Computation (PASCO)","author":"D. Kunkle","year":"2010","unstructured":"Kunkle, D., Slavici, V., Cooperman, G.: Parallel disk-based computation for large, monolithic binary decision diagrams. In: Maza, M.M., Roch, J.-L. (eds.) Proc. of the 4th Intl. Workshop on Parallel and Symbolic Computation (PASCO), pp.\u00a063\u201372. ACM, New York (2010)"},{"key":"7_CR43","series-title":"LNCS","first-page":"113","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS)","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.P.: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS). LNCS, vol.\u00a02324, pp.\u00a0113\u2013140. Springer, Heidelberg (2002)"},{"issue":"3","key":"7_CR44","first-page":"271","volume":"6","author":"K.G. Larsen","year":"1999","unstructured":"Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6(3), 271\u2013298 (1999)","journal-title":"Nord. J. Comput."},{"key":"7_CR45","first-page":"205","volume-title":"Proc. of the 25th ACM\/IEEE Design Automation Conf. (DAC)","author":"J.C. Madre","year":"1988","unstructured":"Madre, J.C., Billon, J.P.: Proving circuit correctness using formal comparison between expected and extracted behaviour. In: Proc. of the 25th ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0205\u2013210. ACM\/IEEE, New York\/Piscataway (1988)"},{"key":"7_CR46","first-page":"6","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"S. Malik","year":"1988","unstructured":"Malik, S., Wang, A., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Logic verification using binary decision diagrams in a logic synthesis environment. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a06\u20139. IEEE, Piscataway (1988)"},{"key":"7_CR47","volume-title":"Handbook of Model Checking","author":"J. Marques-Silva","year":"2018","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"3","key":"7_CR48","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1109\/43.913762","volume":"20","author":"C.B. McDonald","year":"2001","unstructured":"McDonald, C.B., Bryant, R.E.: CMOS circuit verification with symbolic switch-level timing simulation. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 20(3), 458\u2013474 (2001)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"7_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Norwell (1993)"},{"key":"7_CR50","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1038\/218019a0","volume":"218","author":"D. Michie","year":"1968","unstructured":"Michie, D.: \u201cMemo\u201d functions and machine learning. Nature 218, 19\u201322 (1968)","journal-title":"Nature"},{"key":"7_CR51","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1145\/157485.164890","volume-title":"Proc. of the 30th ACM\/IEEE Design Automation Conf. (DAC)","author":"S. Minato","year":"1993","unstructured":"Minato, S.: Zero-suppressed BDDs for set manipulation in combinatorial problems. In: Proc. of the 30th ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0272\u2013277. ACM\/IEEE, New York\/Piscataway (1993)"},{"key":"7_CR52","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/123186.123225","volume-title":"Proc. of the 27th ACM\/IEEE Design Automation Conf. (DAC)","author":"S. Minato","year":"1990","unstructured":"Minato, S., Ishiura, N., Yajima, S.: Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation. In: Proc. of the 27th ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a052\u201357. ACM\/IEEE, New York\/Piscataway (1990)"},{"key":"7_CR53","series-title":"LNCS","first-page":"826","volume-title":"Computer Science Logic (CSL)","author":"J. M\u00f8ller","year":"1999","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodriguez-Artalejo, M. (eds.) Computer Science Logic (CSL). LNCS, vol.\u00a01683, p.\u00a0826. Springer, Heidelberg (1999)"},{"key":"7_CR54","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1109\/ICCAD.1996.569909","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"A. Narayan","year":"1996","unstructured":"Narayan, A., Jain, J., Fujita, M., Sangiovanni-Vincentelli, A.L.: Partitioned OBDDs\u2014a compact, canonical, and efficiently manipulable representation for Boolean functions. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0547\u2013554. IEEE, Piscataway (1996)"},{"key":"7_CR55","first-page":"48","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"H. Ochi","year":"1993","unstructured":"Ochi, H., Yasuoka, K., Yajima, S.: Breadth-first manipulation of very large binary-decision diagrams. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a048\u201355. IEEE, Piscataway (1993)"},{"key":"7_CR56","unstructured":"Ossowski, J.: JINC\u2014a multi-threaded library for higher-order weighted decision diagram manipulation. Ph.D. thesis, Rheinische Friedrich-Wilhelms-Universit\u00e4t, Bonn (2009)"},{"key":"7_CR57","first-page":"74","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"S. Panda","year":"1995","unstructured":"Panda, S., Somenzi, F.: Who are the variables in your neighbourhood. In: Formal Methods in Computer-Aided Design (FMCAD), pp.\u00a074\u201377. IEEE, Piscataway (1995)"},{"key":"7_CR58","first-page":"635","volume-title":"Proc. of the 33rd ACM\/IEEE Design Automation Conf. (DAC)","author":"R.K. Ranjan","year":"1996","unstructured":"Ranjan, R.K., Sanghavi, J.V., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: High performance BDD package based on exploiting memory hierarchy. In: Proc. of the 33rd ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0635\u2013640. ACM\/IEEE, New York\/Piscataway (1996)"},{"key":"7_CR59","first-page":"139","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD)","author":"R.L. Rudell","year":"1993","unstructured":"Rudell, R.L.: Dynamic variable ordering for ordered binary decision diagrams. In: Proc. of the Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0139\u2013144. IEEE, Piscataway (1993)"},{"issue":"3","key":"7_CR60","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1008681625346","volume":"13","author":"O. Schr\u00f6er","year":"1998","unstructured":"Schr\u00f6er, O., Wegener, I.: The theory of zero-suppressed BDDs and the number of knight\u2019s tours. Form. Methods Syst. Des. 13(3), 235\u2013253 (1998)","journal-title":"Form. Methods Syst. Des."},{"key":"7_CR61","series-title":"LNCS","first-page":"205","volume-title":"Symp. on Theoretical Aspects of Computer Science (STACS)","author":"D. Sieling","year":"1998","unstructured":"Sieling, D.: On the existence of polynomial time approximation schemes for OBDD minimization. In: Morvan, M., Meinel, C., Krob, D. (eds.) Symp. on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a01373, pp.\u00a0205\u2013215. Springer, Heidelberg (1998)"},{"issue":"3","key":"7_CR62","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0020-0190(93)90256-9","volume":"48","author":"D. Sieling","year":"1993","unstructured":"Sieling, D., Wegener, I.: Reduction of OBDDs in linear time. Inf. Process. Lett. 48(3), 139\u2013144 (1993)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"7_CR63","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s100090100042","volume":"3","author":"F. Somenzi","year":"2001","unstructured":"Somenzi, F.: Efficient manipulation of decision diagrams. Int. J. Softw. Tools Technol. Transf. 3(2), 171\u2013181 (2001)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR64","first-page":"641","volume-title":"Proc. of the 33rd ACM\/IEEE Design Automation Conf. (DAC)","author":"T. Stornetta","year":"1996","unstructured":"Stornetta, T., Brewer, F.: Implementation of an efficient parallel BDD package. In: Proc. of the 33rd ACM\/IEEE Design Automation Conf. (DAC), pp.\u00a0641\u2013644. ACM\/IEEE, New York\/Piscataway (1996)"},{"key":"7_CR65","first-page":"389","volume":"762","author":"S. Tani","year":"1993","unstructured":"Tani, S., Hamaguchi, K., Yajima, S.: The complexity of the optimal variable ordering problems of shared binary decision diagrams. Algorithms Comput. 762, 389\u2013398 (1993)","journal-title":"Algorithms Comput."},{"issue":"1","key":"7_CR66","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F. Wang","year":"2004","unstructured":"Wang, F.: Efficient verification of timed automata with efficient BDD-like data structures. Int. J. Softw. Tools Technol. Transf. 6(1), 77\u201397 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR67","series-title":"LNCS","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"B. Yang","year":"1998","unstructured":"Yang, B., Bryant, R.E., O\u2019Hallaron, D.R., Biere, A., Coudert, O., Janssen, G., Ranjan, R.K., Somenzi, F.: A performance study of BDD-based model checking. In: Gopalakrishnan, G., Windley, P. (eds.) Formal Methods in Computer-Aided Design (FMCAD). LNCS, vol.\u00a01522. Springer, Heidelberg (1998)"},{"key":"7_CR68","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1109\/ASPDAC.1998.669515","volume-title":"Proc. of the 1998 Conf. on Asia South Pacific Design Automation (ASP-DAC)","author":"B. Yang","year":"1998","unstructured":"Yang, B., Chen, Y.A., Bryant, R.E., O\u2019Hallaron, D.R.: Space- and time-efficient BDD construction via working set control. In: Proc. of the 1998 Conf. on Asia South Pacific Design Automation (ASP-DAC), pp.\u00a0423\u2013432. IEEE, Piscataway (1998)"},{"key":"7_CR69","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/BFb0031826","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"T. Yoneda","year":"1996","unstructured":"Yoneda, T., Hatori, H., Takahara, A., Minato, S.: BDDs vs. zero-suppressed BDDs for CTL symbolic model checking of Petri nets. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD). LNCS, vol.\u00a01166, pp.\u00a0435\u2013449. Springer, Heidelberg (1996)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T21:57:45Z","timestamp":1661291865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_7","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}