{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:34:42Z","timestamp":1759638882781,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_63","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:43Z","timestamp":1330269943000},"page":"299-310","source":"Crossref","is-referenced-by-count":49,"title":["Efficient model checking by automated ordering of transition relation partitions"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Geist","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilan","family":"Beer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Ilan Beer, Michael Yoeli, Shoham Ben-David, and Daniel Geist. Methodology and System for Practical Formal Verification of Reactive Hardware. Accepted to CAV 94, 1994.","DOI":"10.1007\/3-540-58179-0_53"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Karl. S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient Implentation of a BDD Package. In 27th ACM\/IEEE Design Automation Conference, pages 40\u201345. ACM\/IEEE, 1990.","DOI":"10.1145\/123186.123222"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Randal E. Bryant. Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24:298\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"25_CR5","volume-title":"Symbolic Model Checking with Partitioned Transition Relations","author":"J. R. Burch","year":"1991","unstructured":"Jerry R. Burch, Edmund M. Clarke, and David E. Long. Symbolic Model Checking with Partitioned Transition Relations. In International Conference on Very Large Scale Integration, Edinburg, Scotland, August 1991. IFIP."},{"key":"25_CR6","unstructured":"Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David L. Long, Kenneth L. McMillan, and Linda A. Ness. Verification of the Futurebus+ Cache Coherence Protocol. In Proceedings of the 11th International Conference on Computer Hardware Description Languages, pages 15\u201330, 1993."},{"key":"25_CR7","first-page":"75","volume-title":"Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams","author":"O. Coudert","year":"1990","unstructured":"Olivier Coudert, Jean C. Madre, and Christian Berthet. Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams. In R. Kurshan and E. M. Clarke, editors. Workshop on Computer Aided Verification, DIMACS, pages 75\u201384. American Mathematical Society, Providence, RI, 1990."},{"key":"25_CR8","unstructured":"Alan J. Hu and David L. Dill. Efficient Verification with BDDs using Implicitly Conjoined Invariants. In Proceedings of the Conference on Computer Aided Verification (CAV 93), 1993."},{"key":"25_CR9","volume-title":"The SMV System DRAFT","author":"K. L. McMillan","year":"1992","unstructured":"K. L. McMillan. The SMV System DRAFT. Carnegie Mellon University, Pittsburgh, PA, 1992."},{"key":"25_CR10","unstructured":"K. L. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistency protocol. In Proceedings of the 1991 International Symposium on Shared Memory Multiprocessors, April 1991."},{"key":"25_CR11","unstructured":"Kenneth L. McMillan. Symbolc Model Checking. PhD thesis, Carnegie Mellon University, May 1992."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"H. J.Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit State Enumeration of Finite State Machines usin BDD's. In IEEE International Conference on CAD, pages 130\u2013133, 1990.","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-58179-0_63.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:21:50Z","timestamp":1742595710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}