{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:40:46Z","timestamp":1725550846525},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_4","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"34-48","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Experimental Analysis of Different Techniques for Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"Robert","family":"Kurshan","sequence":"additional","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Ricardo","family":"Medel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In FMCAD, 2000.","DOI":"10.1007\/3-540-40922-X_23"},{"key":"4_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of LNCS, 1999."},{"key":"4_CR3","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS, 1990."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In CAV, 1999.","DOI":"10.21236\/ADA360973"},{"key":"4_CR5","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996."},{"key":"4_CR6","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"P. Bjesse","year":"2001","unstructured":"P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an Alpha microprocessor using satisfiability solvers. In CAV, volume 2102 of LNCS, 2001."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"A. Boralv. The industrial success of verification tools based on stalmarck\u2019s method. In CAV, 1997.","DOI":"10.1007\/3-540-63166-6_3"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Can bdds compete with sat solvers on bounded model checking. In DAC, 2002.","DOI":"10.1145\/513945.513949"},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS, 1981."},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"C. Fady","year":"2001","unstructured":"Fady C., L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV, volume 2102 of LNCS, 2001."},{"key":"4_CR12","unstructured":"E. Goldberg and Y. Novikov. Berkmin: A fast and robust sat-solver. In DATE, 2002."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Z. Har\u2019El and R. P. Kurshan. Software for analytical development of communications protocols. AT&T Technical Journal, 69(1), 1990.","DOI":"10.1002\/j.1538-7305.1990.tb00102.x"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In DAC, 1997.","DOI":"10.1145\/266021.266090"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In VMCAI, 2002.","DOI":"10.1007\/3-540-36384-X_24"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"4_CR18","unstructured":"K. McMillan. Getting started with smv, 1999. URL: \n                    http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\n                    \n                  ."},{"key":"4_CR19","unstructured":"M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC\u201901), 2001."},{"key":"4_CR20","unstructured":"Marques-Silva and Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers, 48, 1999."},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Specification and verification of concurrent systems in CESAR","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"4_CR22","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"M. Sheeran","year":"1998","unstructured":"M. Sheeran and G. St\u00e5lmarck. A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In CAV, volume 1522 of LNCS, 1998."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"O. Strichman. Tuning SAT checkers for bounded model checking. In CAV, 2000.","DOI":"10.1007\/10722167_36"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"M. N. Velev and R. E. Bryant. Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW. In Proceedings of the 38th Conference on Design Automation Conference 2001, 2001.","DOI":"10.1145\/378239.378469"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An eficient propositional prover. In Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T14:34:44Z","timestamp":1558276484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}