TChecker Demos

TChecker is an open source library and tool for model-checking timed automata. This webpage offers an online demo of TChecker that can be used to test the tools on small models.

Please visit the GitHub repository https://github.com/ticktac-project/tchecker to access the source code.

Installation instructions as well as the documentation of tools and tutorials are available from the wiki page.

Please, also consider our companion tool uppaal-to-tchecker that translates UPPAAL models into TChecker models.

TChecker file format is described on this page.