Model Checking @CMU
[Home]

[People]

[Software]

[Publications]

[Support]

 [Links]

[Internal]

 

The SMV System

SMV for NT

I hope you know what to do with these ones... Thanks to Dong Wang for porting SMV to NT.
smv-nt2.5.zip - version 2.5.0 (July 30, 1998)
smv-nt.zip - version 2.4 (June 24, 1998)

New releases of SMV 2.5 are available. 

For more information on what is new download the sources and read the NEW file.

Source Code

The entire distribution of SMV software in gzipped tar format is available below (by releases). We have paused the development for now:

* smv.r2.5.4.3.tar.gz (216K)  Added 11/19/2001. A small error in the manual (grammar of until was wrong). Also, on internal errors SMV will print its version.
* smv.r2.5.4.2.tar.gz (214K) Added 11/01/2001. A few minor bug fixes, a couple of more options added related to dynamic variable reordering (see man the page). Also, a couple of small updates to the manual have been made - thanks to Andras Horvath and Hernan Eguiluz for the feedback on that!
* smv.r2.5.4.tar.gz (213K) Added 06/11/2000. The newly updated manual is now bundled with the distribution.
* smv.r2.5.3.1d.tar.gz (78K) Added 23/04/99. Fixed a small typo in input.m4.
* smv.r2.5.3.1c.tar.gz (78K) Added 23/03/99. Man pages are updated (finally!). Also added -reorderfactor option.
* smv.r2.5.3.1b.tar.gz (78K) Added 10/20/98, updated 02/11/99. Fixed a bug in printing specs and error messages.
* smv.r2.5.3.1.tar.gz (78K) Added 10/18/98 with some moderately significant changes and more bugs fixed (e.g., smv -early -inc -cp doesn't seg. fault any more).
* smv.r2.5.3.tar.gz (77K) Added 08/27/98. Has PRINT feature for printing BDDs as formulas.
* smv.r2.5.1.1.tar.gz (58K)
* smv.r2.5.0.tar.gz (58K) This is a considerable improvement from 2.4

SMV Manual

The updated manual is available as a Postscript file. Note, that it is now bundled with the SMV distribution. So, if you already got the latest SMV tarball, you don't need to download the manual separately.

smvmanual.ps (499K)
smvmanual.ps.Z (compressed, 192K)
smvmanual.ps.gz (gzip'ed, 129K)
Many thanks to Tatsuhiro Tsuchiya from Osaka University, Japan, for extracting the SMV manual from the original postscript file and restoring the latex sources!

Binaries

Some precompiled binaries are available for SMV 2.5.3.1e (gzipped and plain versions)

SPARC (SunOS4): smv-sun4.gz(125K), smv-sun4(484K)
SPARC (SunOS5, Solaris): smv-solaris.gz(102K), smv-solaris(263K)
Intel x86 (Linux) smv-linux.gz(110K), smv-linux(294K)
DECstation (Ultrix) smv-pmax.gz(110K), smv-pmax(313K)
Clicking on the references above retrieves the files automatically. You may need to press <Shift> key and click on the file to save it to disk in browsers like Netscape. I

The file smv.r2.5.4.tar.gz (in gzip'ed "tar" format) contains the sources and some examples. To break out the directory structure, after you have gotten the files, use the commands

gunzip smv.r2.5.4.tar.gz
tar -xf smv.r2.5.4.tar
The file smv/doc/smvmanual.ps gives an introduction to the language and the model checker in postscript format. The examples from the manual can be found in the subdirectory examples. The manual does not cover the temporal logic CTL, or model checking algorithms.

Emacs interface and VIM syntax highlighting

If you are at CMU in Computer Science Department, most likely emacs mode for SMV is already installed on your machine. Add these lines to your ~/.emacs file to make it load automatically when you open an .smv file: 

(add-to-list 'load-path "/usr/local/lib/smv")
(autoload 'smv-mode "smv-mode" "SMV mode." t)
(add-to-list 'auto-mode-alist '("\\.smv$" . smv-mode))
(add-to-list 'auto-mode-alist '("\\.ord$" . smv-ord-mode))
(add-to-list 'completion-ignored-extensions ".ord")
(add-to-list 'completion-ignored-extensions ".opt")
Outside CMU, download the following files and follow the instructions in the comments.

  • smv-mode.el - emacs library that provides an SMV interface (last updated: Mar 23, 1999.)
  • .vimrc - resorce file for the latest versions of the VI editor (VIM)
Emacs library provides a convenient user interface to SMV, does smart syntax highlighting and simple indentation (TAB key). When you install it, type `C-h m' in any SMV buffer to get the list of features and key bindings.

smv-mode.el is now included in the SMV distribution, so you can get the latest version from there.

VIM script also does syntax highlighting, but this editor doesn't support inferior processes yet.

These are both experimental libraries, and any bug reports or suggestions are welcome!

SMV acronym

Besides Symbolic Model Verifier, SMV also stands for:

CMU-SCS Model Checking home page

Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.