Verified Model Checking of Timed Automata -- Artifact

This dataset, corresponding to the TACAS 2018 submission"Verified Model Checking of Timed Automata", contains source code, dependencies and instructions to build the tool described, as well as the benchmarks used to evaluate it.
The tool presented here, munta, constitutes a fully verified model checker for timed automata, a widely used formalism for modeling real-time systems. munta is not intended to replace existing model checkers, but rather a sufficiently performant reference implementation against which other implementations can be validated. It also aims for high feature compatibility with the state-of-the-art model checker Uppaal.
munta is implemented in Standard ML using the proof assistant Isabelle/HOL.
munta's source code is provided in the directory munta. The sub-directory benchmarks contains the standard benchmark models used to evaluate the tool, as described in section 6 of the related manuscript. Benchmarks are implemented in minimally pre-processed Uppaal bytecode.
The open-source Standard ML compiler mlton must be installed in order to run munta. A copy of this is provided in the directory mlton.
Sources included in the munta directory can be viewed interactively in Isabelle. In order to do so, Isabelle and the AFP must be installed. These are provided in the directories Isabelle2017 and afp respectively.
Detailed installation instructions are provided in README.md.