{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:04:31Z","timestamp":1737435871561,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424970"},{"type":"electronic","value":"9783540446859"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44685-0_16","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:16:21Z","timestamp":1186740981000},"page":"233-247","source":"Crossref","is-referenced-by-count":14,"title":["Techniques for Smaller Intermediary BDDs"],"prefix":"10.1007","author":[{"given":"Jaco","family":"Geldenhuys","sequence":"first","affiliation":[]},{"given":"Antti","family":"Valmari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,22]]},"reference":[{"key":"16_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"CAV\u201997: Proc. 9th Intl. Conf. Computer-Aided Verification","author":"R. Alur","year":"1997","unstructured":"R. Alur, R.K. Brayton, T. Henzinger, S. Qadeer, & S.K. Rajamani. Partial-order reduction in symbolic state space exploration. In CAV\u201997: Proc. 9th Intl. Conf. Computer-Aided Verification, LNCS #1254, pp. 340\u2013351. Springer-Verlag, Jun 1997."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, & F. Somenzi. Algebraic decision diagrams and their applications. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 188\u2013191, Nov 1993.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proc. 5th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, & Y. Zhu. Symbolic model checking without BDDs. In Proc. 5th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS #1579, pp. 193\u2013207. Springer-Verlag, Mar 1999."},{"key":"16_CR4","first-page":"701","volume":"VIII","author":"R. Bloem","year":"2000","unstructured":"R. Bloem, I.-H. Moon, K. Ravi, & F. Somenzi. Approximations for fixpoint computations in symbolic model checking. In Proc. World Multiconference on Systemics, Cybernetics and Informatics, Vol. VIII, Part II, pp. 701\u2013706, 2000.","journal-title":"Proc. World Multiconference on Systemics, Cybernetics and Informatics"},{"issue":"8","key":"16_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, C-35(8):677\u2013691, Aug 1986.","journal-title":"IEEE Trans. Computers"},{"key":"16_CR6","unstructured":"J.R. Burch, E.M. Clarke, & D.E. Long. Symbolic model checking with partitioned transition relations. In Proc. IFIP Intl. Conf. Very Large Scale Integration, pp. 49\u201358, Aug 1991."},{"issue":"4","key":"16_CR7","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, & D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 13(4):401\u2013424, Apr 1994.","journal-title":"IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"2","key":"16_CR8","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, & L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, Jun 1992.","journal-title":"Information and Computation"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, L. Lavagno, & S. Quer. Disjunctive partitioning and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In Proc. 34th ACM\/IEEE Conf. Design Automation, pp. 728\u2013733, Jun 1997.","DOI":"10.1109\/DAC.1997.597241"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, & S. Quer. Improved reachability analysis of large finite state machines. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 354\u2013360, Nov 1996.","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, & S. Quer. Improving symbolic traversals by means of activity profiles. In Proc. 36th ACM\/IEEE Conf. Design Automation, pp. 306\u2013311, Jun 1999.","DOI":"10.1145\/309847.309938"},{"issue":"12","key":"16_CR12","doi-asserted-by":"crossref","first-page":"1451","DOI":"10.1109\/43.552079","volume":"15","author":"H. Cho","year":"1996","unstructured":"H. Cho, G.D. Hachtel, E. Macii, B. Plessier, & F. Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 15(12):1451\u20131464, Dec 1996.","journal-title":"IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"12","key":"16_CR13","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H. Cho","year":"1996","unstructured":"H. Cho, G.D. Hachtel, E. Macii, B. Plessier, & F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 15(12):1465\u20131478, Dec 1996.","journal-title":"IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems"},{"key":"16_CR14","series-title":"Lect Notes Comput Sci","first-page":"365","volume-title":"Proc. Intl. Workshop on Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, & J.C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Proc. Intl. Workshop on Automatic Verification Methods for Finite State Systems, LNCS #407, pp. 365\u2013373. Springer-Verlag, Jun 1989."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"M. Fujita, Y. Matsunaga, & T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In Proc. European Design Automation Conference, pp. 50\u201354, 1991.","DOI":"10.1109\/EDAC.1991.206358"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"S.G. Govindaraju, D.L. Dill, A.J. Hu, & M.A. Horowitz. Approximate reachability with BDDs using overlapping projections. In Proc. 35th ACM\/IEEE Conf. Design Automation, pp. 451\u2013456, Jun 1998.","DOI":"10.1145\/277044.277169"},{"key":"16_CR17","unstructured":"A.J. Hu. Efficient Techniques for Formal Verification Using Binary Decision Diagrams. PhD thesis, Stanford Univ., 1995."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"A.J. Hu, G. York, & D.L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In Proc. 31th ACM\/IEEE Conf. Design Automation, pp. 276\u2013282, Jun 1994.","DOI":"10.1145\/196244.196377"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"S.-i. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proc. 30th ACM\/IEEE Conf. Design Automation, pp. 272\u2013277, Jun 1993.","DOI":"10.1145\/157485.164890"},{"key":"16_CR20","unstructured":"T. Kam. State Minimization of Finite State Machines using Implicit Techniques. PhD thesis, Electronics Research Laboratory, Univ. of California at Berkeley, 1995."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"16_CR22","unstructured":"D.E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon Univ., 1993."},{"key":"16_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Proc. 20th Intl. Conf. Application and Theory of Petri Nets","author":"A. Miner","year":"1999","unstructured":"A. Miner & G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In Proc. 20th Intl. Conf. Application and Theory of Petri Nets, LNCS #1639, pp. 6\u201325. Springer-Verlag, Jun 1999."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"A. Narayan, A.J. Isles, J. Jain, R.K. Brayton, & A.L. Sangiovanni-Vincentelli. Reachability analysis using partitioned-ROBDDs. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 388\u2013393, Nov 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"16_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"Proc. 15th Intl. Conf. Application and Theory of Petri Nets","author":"E. Pastor","year":"1994","unstructured":"E. Pastor, O. Roig, J. Cortadella, & R. Badia. Petri net analysis using boolean manipulation. In Proc. 15th Intl. Conf. Application and Theory of Petri Nets, LNCS #815, pp. 416\u2013435. Springer-Verlag, 1994."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"K. Ravi & F. Somenzi. High-density reachability analysis. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 154\u2013158, Nov 1995.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"16_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-48153-2_19","volume-title":"Proc. 10th IFIP WG 10.5 Intl. Conf. Correct Hardware Design and Verification Methods","author":"K. Ravi","year":"1999","unstructured":"K. Ravi & F. Somenzi. Hints to accelerate symbolic traversal. In Proc. 10th IFIP WG 10.5 Intl. Conf. Correct Hardware Design and Verification Methods, LNCS #1703, pp. 250\u2013264. Springer-Verlag, Sept 1999."},{"key":"16_CR28","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 42\u201347, Nov 1993."},{"key":"16_CR29","unstructured":"A. Srinivasan, T. Kam, S. Malik, & R.K. Brayton. Algorithms for discrete function manipulation. In Proc. ACM\/IEEE Intl. Conf. Computer-Aided Design, pp. 92\u201397, Nov 1990."},{"key":"16_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/BFb0023460","volume-title":"Proc. 14th Annual Symposium on Theoretical Aspects of Computer Science","author":"S. Waack","year":"1997","unstructured":"S. Waack. On the descriptive and algorithmic power of parity ordered binary decision diagrams. In Proc. 14th Annual Symposium on Theoretical Aspects of Computer Science, LNCS #1200, pp. 201\u2013212. Springer-Verlag, Feb 1997."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2001 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44685-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:24:58Z","timestamp":1737357898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44685-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424970","9783540446859"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-44685-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}