{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:36Z","timestamp":1761611256955},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_43","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"436-453","source":"Crossref","is-referenced-by-count":83,"title":["Benefits of Bounded Model Checking at an Industrial Setting"],"prefix":"10.1007","author":[{"given":"Fady","family":"Copty","sequence":"first","affiliation":[]},{"given":"Limor","family":"Fix","sequence":"additional","affiliation":[]},{"given":"Ranan","family":"Fraer","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Gila","family":"Kamhi","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"43_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Proc. of the 6th International Conference of Tools and Algorithms for Construction and Analisys of Systems (TACAS 2000)","author":"P. A. Abdulla","year":"2000","unstructured":"P. A. Abdulla, P. Bjesse, and N. E\u2019en. Symbolic reachability analisys based on SAT solvers. In Proc. of the 6th International Conference of Tools and Algorithms for Construction and Analisys of Systems (TACAS 2000), volume 1785 of LNCS, pages 411\u2013425, Berlin, 2000. Springer."},{"key":"43_CR2","unstructured":"R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi. ForSpec: A Formal Temporal Specification Language, Submitted to ICCAD\u201901"},{"key":"43_CR3","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, A. Landver. \u201cRuleBase: An industry-oriented formal verification tool\u201d. In Proc. Design Automation Conference 1996 (DAC\u201996).","DOI":"10.1145\/240518.240642"},{"key":"43_CR4","doi-asserted-by":"crossref","unstructured":"I. Beer, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, Y. Wolfsthal. \u201cRuleBase: Model Checking at IBM\u201d, Proceedings of CAV\u201997.","DOI":"10.1007\/3-540-63166-6_53"},{"key":"43_CR5","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, and K.L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"Armin Biere, Edmund Clarke, Richard Raimi, and Yunshan Zhu. \u201cVerifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs\u201d. Proc. of Computer Aided Verification, 1999 (CAV\u201999).","DOI":"10.1007\/3-540-48683-6_8"},{"key":"43_CR7","unstructured":"A. Biere, A Cimatti, E. M. Clarke, and Y. Zhu. \u201cSymbolic model checking without BDDs\u201c. TACAS\u201999"},{"key":"43_CR8","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of the 36th Conference on Design Automation (DAC\u2019 99), pages 317\u2013320. ACM Press, 1999.","DOI":"10.1145\/309847.309942"},{"issue":"3","key":"43_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"43_CR10","doi-asserted-by":"crossref","unstructured":"R. J. Bayardo, Jr. and R. C. Schrag, \u201cUsing CSP Look-Back Techniques to Solve Real-World SAT Instances\u201c, pages 203\u2013208, Proc. AAAI, 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"43_CR11","doi-asserted-by":"crossref","unstructured":"M. Davis and G. Logemann and D. Loveland, \u201cA machine program for theorem proving\u201d, Journal of the ACM, vol. 5, 1962.","DOI":"10.1145\/368273.368557"},{"issue":"n.3","key":"43_CR12","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R. Dechter","year":"1990","unstructured":"R. Dechter, \u201cEnhancement Schemes for Constraint Processing: Backjumping, Learning, and Cutset Decomposition\u201d, Artificial Intelligence, pages 273\u2013312, vol. 41,n.3, 1990.","journal-title":"Artificial Intelligence"},{"key":"43_CR13","unstructured":"R. Fraer, G. Kamhi, B. Ziv, M. Vardi, L. Fix, \u201cEfficient Reachability Computation Both for Verification and Falsification\u201c, Proceedings of International Conference on Computer-Aided Design, (CAV\u201900)."},{"key":"43_CR14","unstructured":"J.W. Freeman, \u201cImprovements to propositional satisfiability search algorithms\u201d, PhD Thesis. University of Pennsylvania, 1995."},{"key":"43_CR15","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking: an Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"43_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum, \u201cA Structure-preserving Clause Form Translation\u201d, Journal of Symbolic Computation, vol.2, pages=293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"43_CR17","unstructured":"Prover 4.0 Application Programming Reference Manual, Prover Technology AB, 2000. PPI-01-ARM-1."},{"issue":"n. 3","key":"43_CR18","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"P. Prosser, \u201cHybrid algorithms for the constraint satisfaction problem\u201d, Computational Intelligence, vol. 9,n. 3, pages 268\u2013299, 1993.","journal-title":"Computational Intelligence"},{"key":"43_CR19","doi-asserted-by":"crossref","unstructured":"O. Shtrichman, \u201cTuning SAT checkers for Bounded Model-Checking\u201d Proc. of Computer Aided Verification, 2000 (CAV\u201900).","DOI":"10.1007\/10722167_36"},{"key":"43_CR20","doi-asserted-by":"crossref","unstructured":"M. Sheeran, S. Singh and G. Staalmarck, \u201cChecking safety properties using induction and a SAT solver\u201c Proceedings of Formal Methods in Computer Aided Design 2000 (FMCAD00)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"43_CR21","unstructured":"J.P. Marques Silva and Karem A. Sakallah. GRASP \u2014 a new search algorithm for satisfiability. Technical report, University of Michigan, April 1996."},{"key":"43_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Proc. of the 2nd International Conference on Formal Methods in Computer Aided Design (FMCAD\u2019 98)","author":"M. Sheeran","year":"1998","unstructured":"M. Sheeran and G. Stalmarck. A tutorial on Stalmarck\u2019s proof procedure for propositional logic. In Proc. of the 2nd International Conference on Formal Methods in Computer Aided Design (FMCAD\u2019 98), volume 1522 of LNCS, pages 82\u201399, Berlin, 1998. Springer."},{"key":"43_CR23","unstructured":"G. Stalmarck. System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated From Boolean Formula. Swedish Patent No. 467076 (approved 1992), US Patent No. 5276897 (1994), European Patent No. 0403454 (1995), 1989."},{"key":"43_CR24","unstructured":"A. Tacchella. \u201cSAT Based decision procedures for knowledge representation and Formal Verification\u201d. PhD Thesis. University of Genova. 2000."},{"key":"43_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Proc. of the 12th International Conference on Computer Aided Verification (CAV 2000)","author":"P. F. Williams","year":"2000","unstructured":"P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. of the 12th International Conference on Computer Aided Verification (CAV 2000), volume 1855 of LNCS, pages 124\u2013138, Berlin, 2000. Springer."},{"key":"43_CR26","unstructured":"J. Yang, A. Tiemeyer. \u201cLazy Symbolic Model Checking\u201d. DAC\u201900."},{"key":"43_CR27","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 272\u2013275, Berlin, July 13\u201317 1997. Springer.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T18:28:58Z","timestamp":1558808938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_43","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}