

                       The Verus Model Checking System
                       ===============================

Sergio Campos -- 1997


What is Verus ?
---------------

Verus is a formal verification tool that allows the 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.


Can I have it ?
---------------

Yes, provided you read and follow the instructions in the license
agreement described in the file license.txt


How do I start ?
----------------

Get the sources for Verus and the BDD library. Install the BDD library
according to its instructions. Then compile Verus and write your own
Verus programs. Sample programs are provided to assist at the
beginning. Some hints on compiling Verus may that may prove useful
follow. The files vmanual.[ps,txt] provide detailed information on the
features supported by Verus. However, we cannot guarantee that Verus
can be compiled on any system, even though it should work without
problems in most Unixes.

. Verus has been originally compiled under Linux. Using a similar
  setup simplifies installation by avoiding most compatibility
  problems.

. In order to compile Verus, some Unix utilities are used, mainly gcc,
  lex, yacc and make. Incompatibilities may arise from using different
  programs. While gcc and make are usually trouble free, lex and yacc
  may cause problems. It seems that in particular lex is very
  sensitive to different versions. Whenever possible the use of flex
  (linux version of lex) and bison (linux version of yacc) is
  recommended.

. Verus uses the BDD library that is distributed with it. The BDD
  library must be installed before compiling Verus.

. The default environment in which Verus is compiled maintains the
  source files in the directory ~/src/verus, and the object files in
  directory ~/obj/verus. If the default environment is used, typing
  mk<enter> should suffice to compile it.  If a different directory
  structure is used the makefile must be changed.


I think Verus is [great,boring,terrible]. Do you want to know why ?
-------------------------------------------------------------------

Yes, we do. Please send comments, suggestions, bug reports and tell us
what you think of it. We also would like to know more about what kind
of applications you want to use Verus for and if you are being
successful or not. It is very important that we receive feedback in
order to make Verus [even greater,more than just boring,worth your
time]. Send comments to:

Sergio Campos -- campos@cs.cmu.edu

or

Edmund Clarke -- emc@cs.cmu.edu

5000 Forbes ave.
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA, 15213, USA.
