SMV

By selecting almost any of these links, you will be leaving NIST web space. We provided these links because they may have information of interest to you. No inferences should be drawn because some sites are referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the assertions presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites. Please address comments about this page to paul.black@nist.gov.

SMV (Symbolic Model Verifier) is a model checker that uses CTL (Computation Tree Logic). The input is a state machine model and temporal logic formulas. SMV checks that the formulas are consistent with the model. In some cases SMV can (and does) report a trace or counterexample when an inconsistency is found. This page has resources about SMV.

The definitive book is Kenneth L. McMillan Symbolic Model Checking, Kluwer Academic Publishers, 1993. It is a revised edition of McMillan's 1992 doctoral dissertation.

NuSMV

NuSMV is an open source reimplementation and extension of SMV available at http://nusmv.irst.itc.it/.

Cadence

Cadence Berkeley Labs has a commercial version of SMV called FormalCheck. Since they "continue to use SMV as a research platform", they "will continue to make SMV available on the web". You can download their free SMV after registering.

CMU SMV

CMU's model checking doesn't seem to be active. The latest update is November 2001. They have other model checkers and software.

They have a short introduction to model checking with SMV. You can get source code, binaries, etc.

Other Model Checkers

There are many, many other model checkers based on other logics and working with different specification languages. SMV is just what we use in our Automatic Test Generation from Formal Specifications (AFTG) project.

Created Thu May 22 11:36:09 2003

This page's URL is /~black/FTG/smv.html