{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:18Z","timestamp":1742617158847,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:13:08Z","timestamp":1330254788000},"page":"82-95","source":"Crossref","is-referenced-by-count":9,"title":["Higher-level specification and verification with BDDs"],"prefix":"10.1007","author":[{"given":"Alan J.","family":"Hu","sequence":"first","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Andreas J.","family":"Drexler","sequence":"additional","affiliation":[]},{"given":"C. Han","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"8_CR1","unstructured":"Derek L. Beatty, Randal E. Bryant, and Carl-Johann H. Seger, \u201cSynchronous Circuit Verification by Symbolic Simulation: An Illustration,\u201d Advanced Research in VLSI: Proceedings of the Sixth MIT Conference, William J. Dally, ed., MIT Press, 1990."},{"key":"8_CR2","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":"8_CR3","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 TC 10\/WG 10.5 International Conference on Very Large Scale Integration, Edinburgh, Great Britain, 1991."},{"key":"8_CR4","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":"8_CR5","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":"8_CR6","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":"8_CR7","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":"8_CR8","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, Orna Grumberg, and David E. Long, \u201cModel Checking and Abstraction,\u201d Proceedings of the ACM Symposium on Principles of Programming Languages, 1992, pp. 343\u2013354.","DOI":"10.1145\/143165.143235"},{"key":"8_CR9","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, 3. Sifakis, ed., Lecture Notes in Computer Science Vol. 407, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"8_CR10","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":"8_CR11","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Ran Yang, \u201cProtocol Verification as a Hardware Design Aid,\u201d to appear in IEEE International Conference on Computer Design, 1992."},{"key":"8_CR12","unstructured":"David L. Dill, Alan J. Hu, and Howard Wong-Toi, \u201cChecking for Language Inclusion Using Simulation Preorders,\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."},{"key":"8_CR13","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":"8_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":"8_CR15","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein and David Dill, \u201cFormal Verification of Cache Systems using Refinement Relations,\u201d IEEE International Conference on Computer Design, 1990, pp. 228\u2013233.","DOI":"10.1109\/ICCD.1990.130211"},{"key":"8_CR16","unstructured":"J. McCarthy and P.J. Hayes, \u201cSome Philosophical Problems from the Standpoint of Artificial Intelligence,\u201d in Machine Intelligence 4, B. Meltzer and D. Michie, eds., Edinburgh University Press, 1969."},{"key":"8_CR17","unstructured":"K. L. McMillan and J. Schwalbe, \u201cFormal Verification of the Gigamax Cache-Consistency Protocol,\u201d Proceedings of the International Symposium on Shared Memory Multiprocessing, Information Processing Society of Japan, 1991, pp. 242\u2013251."},{"key":"8_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":"8_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-56496-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:49:02Z","timestamp":1742593742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}