SVISS: Symbolic Verification of Symmetric Systems

SVISS (historically, "Symbolic Verification of Invariants of Symmetric Systems") is an experimentation platform incorporating efficient symmetry reduction into symbolic model checking. The tool includes an extensive C++ library for system modeling using BDDs and a rich CTL model checking engine. Applications range from communication protocols to computer hardware and multi-threaded software.

You can view SVISS' documentation, read a short paper about it or (for the impatient) view some screenshots.

Downloading SVISS

To obtain and install a copy of the SVISS verifier, proceed as follows:

1. Download a copy of the source code archive sviss.tgz (which also includes a copy of the CUDD BDD library) into a fresh directory.

    NOTE: Please use the version of the CUDD library included with SVISS. It is identical
    to the one available from the original author, Fabio Somenzi, except that it fixes some
    problems with inline functions in the C++ extension to CUDD, and it collects all include
    files in one directory and all libraries in another directory.

2. Unpack the tool. With GNU tar:

tar xzf sviss.tgz

3. Now follow the instructions in the README file of the SVISS directory to compile the tool.

Last update: Thu Apr 3 14:08:23 CET 2008