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 Cam I program, which is added as a safe decision procedure to the system. We thereby avoid the generation of large proof objects while preserving the high reliability of the proof environment. An example illustrates the combination of model checking with deductive techniques.
Cite
CITATION STYLE
Sprenger, C. (1998). A verified model checker for the modal µ-calculus in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1384, pp. 167–183). Springer Verlag. https://doi.org/10.1007/bfb0054171
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
