Skip to main content
TChecker
- Description
- This is TChecker, an open-source model-checker for timed systems. TChecker is written in C++17 and provides a library of classes to describe timed systems, to compute the corresponding timed automata, to compute its semantics, as well as symbolic representations and algorithms to check requirements over timed systems. It also comes with tools to run these algorithms from the command line.
TChecker is intended to serve as a plateform to experiment new data structures and algorithms for the verification and the synthesis of timed systems. The goal of the project is to implement state-of-the-art algorithms as well as benchmarks to evaluate these algorithms, and to share then with the community.
- Use cases
- Modeling and analysis timed systems
- LaBRI contributors
- Frédéric Herbreteau, Gérald Point
- Source code depot
- https://github.com/ticktac-project/tchecker
- Software licenses
- MIT License
- Supported OS
- Linux, MacOS
- More informations
- https://tchecker.labri.fr
Back