A Verified Model Checker for the Modal µ-calculus in Coq
Abstract elided by the publisher.
Related papers
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq POPL 2020
- CoqCryptoLine: A Verified Model Checker with Certified Results CAV 2023
- Formalizing, Mechanizing, and Verifying Class-Based Refinement Types ECOOP 2024
- Modal µ-Calculus, Model Checking and Gauß Elimination TACAS 1995
- Incremental Model Checking in the Modal Mu-Calculus CAV 1994
- Faster Model Checking for the Modal Mu-Calculus CAV 1992
- Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems TACAS 2002
- Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus TACAS 1996