KAT-ML

MaRDI QIDQ20515swMATHFDO

Official website http://www.cs.cornell.edu/Projects/KAT/

Described by source

• KAT-ML: an interactive theorem prover for Kleene algebra with tests

Cited in

(12)

• RALL
• GUItar
• PDCoq
• Deciding Kleene algebra terms equivalence in Coq
• Canonical finite models of Kleene algebra with tests
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Synchronous Kleene algebra
• Enabledness and termination in refinement algebra
• Local variable scoping and Kleene algebra with tests
• Using probabilistic Kleene algebra pKA for protocol verification
• A sketch of a dynamic epistemic semiring

This page was built for software: KAT-ML