{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T15:17:09Z","timestamp":1774797429513,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_29","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"359-364","source":"Crossref","is-referenced-by-count":878,"title":["NuSMV 2: An OpenSource Tool for Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Pistore","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, and R. Sebastiani. A SAT based approach for solving formulas over boolean and linear mathematical propositions. In Proc. of CADE\u201902, 2002.","DOI":"10.1007\/3-540-45620-1_17"},{"key":"29_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":"29_CR3","unstructured":"P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, and P. Traverso. MBP: a Model Based Planner. In Proc. of the IJCAI\u201901 Workshop on Planning under Uncertainty and Incomplete Information, Seattle, August 2001."},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), 1999.","DOI":"10.21236\/ADA360973"},{"key":"29_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, editors, Proc. of the Second International ERCIM FMICS, Pisa, Italy, July 1997."},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT), 2(4), March 2000.","DOI":"10.1007\/s100090050046"},{"key":"29_CR7","series-title":"Lect Notes Comput Sci","first-page":"182","volume-title":"Proc. WMCAI 2002","author":"A. Cimatti","year":"2002","unstructured":"A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In Proc. WMCAI 2002, number 2294 in LNCS, pages 182\u2013195, 2002."},{"key":"29_CR8","first-page":"15213","volume-title":"Technical Report CMU-CS-95-161","author":"E. Clarke","year":"1995","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\u20133891, USA, May 1995."},{"key":"29_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45669-4","volume-title":"Proc. of Conference on Computer-Aided Verification (CAV\u201902)","author":"E. M. Clarke","year":"2002","unstructured":"E. M. Clarke, A. Gupta, J. Kukula, and O. Strichman. Sat based abstraction-refinement using ILP and machine learning techniques. In Proc. of Conference on Computer-Aided Verification (CAV\u201902), LNCS, 2002. To appear in this volume."},{"key":"29_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Proc. of CAV 2001","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of bounded model checking at an industrial setting. In Proc. of CAV 2001, LNCS, pages 436\u2013453, 2001."},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"R. Eshuis and R. Wieringa. Verification support for workflow design with UML activity graphs. In Proc. of ICSE, 2002. To appear.","DOI":"10.1145\/581360.581362"},{"key":"29_CR12","unstructured":"A. Fuxman, M. Pistore, J. Mylopoulos, and P. Traverso. Model checking early requirements specifications in Tropos. In Proc. of the Fifth IEEE International Symposium on Requirements Engineering (RE\u201901), Toronto, August 2001."},{"key":"29_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45744-5_26","volume-title":"Proc. of IJCAR 2001","author":"E. Giunchiglia","year":"2001","unstructured":"E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proc. of IJCAR 2001, volume 2083 of LNCS, pages 347\u2013363. Springer, 2001."},{"key":"29_CR14","unstructured":"The Gnu Lesser General Public License: http:\/\/www.fsf.org\/licenses\/lgpl.html ."},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proc. of the 39th Design Automation Conference, June 2001.","DOI":"10.1145\/378239.379017"},{"key":"29_CR17","unstructured":"The Open Source Organization. http:\/\/www.opensource.org ."},{"key":"29_CR18","unstructured":"R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In Proc. IEEE\/ACM International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995."},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"O. Shtrichman. Tuning SAT checkers for bounded model-checking. In Proc. 12th International Computer Aided Verification Conference (CAV\u201900), 2000.","DOI":"10.1007\/10722167_36"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:21:20Z","timestamp":1556414480000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}