DESCRIPTION

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++.

DOWNLOADS

Current version is 1.0 and is available for Linux and Solaris as statically linked binaries:

• tip.linux.static.1.0.gz
• tip.solaris.static.1.0.gz

• mv2.linux.static.1.0.gz
• mv2.solaris.static.1.0.gz
• circ2smv.linux.static.1.0.gz
• circ2smv.solaris.static.1.0.gz

BENCHMARKS

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.

• TipSuite_unmangled.tar.gz   (4.19 MB compressed, 43.76 MB uncompressed)
• TipSuite_mangled.tar.gz   (2.95 MB compressed, 17.55 MB uncompressed)

	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.

REFERENCES

[BCCZ99] 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.

[Eijk98] C.A.J. van Eijk. ``Sequential equivalence checking without state space traversal'' in Proc. Conf. on Design, Automation and Test in Europe, 1998.

[ES03] N. Eén, N. Sörensson ``Temporal Induction by Incremental SAT Solving'' First International Workshop on Bounded Model Checking, ENTCS issue 4 volume 89.

[SSS00] 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.