The TickTac project aims to design efficient algorithms and softwares for the analysis of timed automata.

We are developing several open-source softwares:

• TChecker is a framework for the implementation of verification algorithms for real-time systems. In particular, it proposes a command-line tool that implements a covering reachability algorithm (see the wiki page using tchecker).
• tcltl is an LTL model-checker based on the TChecker library and Spot. TChecker is used to produce the state-space of the system while Spot checks the satisfiability of the LTL formula.
• uppaal-to-tchecker can be used to translate Uppaal models into TChecker file format.

The project is also proposing a benchmark of test-cases.