SYnchronous MODular Analyzer


Download
The source code for symoda is here. The tool binary for Linux/i686 is here.

Installation
You can find Makefile in the src directory to compile it. SYMODA makes use of multiple third-party tools, which must be installed before you will be able to compile/use it. Download and install these tools for your platform.

YICES:
http://yices.csl.sri.com/

FOCI:
http://www.cadence.com/webforms/cbl_software/index.aspx
(My distribution has FOCI for linux. You will have to replace the lib directory by the files for your platform).

CUDD:
http://vlsi.colorado.edu/~fabio/CUDD/

Modify the entries in the files Makefile.decls and foci.decls to point to your local directories.
Then type "make" in src directory to compile.

Once you have compiled it, you can download the benchmarks from here.

and test it on say model file "a.sil" and property file "a.prp" by:

symoda -r cp -f a.sil -p a.prp

AGR can be invoked by:

(non-circular, multi-component)          symoda -ag nc -f a.sil -p a.prp
(circular, multi-component)                 symoda -ag c -f a.sil -p a.prp

Resources

This technical report, titled "SAT-based Compositional Verification using Lazy Learning", describes the algorithms implemented in the tool.