SyMP - Symbolic Model Prover
symp [ options ] input-file
SyMP stands for Symbolic Model Prover, and is a general purpose prover generator for generating special purpose theorem provers in various application domains. The core of the tool is a generic prover which is connected to several proof system modules. Each such module defines an input specification language, a proof system, and a rule application mechanism, and the generic prover provides all the proof management and an interactive user interface.
Currently, SyMP has two proof systems: the default and Athena.
The default proof system implements a general framework for combining model checking and theorem proving, and has a hardware-oriented specification language that resembles SML. Programs in the default input language should be saved in files with extension `.symp'. The main purpose of the language is to provide a convenient environment for fast and clean prototyping of new (mostly hardware) verification methodologies based on model checking with some elements of theorem proving. It can also be used as an intermediate representation in translations between other specification languages.
The Athena proof system is specialized in verifying security protocols, and is based on Strand Spaces and the algorithms developed for them by Dawn Song. We believe, it is fairly complete at this point, however, the automatic proof search is not as good as it should be yet. File extension for the Athena programs is `.ath'.
The tool is best run interactively from emacs. There is a limited command-line interface, but it is not supported, at least in this release.
Generate a transition system for the spec (theorem). Specs are full SyMP theorem expressions. There can be several --spec instances in one call.
modelchecker name - the name of the back-end model checker. Currently, only `smv' is supported, and is the default.
the name of the output file. A dash `-' means stdout. default is `out.smv'. This is a temporary option before the call to the back-end model checker is automated.
set the threshold on the type size after which the type is considered too large or infinite for translation purposes.
print a version string and exit
print this help and exit
verbose mode
quiet mode (default)
dump (a lot of!) debug output where debug-spec stands for:
dump all possible debug info
print debug info only for the functions f1, f2, etc.. The function names must be separated by commas or spaces, but in the latter case they must be enclosed in quotes.
Read the README file in the distribution.
SyMP is now considered relavitely mature as a general purpose prover generator. It provides a well-defined API to custom-built proof systems, the unified proof management mechanism, and the abstract layer of the interactive user interface. Concrete user interface modules are plugged in through another well-defined API. The reason it is still in beta is because the provided proof systems modules are still being developed. The core of the tool, however, is reasonably stable and hasn't changed much from the previous version.
Currently, SyMP has two proof systems: the default and Athena. The only interactive user interface is implemented in Emacs. The default proof system implements our general idea of a ``model prover'' with many theorem proving as well as model checking and abstraction capabilities built-in. The Athena proof system is designed for security protocols verification, and is believed to be a complete implementation of what is described in our original journal paper.
For more features, read the User's Guide and the BUGS section below.
The central core (proof manager, user interface, etc.) seems to be rather stable, and no new bugs were discovered from the previous release, even after a few small optimizations.
The Athena proof system probably still have some bugs, but we haven't seen any for a few days. Anyway, this code is pretty new and should be considered alpha-stage.
However, there are plenty of bugs in the default proof system, and we are working on them. To mention a few:
If you find a serious bug, please report it to sergey.berezin@cs.cmu.edu .
http://www.cs.cmu.edu/~modelcheck/symp.html. It is highly recommended that you download the latest release of the tool and upgrade often, as we are in the process of rapid developement, and a lot of bug fixes and improvements are under way.
http://teapot.modck.cs.cmu.edu/symp/ Here you can download the latest (but probably unstable) daily CVS snapshot of the tool.
Sergey Berezin, Carnegie Mellon University. sergey.berezin@cs.cmu.edu,
Alex Groce, Carnegie Mellon University. agroce+@cs.cmu.edu.
June 2001