SyMP: Symbolic Model Prover

Welcome to the SyMP page!

News

• June 20, 2000 The next version of SyMP came out ( 0.3-beta). The core of the Athena proof system has been completed, the default proof system has abstract interpretation, and the proof manager is optimized to handle large proof trees efficiently (thousands of subgoals). Also, a general-purpose proof search strategies are added to the core.
• December 28, 2000. The new version of SyMP ( 0.2-beta) has been released. This version adds quite a few proof rules in the default proof system, together with lots of bug fixes. It also begins a new proof system Athena specialized in security protocols, which is going to be another implementation of the Athena algorithm developed originally by Dawn Song. This release contains only the parser and typechecker for the Athena input language.

Download SyMP

SyMP is distributed as SML source code. To compile it you must have gcc, GNU make, Perl version >= 5, CMU SMV version >= 2.5.3 or compatible, and SML of NJ version >= 110 installed on your system. You also need GNU Emacs (preferred), or XEmacs to run the interactive SyMP prover.

SyMP has only been tested under Linux, but it should also work on other UNIX platforms where the required components are installed.

Download the latest release of SyMP as a gzip'ed tar file. This is usually a more stable version, however, it may not yet contain the latest updates and bug fixes.

The most recent (but possibly less stable) version can be obtained directly from the CVSWeb Repository, or download the latest daily snapshot.

SyMP Releases

symp.0.3-beta.tar.gz (667KB, June 20, 2001)  The core of the Athena proof system has been completed, the default proof system has abstract interpretation, and the proof manager is optimized to handle large proof trees efficiently (thousands of subgoals). Also, a general-purpose proof search strategies are added to the core.

symp.0.2-beta.tar.gz (486KB, December 28, 2000) This version adds quite a few proof rules in the default proof system, together with lots of bug fixes. It also begins a new proof system Athena specialized in security protocols. This release contains only the parser and typechecker for the Athena input language.

symp.0.2-alpha.tar.gz (415KB, August 14, 2000) This version introduces the prover engine, and the emacs-based interactive user interface, somewhat similar to PVS. It still lacks a lot of planned functionality, and we are working hard on it. We are alpha-releasing this version mostly to show where the development is going to.

symp.0.1-alpha.tar.gz (280KB, Jan 30, 2000) This is a very preliminary release, mostly to let the users look at the manual and play with the input language a bit. The program works as a translator from SyMP default language to SMV.

SyMP should run on any platform that has gcc and SML of New Jersey (version 110 or higher) installed. We only tried it under Linux.

To install SyMP, download the latest distribution above and unpack it with

gunzip -c symp.0.3-beta.tar.gz | tar xf -

SyMP Manuals

The SyMP User's Guide (gzip'ed Postscript, 59K) - a `must read' for anyone who wants to use the tool.

The SyMP Language Reference Card (gzip'ed Postscript, 14K)

The SyMP Hacker's Manual (gzip'ed Postscript, 121K). This is essentially, the formal semantics of the language and a high level description of all algorithms used in the implementation in the form of inference rules. You need this only if you want to understand and/or modify the source code.

SyMP man page - UNIX manual page in HTML format.

README file from the distribution

What is SyMP?

SyMP stands for `Symbolic Model Prover' and is a general purpose hardware-oriented specification language written in Standard ML'97 (SML/NJ). 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 name `Model Prover' is a preliminary term we use for a tool that adds some theorem proving techniques to the main model checking procedures in a single framework. Mathematically, the verification problem remains the same as in model checking: given a model, prove that it satisfies a given property. However, the term `Model Checking' usually assumes that such a proof is done automatically (checking tends to means checking algorithmically). Despite several breakthroughs in the past decade, the average size of a model that can be automatically verified is still hardly larger than 10¹⁰⁰ states, which, though larger than the number of protons in the Universe, still does not go far beyond 300 bits of state variables. This figure is absurdly small compared to the size of a typical modern microprocessor consisting of tens or even hundreds of millions of transistors implementing millions of gates. For those designs the use of intricate abstractions, and thus, some theorem proving, is inevitable. This, of course, makes the verification task not as automatic, and therefore, cannot be called just `model checking'. It is also not a general theorem proving, since we prove the properties relative to a specific model, and not in general. We will refer to this set of techniques as `Model Proving'.

The SyMP tool is designed to support most of the existing model proving techniques. It has a clean and, hopefully, unambiguous input language based on ML. It is also open for many extensions, so that many new verification methodologies can be implemented in it relatively easily. SyMP is best viewed as a front-end to other lower-level techniques, such as explicit state model checking, BDDs, SAT and other decision procedures. The back-end APIs will be well-defined, and probably even customizable. In short, it is designed to be `researcher-friendly' in as many ways as possible.

The SyMP language is largely based on ML. There are several reasons for this choice. First, a functional strongly typed language is the best suited for theorem proving; and ML was specifically designed for this purpose. Since we have to use elements of theorem proving, it is an important consideration. ML does not make the model checking part more difficult, on the contrary, many constructs can be expressed in ML much more elegantly than, say, in SMV. Higher-order functions with pattern matching alone can dramatically reduce the size of the program, and at the same time increase its readability. SyMP is type-safe, thus, there will be no `run-time' errors due to type mismatches which are annoying and often difficult to debug. In addition, very popular symmetry reduction is the best expressed through symmetric or uninterpreted types, and thus, a good type system is a bare necessity for the language. From the implementation point of view, ML is a small yet very expressive language with clean semantics, which makes it easier to implement compared to real-world HDL languages like Verilog or VHDL. Also, guaranteed type correctness allows a more efficient binary encoding of a model into BDDs, which surely helps to increase the efficiency of verification. And the last, but not the least reason is that we like ML. So, here we are.

The tool does not have a built-in model checker. Instead, it uses an existing model checker. Currently we only support SMV as a back-end. The `higher-level' procedures that will make SyMP a true `model prover' will gradually be included in the preprocessing stage before passing the problem to the back-end model checker. Other specification or HDL languages like Verilog can also be translated into SyMP and serve as front-ends.

Authors and Developers

Happy Model Proving!

CMU-SCS Model Checking home page

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