Munta: A Verified Model Checker for Timed Automata

Simon Wimmer 📧

May 22, 2025

Abstract

Munta is a verified model checker for timed automata. It has been described in detail in a PhD thesis [3] and conference publications [4, 2]. This entry supersedes earlier versions of Munta hosted on GitHub.

License

BSD License

Topics

Related publications

  • Wimmer, S., & Lammich, P. (2018). Verified Model Checking of Timed Automata. Tools and Algorithms for the Construction and Analysis of Systems, 61–78. https://doi.org/10.1007/978-3-319-89960-2_4
  • Wimmer, S. (2019). Munta: A Verified Model Checker for Timed Automata. Formal Modeling and Analysis of Timed Systems, 236–243. https://doi.org/10.1007/978-3-030-29662-9_14
  • https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20201209-1576100-1-0

Session Munta_Base

Session Munta_Model_Checker

Depends on

Cite

× 
@article{Munta_Model_Checker-AFP,
  author  = {Simon Wimmer},
  title   = {Munta: A Verified Model Checker for Timed Automata},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Munta_Model_Checker.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download