TABEC aims at providing a way of checking the emptiness of Timed Automata (TAs), in particular parametric, non-resetting test (nrt) TAs with two clocks and one parameter (this is done by relying on tChecker). TABEC can also be used as a conversion tool from UPPAAL's syntax to tChecker's syntax. Due to the limited scope of our usage, TABEC can convert only a limited set of the possible TAs one can create in UPPAAL.
📖 Check the Wiki to get a deeper overview of TABEC's functionalities.