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