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.
Number of runs is
Sergey Berezin / berez+@cs.cmu.edu
