Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Muntac: A Verified Certificate...

Email Gateway (Oct 20 2025 at 16:45):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Another nice contribution on timed automata model checking by Simon Wimmer:

Muntac: A Verified Certificate Checker for Timed Automata

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.
https://www.isa-afp.org/entries/Munta_Certificate_Checker.html

Enjoy!

--

Peter

Last updated: Nov 09 2025 at 20:21 UTC