This page is devoted to the tool Tip described in [ES03]
Tip is prover for safety properties of finite state machines provided in the
SMV-format. Only non-hierarchical, all-boolean descriptions are supported. The prover is based on
induction methods [SSS00], which can be seen as the combination of establishing an
upper-bound of a shortest counter-example, and looking for counter-example essentially by
BMC methods [BCCZ99]. Built into Tip is the state-of-the-art SAT-solver Satzoo, which supports incremental SAT-solving.
The first version of Tip was written by Niklas Sörensson using a mixture of C++ and Haskell.
The current version by me (Niklas Een) is written entirely in C++.
Current version is 1.0 and is available for Linux and Solaris as statically
Related software: The conversion tool mv2 converts BLIF-mv files to a number of
other formats. Currently that number is one, the "circ" format (used by my old tool FixIt),
so you may want to download circ2smv as well.
The test-suite used in [ES03] is available in two versions: one with the original names, and
one with the named mangled into short names to save space. All problems are on flat SMV-format and
contain one AG property each.
Each problem is tagged with its source:
| || cadence || - || Example files from the Cadence SMV distribution. |
| || cmu || - || Example files from the CMU SMV distribution. |
| || ken || - || SMV case studies from Ken McMillan's web-page. |
| || nusmv || - || Example files from the NuSMV distribution. |
| || vis || - || Example files from the VIS distribution. |
| || texas || - || The Texas 97 benchmarks available from Berkeley University. |
| || eijk || - || ISCAS'89 sequential equivalence checking from [Eijk98]. |
| || irst || - || Problems from the Model Checking Group at IRST. |
and with the flattening method used:
| || B || - || Converted by Armin Biere's tool SmvFlatten. |
| || N || - || Converted by NuSMV's "write_boolean_model" command. |
| || C || - || Converted by Cadence SMV using the '-bmc' option. |
| || E || - || Converted by my tool mv2. |
| || S || - || Converted by tailor-made software of Niklas Sörensson. |
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu
``Symbolic model checking without BDDs''
in Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems,
LNCS:1579, Springer-Verlag 1999.
C.A.J. van Eijk.
``Sequential equivalence checking without state space traversal''
in Proc. Conf. on Design, Automation and Test in Europe, 1998.
N. Eén, N. Sörensson
``Temporal Induction by Incremental SAT Solving''
First International Workshop on Bounded Model Checking, ENTCS issue 4 volume 89.
M. Sheeran, S. Singh, G. Stålmarck
``Checking safety properties using induction and a SAT-solver''
in Formal Methods in Computer Aided Design, LNCS:1954, Springer-Verlag 2000.
© Copyright Niklas Eén, 2003