Unbounded-Thread Program Verification using Thread-State Equations

This webpage describes how to download and use the TSE tool that implements the above technique.

1. Download

2. Installation


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:

5. Bug reporting

Please send bug reports to us.