{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:32Z","timestamp":1781238812538,"version":"3.54.1"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1997,4]]},"DOI":"10.1023\/a:1008699807402","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"171-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":179,"title":["Algebraic Decision Diagrams and Their Applications"],"prefix":"10.1007","volume":"10","author":[{"given":"R.I.","family":"Bahar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"E.A.","family":"Frohm","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C.M.","family":"Gaona","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"E.","family":"Macii","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Pardo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"F.","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[1997,4,1]]},"reference":[{"key":"126528_CR1","unstructured":"A.V. Aho, J.E. Hopcroft, and J.D. Ullman, The Design and Analysis of Computer Algorithms, Addison Wesley, 1974."},{"key":"126528_CR2","volume-title":"The Mathematical Analysis of Logic","author":"G. Boole","year":"1847","unstructured":"G. Boole, The Mathematical Analysis of Logic, Macmillan, 1847, Reprinted by B. Blackwell, Oxford, UK, 1951."},{"key":"126528_CR3","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R. Rudell, and R. Bryant, \"Efficient implementation of a BDD package,\" DAC-27: ACM\/IEEE Design Automation Conference, Orlando, FL, June 1990, pp. 40-45.","DOI":"10.1145\/123186.123222"},{"key":"126528_CR4","doi-asserted-by":"crossref","unstructured":"F.M. Brown, Boolean Reasoning: The Logic of Boolean Equations, Kluwer Academic Publishers, 1990.","DOI":"10.1007\/978-1-4757-2078-5"},{"issue":"8","key":"126528_CR5","first-page":"79","volume":"35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \"Graph-Based Algorithms for Boolean function manipulation,\" IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 79-85, Aug. 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"126528_CR6","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, \"Sequential circuit verification using symbolic model checking,\" DAC-27: ACM\/IEEE Design Automation Conference, Orlando, FL, June 1990, pp. 46-51.","DOI":"10.1145\/123186.123223"},{"key":"126528_CR7","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long, \"Representing circuits more efficiently in symbolic model checking,\" DAC-28: ACM\/IEEE Design Automation Conference, San Francisco, CA, June 1991, pp. 403-407.","DOI":"10.1145\/127601.127702"},{"key":"126528_CR8","doi-asserted-by":"crossref","unstructured":"H. Cho, G.D. Hachtel, S.W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi, \"ATPG aspects of FSM verification,\" ICCAD-90: IEEE International Conference on Computer Aided Design, Santa Clara, CA, Nov. 1990, pp. 134-137.","DOI":"10.1109\/ICCAD.1990.129861"},{"key":"126528_CR9","doi-asserted-by":"crossref","unstructured":"H. Cho, G.D. Hachtel, E. Macii, B. Plessier, and F. Somenzi, \"Algorithms for approximate FSM traversal,\" DAC-30: ACM\/IEEE Design Automation Conference, Dallas, TX, June 1993, pp. 25-30.","DOI":"10.1145\/157485.164555"},{"key":"126528_CR10","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, \"Spectral transforms for large Boolean functions with applications to technology mapping,\" DAC-30: ACM\/IEEE Design Automation Conference, Dallas, TX, June 1993, pp. 54-60.","DOI":"10.1145\/157485.164569"},{"key":"126528_CR11","unstructured":"E.M. Clarke, M. Fujita, P.C. McGeer, K. McMillan, and J. Yang, \"Multi-terminal binary decision diagrams: An efficient data structure for matrix representation,\" IWLS'93: International Workshop on Logic Synthesis, Lake Tahoe, CA, May 1993, pp. 6a:1-15."},{"key":"126528_CR12","unstructured":"T.H. Cormen, C.E. Leiserson, and R.L. Rivest, An Introduction to Algorithms, McGraw-Hill, 1990."},{"key":"126528_CR13","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","volume":"407","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \"Verification of sequential machines based on symbolic execution,\" Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, Vol. 407, pp. 365-373, 1989.","journal-title":"Automatic Verification Methods for Finite State Systems"},{"key":"126528_CR14","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \"Verification of sequential machines using boolean functional vectors,\" IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, Nov. 1989, pp. 111-128."},{"key":"126528_CR15","unstructured":"I.S. Duff, \"Harwell Subroutine Library,\" AERE Report R.8730, Atomic Energy Research Establishment, Oxon, England, 1977."},{"key":"126528_CR16","unstructured":"I.S. Duff, A.M. Erisman, and J.K. Reid, Direct Methods for Sparse Matrices, Clarendon Press, 1986."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008699807402.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008699807402\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008699807402.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:43:40Z","timestamp":1754369020000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008699807402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":16,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["126528"],"URL":"https:\/\/doi.org\/10.1023\/a:1008699807402","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,4]]},"assertion":[{"value":"1 April 1997","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}