Unbounded-Thread Program Verification using Thread-State EquationsThis webpage describes how to download and use the TSE tool that implements the above technique. Thanks to Konstantinos for helping to design this website.
DependenciesInstall the SMT solver z3 on your system. TSE currently relies on z3 as the backend solver.
Install from source
- git clone the github repository
Using the binaries
- Unpack the TSE binary for your architecture, using the tarball above.
- Make sure TSE finds z3 library.
3. Tool useFor 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.