The SMV System
Dong Wang for porting SMV to NT.
New releases of SMV 2.5 are available.For more information on what is new download the sources and read the NEW file.
Source CodeThe entire distribution of SMV software in gzipped tar format is available below (by releases). We have paused the development for now:
SMV ManualThe 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.
Many thanks to Tatsuhiro Tsuchiya from Osaka University, Japan, for extracting the SMV manual from the original postscript file and restoring the latex sources!
BinariesSome precompiled binaries are available for SMV 188.8.131.52e (gzipped and plain versions)
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
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 highlightingIf 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 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 acronymBesides Symbolic Model Verifier, SMV also stands for:
Please send any comments and suggestions to Nishant Sinha - (nishants) at cs dot cmu dot edu.