{"id":405,"date":"2023-04-06T09:02:23","date_gmt":"2023-04-06T08:02:23","guid":{"rendered":"https:\/\/es-wordpress.fbk.eu\/?p=405"},"modified":"2023-05-09T10:02:29","modified_gmt":"2023-05-09T09:02:29","slug":"nusmv","status":"publish","type":"post","link":"https:\/\/es.fbk.eu\/index.php\/tools\/nusmv\/","title":{"rendered":"NuSMV &#8211; Symbolic Model Checker"},"content":{"rendered":"\n\n\n\n\n\n[et_pb_section fb_built=&#8221;1&#8243; admin_label=&#8221;section&#8221; _builder_version=&#8221;3.22&#8243;][et_pb_row admin_label=&#8221;row&#8221; _builder_version=&#8221;3.25&#8243; background_size=&#8221;initial&#8221; background_position=&#8221;top_left&#8221; background_repeat=&#8221;repeat&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;|||&#8221; custom_padding__hover=&#8221;|||&#8221;][et_pb_text admin_label=&#8221;Text&#8221; _builder_version=&#8221;4.8.2&#8243; background_size=&#8221;initial&#8221; background_position=&#8221;top_left&#8221; background_repeat=&#8221;repeat&#8221; hover_enabled=&#8221;0&#8243; sticky_enabled=&#8221;0&#8243;]<p><!-- divi:paragraph --><strong><a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>\u00a0<\/strong>is a symbolic model checker developed as a joint project between:<\/p>\n<p><!-- \/divi:paragraph --><\/p>\n<p><!-- divi:list --><\/p>\n<ul>\n<li><a href=\"https:\/\/es.fbk.eu\/\">Embedded Systems Unit<\/a>\u00a0in the\u00a0<a href=\"http:\/\/cit.fbk.eu\/\">Center for Information Technology<\/a>\u00a0at\u00a0<a href=\"http:\/\/fbk.eu\/\">FBK-IRST<\/a><\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~modelcheck\/\">Model Checking<\/a>\u00a0group at\u00a0<a href=\"http:\/\/www.cs.cmu.edu\/\">Carnegie Mellon University\u00a0<\/a>, the Mechanized Reasoning Group at\u00a0<a href=\"http:\/\/www.dist.unige.it\/\">University of Genova<\/a><\/li>\n<li>Mechanized Reasoning Group at\u00a0<a href=\"http:\/\/www.dit.unitn.it\/\">University of Trento<\/a><\/li>\n<\/ul>\n<p><!-- \/divi:list --><\/p>\n<p><!-- divi:paragraph --><a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>\u00a0is a reimplementation and extension of\u00a0<a href=\"http:\/\/nusmv.fbk.eu\/bibliography.html#SMV\">SMV<\/a>, the first model checker based on BDDs.\u00a0<a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>\u00a0has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.<\/p>\n<p><!-- \/divi:paragraph --><\/p>\n<p><!-- divi:paragraph -->NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model Checker, which can be connected to the\u00a0<a href=\"http:\/\/minisat.se\/\">Minisat SAT Solver<\/a>\u00a0and\/or to the\u00a0<a href=\"http:\/\/www.princeton.edu\/~chaff\/zchaff.html\">ZChaff SAT Solver<\/a>. The University of Genova has contributed SIM, a state-of-the-art SAT solver used until version 2.5.0, and the RBC package use in the Bounded Model Checking algorithms.<\/p>\n<p><!-- \/divi:paragraph --><\/p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]\n\n\n\n\n\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":1,"featured_media":4490,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"<!-- wp:paragraph -->\n<p><a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>&nbsp;is a symbolic model checker developed as a joint project between:<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:list -->\n<ul><li><a href=\"https:\/\/es.fbk.eu\/\">Embedded Systems Unit<\/a>&nbsp;in the&nbsp;<a href=\"http:\/\/cit.fbk.eu\/\">Center for Information Technology<\/a>&nbsp;at&nbsp;<a href=\"http:\/\/fbk.eu\/\">FBK-IRST<\/a><\/li><li><a href=\"http:\/\/www.cs.cmu.edu\/~modelcheck\/\">Model Checking<\/a>&nbsp;group at&nbsp;<a href=\"http:\/\/www.cs.cmu.edu\/\">Carnegie Mellon University&nbsp;<\/a>, the Mechanized Reasoning Group at&nbsp;<a href=\"http:\/\/www.dist.unige.it\/\">University of Genova<\/a><\/li><li>Mechanized Reasoning Group at&nbsp;<a href=\"http:\/\/www.dit.unitn.it\/\">University of Trento<\/a><\/li><\/ul>\n<!-- \/wp:list -->\n\n<!-- wp:paragraph -->\n<p><a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>&nbsp;is a reimplementation and extension of&nbsp;<a href=\"http:\/\/nusmv.fbk.eu\/bibliography.html#SMV\">SMV<\/a>, the first model checker based on BDDs.&nbsp;<a href=\"http:\/\/nusmv.fbk.eu\/NuSMV\/index.html\">NuSMV<\/a>&nbsp;has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model Checker, which can be connected to the&nbsp;<a href=\"http:\/\/minisat.se\/\">Minisat SAT Solver<\/a>&nbsp;and\/or to the&nbsp;<a href=\"http:\/\/www.princeton.edu\/~chaff\/zchaff.html\">ZChaff SAT Solver<\/a>. The University of Genova has contributed SIM, a state-of-the-art SAT solver used until version 2.5.0, and the RBC package use in the Bounded Model Checking algorithms.<\/p>\n<!-- \/wp:paragraph -->","_et_gb_content_width":"","footnotes":""},"categories":[8],"tags":[],"class_list":["post-405","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-tools","et-has-post-format-content","et_post_format-et-post-format-standard"],"_links":{"self":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/405","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/comments?post=405"}],"version-history":[{"count":9,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/405\/revisions"}],"predecessor-version":[{"id":9222,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/405\/revisions\/9222"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media\/4490"}],"wp:attachment":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media?parent=405"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/categories?post=405"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/tags?post=405"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}