Abstract. We report on the formalisation and correctness proof of a model checker for the modal -calculus in Coq's constructive type theory. Using Coq's extraction mechanism we obtain an executable Caml program, which is added as a safe decision procedure to the system. An example illustrates its application in combination with deduction.
The first verification of a model checker we are aware of is by Sprenger for the modal µ-calculus in Coq REF .
A Verified Model Checker for the Modal µ-calculus in Coq
TACAS
Computer Science