Verus

Below you can download the code of Verus. Be sure to get both BDD library and and the actual Verus code.

Download Verus


What is Verus ?

Verus allows the formal specification and verification of real-time and other time critical systems. It can also be applied to several types of untimed software and hardware applications. The system being verified is specified in the Verus language and then compiled into a state-transition graph. Algorithms derived from symbolic model checking are used to compute quantitative information about the model. A CTL symbolic model checker is also provided to assist in the verification. The Verus language has been especially designed to allow a straightforward description of the temporal characteristics of programs. The information produced allows the user to check the temporal correctness of the model: schedulability of the tasks of the system can be determined by computing their response time; reaction times to events and several other parameters of the system can also be analyzed by this method. This information provides insight into the behavior of the system and in many cases it can help identify inefficiencies and suggest optimizations to the design. The same algorithms can then be used to analyze the performance of the modified design. The evaluation of how the optimizations affect the design can be done before the actual implementation. This can significantly reduce development costs.

To break out the directory structure, after you have gotten the files, use the commands

gunzip -c bddlib.tar.gz | tar xf -
gunzip -c verus0.9.tar.gz | tar xf -

CMU-SCS Model Checking home page

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