This is an experimental SyMP implementation in SML'97. VERSION: 0.3-beta NAME 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'. RUN The tool is best run interactively from emacs. There is a limited command-line interface, but it is not supported, at least not in this release. INSTALLATION You need around 20MB of free disk space for compilation, and, in addition, 5MB of space for the installation. Unpack the distribution: gunzip -c symp.0.3-beta.tar.gz | tar xf - This will create a directory named `symp'. Change to that directory and compile the SML image. You must have gcc and SML of New Jersey version >= 110 but no greater than 110.9.1 installed on your system. (The more recent versions of SML/NJ have a different interface to the complilation manager, which doesn't have much documentation and seems to be unstable. It will be supported in the future releases.) cd symp ./configure make - to make all necessary files for interactive loading in sml; make install - to install the SML image and the startup script. By default, `make install' will install SyMP files in /usr/local/{bin,symp,doc/symp,man/man1,share/emacs/site-lisp} . You can change the installation directories in several ways. o Run ./configure with --prefix=/new/path (and, similarly, --bindir). See the output of ./configure --help for more options. o Edit the `prefix' and/or `bindir', `sympdir', etc. variables in the "Makefile", or o Give extra parameters to `make'. For instance: make install prefix=/opt/local will install SyMP files in /opt/local/bin, /opt/local/symp, /opt/local/doc/symp, /opt/local/share/emacs/site-lisp, and /opt/local/man/man1. NOTE: if you modify `prefix' at `make install' time, the SyMP scripts and binaries will still be looking for the other components in /usr/local (or the path specified with ./configure --prefix=...). Use this method only if you are installing SyMP with a package manager like `stow' or `depot' which would later set up the appropriate symlinks to make SyMP appear under /usr/local. Installing the Emacs Library. Symp has its own mode in emacs. To install it, just add the following lines to your ~/.emacs file: ;;;; SyMP mode (add-to-list 'load-path "/usr/local/share/emacs/site-lisp") ;; Default proof system (autoload 'symp-mode "symp-mode" "SyMP specifications editing mode." t) (add-to-list 'auto-mode-alist '("\\.symp$" . symp-mode)) ;; Athena proof system (autoload 'symp-athena-mode "symp-athena-mode" "SyMP specifications editing mode." t) (add-to-list 'auto-mode-alist '("\\.ath$" . symp-athena-mode)) ;;;; End of SyMP mode If you installed SyMP in a different directory, edit the first line accordingly. If your emacs already has this path in its load-path, then this line is not necessary. SyMP is best run from within emacs. Open a file with the extension `.symp' or `.ath'. The buffer should switch to the appropriate SyMP mode automatically. Then `C-c C-t' starts the SyMP server as an inferior emacs process, which will parse and typecheck the program. You can also start the server without running the typechecker by `C-c C-s'. `C-c C-p' starts a new prover on a theorem. If the theorem you specify already has an active prover, the corresponding prover's buffer will be brought on top. For more information on the SyMP mode, run `C-h m' in the SyMP emacs buffer. This version of SyMP does NOT support command line interface. We plan to add it in the future for running the tool from scripts in a batch mode. FEATURES 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. CHANGES FROM 0.2-beta RELEASE o New general-purpose strategies for automatic proof search. o The proof manager is optimized, and large proof trees (thousands of subgoals) do not seem to slow down its performance anymore. o Added a few more rules to the default proof system, and weeded out tons of new bugs; in particular, the new abstract_split rule implements the "case splitting" and abstract interpretation of datatypes. o Completed the main core of the Athena proof system (for security protocols). BUGS 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: * The default proof still contains too few rules. This is not exactly a bug, but we are constantly working on it to make the tool more usable. (It carries over from the previous release :) * The manual is in a very alpha stage, pretty much like the tool itself. It describes most of what you need to start using both proof systems, but not much more. We are also working on it. * Some proof rules in the default system are not quite correct. The replace rule will not replace everything that it should in the model (due to its being too conservative in preserving soundness). The typechecker still breaks quite often as soon as we try some new example. Eventually, it should be rewritten in a much cleaner way, it is virtually impossible to debug it completely as it is now. WHERE TO GET SyMP CMU Model Checking Page: 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. CVS-Web Repository: http://teapot.modck.cs.cmu.edu/symp/ Here you can download the latest (but probably unstable) daily CVS snapshot of the tool. AUTHORS Main author: Sergey Berezin, Carnegie Mellon University. sergey.berezin@cs.cmu.edu, Co-developer: Alex Groce, Carnegie Mellon University. agroce+@cs.cmu.edu. June, 2001