{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:53Z","timestamp":1761611213799,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433811"},{"type":"electronic","value":"9783540459880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45988-x_5","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T02:19:02Z","timestamp":1181182742000},"page":"49-56","source":"Crossref","is-referenced-by-count":13,"title":["Integrating BDD-Based and SAT-Based Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Pistore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Proc. Tools and Algorithms for the Construction and Analysis of Systems TACAS","author":"P. A. Abdulla","year":"2000","unstructured":"Parosh Aziz Abdulla, Per Bjesse, and Niklas E\u00e9n. Symbolic reachability analysis based on SAT-solvers. In Susanne Graf and Michael Schwartzbach, eds., Proc. Tools and Algorithms for the Construction and Analysis of Systems TACAS, Berlin, Germany, volume 1785 of LNCS. Springer-Verlag, 2000."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"S. Berezin, S. Campos, and E. M. Clarke. Compositional reasoning in model checking. In Proc. COMPOS, 1997.","DOI":"10.21236\/ADA339195"},{"key":"5_CR3","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. 36th Conference on Design Automation, 1999.","DOI":"10.1145\/309847.309942"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99), 1999.","DOI":"10.21236\/ADA360973"},{"key":"5_CR5","unstructured":"A. Bor\u00e4lv. A Fully Automated Approach for Proving Safety Properties in Interlocking Software Using Automatic Theorem-Proving. In S. Gnesi and D. Latella, eds., Proceedings of the Second International ERCIM Workshop on Formal Methods for Industrial Critical Systems, Pisa, Italy, July 1997."},{"issue":"3","key":"5_CR6","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"},{"issue":"2","key":"5_CR7","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":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings Eleventh Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, eds., Proceedings Eleventh Conference on Computer-Aided Verification (CAV\u201999), number 1633 in Lecture Notes in Computer Science, pages 495\u2013499, Trento, Italy, July 1999. Springer-Verlag."},{"issue":"1","key":"5_CR9","first-page":"57","volume":"10","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10(1):57\u201371, February 1997.","journal-title":"Formal Methods in System Design"},{"key":"5_CR10","unstructured":"E. Clarke and X. Zhao. Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits. Technical Report CMU-CS-95-161, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213-3891, USA, May 1995."},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Synthesis of synchronization skeletons for branching time tem poral logic","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time tem poral logic. In Logic of Programs: Workshop. Springer Verlag, May 1981. Lecture Notes in Computer Science No. 131."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Fady Copty, Limor Fix, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, and Moshe Vardi. Benefits of bounded model checking at an industrial setting. In Proceedings of CAV 2001, pages 436\u2013453, 2001.","DOI":"10.1007\/3-540-44585-4_43"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, and Limor Fix. Prioritized traversal: Efficient reachability analysis for verification and falsification. In Proceedings of the 12th International Conference on Computer Aided Verification, pages 389\u2013402. Springer, July 2000.","DOI":"10.1007\/10722167_30"},{"key":"5_CR14","unstructured":"E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In Proc. AAAI, 1998."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to nonclausal formulas. In Evelina Lamma and Paola Mello, eds., Proceedings of AI*IA\u201999: Advances in Artificial Intelligence, pages 84\u201394. Springer Verlag, 1999.","DOI":"10.1007\/3-540-46238-4_8"},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45744-5_26","volume-title":"Proceedings of IJCAR 2001","author":"E. Giunchiglia","year":"2001","unstructured":"Enrico Giunchiglia, Marco Maratea, Armando Tacchella, and Davide Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Rajeev Gor\u00e9, Alexander Leitsch, and Tobias Nipkow, eds., Proceedings of IJCAR 2001, volume 2083 of Lecture Notes in Computer Science, pages 347\u2013363. Springer, 2001."},{"issue":"5","key":"5_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker Spin. IEEE Trans. on Software Engineering, 23(5):279\u2013295, May 1997. Special issue on Formal Methods in Software Practice.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th Design Automation Conference, pages 530\u2013535. ACM, 2001.","DOI":"10.1145\/378239.379017"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"5_CR21","unstructured":"R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE\/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. High-density reachability analysis. In International Conference on Computer Aided Design, pages 154\u2013158, Los Alamitos, Ca., USA, November 1995. IEEE Computer Society Press.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"O. Shtrichman. Tuning SAT checkers for bounded model-checking. In Proc. 12th International Computer Aided Verification Conference (CAV), 2000.","DOI":"10.1007\/10722167_36"},{"key":"5_CR24","unstructured":"F. Somenzi. CUDD: CU Decision Diagram package-release 2.1.2. Department of Electrical and Computer Engineering-University of Colorado at Boulder, April 1997."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45988-X_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T01:17:29Z","timestamp":1737076649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45988-X_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433811","9783540459880"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45988-x_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}