Unbounded-Thread Program Verification using Thread-State Equations

This webpage describes how to download and use the TSE tool that implements the above technique. Thanks to Konstantinos for helping to design this website.

1. Download

• Source code on github
• Binaries of TSE for 32bit, 64bit Linux

2. Installation

Dependencies

Install the SMT solver z3 on your system. TSE currently relies on z3 as the backend solver.

Install from source

1. git clone the github repository
2. make

Using the binaries

1. Unpack the TSE binary for your architecture, using the tarball above.
2. Make sure TSE finds z3 library.

3. Tool use

For instructions on how to use TSE, run the tool as follows:

./tse -h [--help]

4. Reproducing experimental results

A summary of our results on this benchmark suite. To convert TTS to Petri Nets we have used both the original implementaion of ttstrans found here, and an implementation by Pierre Ganty. We compare against the following coverability checkers:

• BFC version 2.0.2, available here.
• Petrinizer and IIC, available here
• The eec and ic4pn algorithms of this github release of MIST.

5. Bug reporting

Please send bug reports to us.