{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:31Z","timestamp":1761597331703,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569220"},{"type":"electronic","value":"9783540477877"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56922-7_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:53:40Z","timestamp":1330257220000},"page":"3-14","source":"Crossref","is-referenced-by-count":10,"title":["Efficient verification with BDDs using implicitly conjoined invariants"],"prefix":"10.1007","author":[{"given":"Alan J.","family":"Hu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"2_CR1","unstructured":"S. Bose and A. Fisher, \u201cAutomatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic,\u201d IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, \u201cEfficient Implementation of a BDD Package,\u201d 27th ACM\/IEEE Design Automation Conference, 1990, pp. 40\u201345.","DOI":"10.1145\/123186.123222"},{"issue":"No.8","key":"2_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"Randal E. E. Bryant","year":"1986","unstructured":"Randal E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8 (August 1986), pp. 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR4","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long, \u201cSymbolic Model Checking with Partitioned Transition Relations,\u201d VLSI '91: Proceedings of the IFIP TC10\/WG 10.5 International Conference on Very Large Scale Integration, Edinburgh, Great Britain, 1991."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and David L. Dill, \u201cSequential Circuit Verification Using Symbolic Model Checking,\u201d 27th ACM\/IEEE Design Automation Conference, 1990, pp. 46\u201351.","DOI":"10.1145\/123186.123223"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, \u201cSymbolic Model Checking: 1020 States and Beyond,\u201d Proceedings of the Conference on Logic in Computer Science, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Hyunwoo Cho, Gary Hachtel, Seh-Woong Jeong, Bernard Plessier, Eric Schwarz, and Fabio Somenzi, \u201cATPG Aspects of FSM Verification,\u201d IEEE International Conference on Computer-Aided Design, 1990, pp. 134\u2013137.","DOI":"10.1109\/ICCAD.1990.129861"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Olivier Coudert, Christian Berthet, and Jean Christophe Madre, \u201cVerification of Synchronous Sequential Machines Based on Symbolic Execution,\u201d Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., Lecture Notes in Computer Science Vol. 407, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"2_CR9","unstructured":"Olivier Coudert, Christian Berthet, and Jean Christophe Madre, \u201cVerification of Sequential Machines Using Boolean Functional Vectors,\u201d IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, \u201cProtocol Verification as a Hardware Design Aid,\u201d IEEE International Conference on Computer Design, October 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Thomas Filkorn, \u201cFunctional Extension of Symbolic Model Checking,\u201d Computer-Aided Verification: Third International Workshop, July 1\u20134, 1991, K.G. Larsen and A. Skou, eds., Lecture Notes in Computer Science Vol. 575, Springer-Verlag, published 1992.","DOI":"10.1007\/3-540-55179-4_22"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Alan J. Hu and David L. Dill, \u201cReducing BDD Size by Exploiting Functional Dependencies,\u201d 30th ACM\/IEEE Design Automation Conference, 1993, to appear.","DOI":"10.1145\/157485.164888"},{"key":"2_CR13","unstructured":"Alan J. Hu, David L. Dill, Andreas J. Drexler, and C. Han Yang, \u201cHigher-Level Specification and Verification with BDDs,\u201d Computer-Aided Verification: Fourth International Workshop, July 1992, to be reprinted in Springer-Verlag's LNCS Series."},{"key":"2_CR14","volume-title":"Variable Ordering for FSM Traversal","author":"S.-W. Jeong","year":"1991","unstructured":"S.-W. Jeong, B. Plessier, G.D. Hachtel, and F. Somenzi, \u201cVariable Ordering for FSM Traversal,\u201d Proceedings of the International Workshop on Logic Synthesis, MCNC, Research Triangle Park, NC, May 1991."},{"key":"2_CR15","unstructured":"Timothy Y. K. Kam and Robert K. Brayton, \u201cMulti-Valued Decision Diagrams,\u201d UCB\/ERL M90\/125, December 1990."},{"key":"2_CR16","unstructured":"Yung-Te Lai and Sarma Sastry, \u201cEdge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Verification,\u201d 29th ACM\/IEEE Design Automation Conference, 1992, pp. 608\u2013613."},{"key":"2_CR17","unstructured":"David E. Long, personal correspondence."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Arvind Srinivasan, Timothy Kam, Sharad Malik, and Robert K. Brayton, \u201cAlgorithms for Discrete Function Manipulation,\u201d IEEE International Conference on Computer-Aided Design, 1990, pp. 92\u201395.","DOI":"10.1109\/ICCAD.1990.129849"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Herve J. Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, \u201cImplicit State Enumeration of Finite State Machines using BDD's\u201d IEEE International Conference on Computer-Aided Design, 1990, pp. 130\u2013133.","DOI":"10.1109\/ICCAD.1990.129860"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56922-7_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:57:26Z","timestamp":1742594246000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56922-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569220","9783540477877"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-56922-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}