An SMV Trial

Write a short program in the window, choose options and run it! To get started, try a simple example first. See the guided tour to get a flavor of the language. You can read more about SMV input language in the SMV manual (compressed postscript, 56K).

Please, do not run big programs on this server. This page is intended for demonstration, and any abuse will force me to close or severely restrict this service. At this point you are given 4Mb of RAM + 2Mb of stack and 1 minute of user CPU time on Pentium II 450MHz.

Although these seem to be quite modest resources for a model checker, they are a way more than enough for any demonstration. In fact, using a proper variable ordering, I was able to verify a (nontrivial!) part of the digital autopilot of the Space Shuttle using up less than a quater of the resources provided.

If you want to use SMV in your project, download the SMV software to your local machine.

Cache size: Key Table size:

Forward search Report number of states Output the variable ordering (not avail. yet)
Verbose level: None 1 2

Number of runs is 19 (before Feb. 12).

Sergey Berezin / 

  CMU-SCS Model Checking home page

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