Abstract
Munta is a verified model checker for timed automata.
This entry presents Muntac, an extension of Munta that can check certificates
for Büchi and reachability properties generated by other model checkers.
This work has been described in detail in a PhD thesis [2]
and conference publications [3,4].
This entry supersedes earlier versions of Muntac hosted on GitHub.
License
Topics
Related publications
- Wimmer, S., & Mutius, J. von. (2020). Verified Certification of Reachability Checking for Timed Automata. Tools and Algorithms for the Construction and Analysis of Systems, 425–443. https://doi.org/10.1007/978-3-030-45190-5_24
- Wimmer, S., Herbreteau, F., & van de Pol, J. (2020). Certifying Emptiness of Timed Büchi Automata. Formal Modeling and Analysis of Timed Systems, 58–75. https://doi.org/10.1007/978-3-030-57628-8_4
- https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20201209-1576100-1-0
Session Munta_Certificate_Checker
- More_Graph_Theory
- Graph_Library_Adaptor
- Lasso_Freeness_Certificates_Complete
- Simulation_Graphs_Certification
- Unreachability_Misc
- Unreachability_Certification
- Unreachability_Certification2
- Simulation_Graphs2
- TA_Simulation
- Normalized_Zone_Semantics_Certification
- Normalized_Zone_Semantics_Certification_Impl
- Normalized_Zone_Semantics_Certification_Impl2
- Extract_Certificate
- Simple_Network_Language_Certificate
- Simple_Network_Language_Certificate_Checking
- Simple_Network_Language_Certificate_Code
- Munta_Certificate_Testing
- Munta_Certificate_Compile_MLton
- Munta_Certificate_Compile_Poly