{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:33:17Z","timestamp":1770291197225,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540668565","type":"print"},{"value":"9783540466741","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_25","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"294-307","source":"Crossref","is-referenced-by-count":2,"title":["BDD-Nodes Can Be More Expressive"],"prefix":"10.1007","author":[{"given":"Frank","family":"Reffel","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/BFb0015246","volume":"1000","author":"A. Anuchitanukul","year":"1995","unstructured":"A. Anuchitanukul, Z. Manna, and T. E. Uribe. Differential BDDs. Lecture Notes in Computer Science, 1000:218\u2013233, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR2","unstructured":"A. Biere. Effiziente _-Kalk\u00fcl Modellpr\u00fcfung mit Bin\u00e4ren Entscheidungsdiagrammen. PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, 1997."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"J. Bitner, J. Jain, M. Abadir, J. Abraham, and D. Fussell. Efficient algorithmic verification using indexed BDD\u2019s. In International Symposium on Fault-Tolerant Systems, pages 266\u2013275, 1994.","DOI":"10.1109\/FTCS.1994.315633"},{"issue":"1","key":"25_CR4","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M. C. Browne","year":"1989","unstructured":"M. C. Browne, E. M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. Information and Computation, 81(1):13\u201331, Apr. 1989.","journal-title":"Information and Computation"},{"issue":"8","key":"25_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"5. R. Bryant","year":"1986","unstructured":"[5] R. Bryant. Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"25_CR6","doi-asserted-by":"publisher","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, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"25_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Computer Aided Verification, 10th International Conference, CAV\u201998","author":"E. M. Clarke","year":"1998","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Symmetry reductions in model checking. In Computer Aided Verification, 10th International Conference, CAV\u201998, volume 1427 of Lecture Notes in Computer Sciences, pages 147\u2013158, 1998."},{"issue":"5","key":"25_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, Sept. 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/BFb0015260","volume":"1000","author":"E. M. Clarke","year":"1995","unstructured":"E. M. Clarke and S. Jha. Symmetry and induction in model checking. Lecture Notes in Computer Science, 1000:455\u2013470, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. An ACM Distinguished Dissertation. The MIT Press, 1988.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201995), pages 85\u201394, San Francisco, 1995.","DOI":"10.1145\/199448.199468"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1109\/12.324545","volume":"43","author":"J. Gergov","year":"1994","unstructured":"J. Gergov and C. Meinel. Efficient Analysis and Manipulation of OBDDs can be extended to FBDDs. IEEE Transactions on Computers, 43:1197\u20131209, 1994.","journal-title":"IEEE Transactions on Computers"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"A. Gupta and A. L. Fisher. Representation and symbolic manipulation of linearly inductive boolean functions. In IEEE International Conference on Computer-Aided Design, pages 192\u2013199, 1993.","DOI":"10.1109\/ICCAD.1993.580055"},{"key":"25_CR14","unstructured":"[14] T. Kropf. Benchmark-circuits for hardware-verification. ftp:\/\/goethe.ira.uka.de\/-pub\/hvg\/benchmarks\/Whole documentation.ps.gz."},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"25_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-58179-0_42","volume-title":"Proceedings of the 6th International Conference on Computer-Aided Verification CAV","author":"K. McMillan","year":"1994","unstructured":"K. McMillan. Hierarchical representations of discrete functions, with application to model checking. In Proceedings of the 6th International Conference on Computer-Aided Verification CAV, volume 818 of Lecture Notes in Computer Science, pages 41\u201354, 1994."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"[17] S. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proceedings of the 30th ACM\/IEEE Design Automation Conference, pages 272\u2013277, Dallas, 1993.","DOI":"10.1145\/157485.164890"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In International Conference on Computer-Aided Design, pages 139\u2013144. IEEE, 1993.","DOI":"10.1109\/ICCAD.1993.580029"},{"issue":"1\/2","key":"25_CR19","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\/2):72\u201399, Jan.\/Feb. 1983.","journal-title":"Information and Control"},{"key":"25_CR20","unstructured":"B. Yang. Examples from SMV distribution. http:\/\/www.cs.cmu.edu\/bwolen\/software ."},{"key":"25_CR21","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-49519-3_18","volume":"1522","author":"B. Yang","year":"1998","unstructured":"B. Yang, R. E. Bryant, D. R. O\u2019Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, and F. Somenzi. A performance study of BDD-based model checking. Lecture Notes in Computer Science, 1522:255\u2013289, 1998.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:59:00Z","timestamp":1737593940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}