{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:26:33Z","timestamp":1754483193429},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434771"},{"type":"electronic","value":"9783540460176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_18","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"230-239","source":"Crossref","is-referenced-by-count":19,"title":["Comparing Symbolic and Explicit Model Checking of a Software System"],"prefix":"10.1007","author":[{"given":"Cindy","family":"Eisner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"18_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-48683-6_9","volume-title":"Model checking the IBM Gigahertz Processor: An abstraction algorithm for high-performance netlists","author":"J. Baumgartner","year":"1999","unstructured":"J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz. Model checking the IBM Gigahertz Processor: An abstraction algorithm for high-performance netlists. In Proc. 11\n                           th\n                           International Conference on Computer Aided Verification (CAV), LNCS 1633, pages 72\u201383. Springer-Verlag, 1999."},{"key":"18_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 13th International Conference on Computer Aided Verification (CAV)","author":"I. Beer","year":"2001","unstructured":"I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The temporal logic Sugar. In G. Berry, H. Comon, and A. Finkel, editors, Proc. 13\n                           \n                    th\n                  \n                           International Conference on Computer Aided Verification (CAV), LNCS 2102. Springer-Verlag, 2001."},{"key":"18_CR3","series-title":"Lect Notes Comput Sci","volume-title":"RuleBase: Model checking at IBM","author":"I. Beer","year":"1997","unstructured":"I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, and Y. Wolfsthal. RuleBase: Model checking at IBM. In Proc. 9\n                           \n                    th\n                  \n                           International Conference on Computer Aided Verification (CAV), LNCS 1254. Springer-Verlag, 1997."},{"doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver. RuleBase: an industry-oriented formal verification tool. In Proc. 33\n                           \n                    rd\n                  \n                           Design Automation Conference (DAC), pages 655\u2013660. Association for Computing Machinery, Inc., June 1996.","key":"18_CR4","DOI":"10.1145\/240518.240642"},{"doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in temporal model checking. Formal Methods in System Design, 18(2), 2001.","key":"18_CR5","DOI":"10.1023\/A:1008779610539"},{"key":"18_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"On-the-fly model checking of RCTL formulas","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In Proc. 10\n                           \n                    th\n                  \n                           International Conference on Computer Aided Verification (CAV), LNCS 1427, pages 184\u2013194. Springer-Verlag, 1998."},{"doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","key":"18_CR7","DOI":"10.1109\/TC.1986.1676819"},{"unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.","key":"18_CR8"},{"doi-asserted-by":"crossref","unstructured":"C. Eisner. Model checking the garbage collection mechanism of SMV. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001.","key":"18_CR9","DOI":"10.1016\/S1571-0661(04)00258-0"},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Efficient model checking by automated ordering of transition relation partitions","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. 6\n                           \n                    th\n                  \n                           International Conference on Computer Aided Verification (CAV), LNCS 818, pages 299\u2013310. Springer-Verlag, 1994."},{"unstructured":"G. Holzmann. On the fly, ltl model checking with spin: Simple spin manual. In \n                    http:\/\/cm.bell-labs.com\/cm\/cs\/what\/spin\/Man\/Manual.html\n                    \n                  .","key":"18_CR11"},{"unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.","key":"18_CR12"},{"key":"18_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","key":"18_CR14","DOI":"10.1007\/978-1-4615-3190-6"},{"doi-asserted-by":"crossref","unstructured":"K. Ravi, K. McMillan, T. Shiple, and F. Somenzi. Approximation and decomposition of binary decision diagrams. In Proc. 35\n                           \n                    th\n                  \n                           Design Automation Conference (DAC). Association for Computing Machinery, Inc., June 1998.","key":"18_CR15","DOI":"10.1145\/277044.277168"},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Hints to accelerate symbolic traversal","author":"K. Ravi","year":"1999","unstructured":"K. Ravi and F. Somenzi. Hints to accelerate symbolic traversal. In Proceedings 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 1703, Bad Herrenalb, Germany, September 1999. Springer-Verlag."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","volume-title":"CHARME","author":"O. Shtrichman","year":"2001","unstructured":"O. Shtrichman. Pruning techniques for the SAT-based bounded model checking problem. In T. Margaria and T. F. Melham, editors, CHARME, volume 2144 of Lecture Notes in Computer Science. Springer, 2001."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T14:15:36Z","timestamp":1551017736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}