KAT-ML: an interactive theorem prover for Kleene algebra with tests. We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT (SKAT). We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Uramoto, Takeo: Canonical finite models of Kleene algebra with tests (2016)
- Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
- Armstrong, Alasdair; Struth, Georg; Weber, Tjark: Program analysis and verification based on Kleene algebra in Isabelle/HOL (2013)
- Foster, Simon; Struth, Georg; Weber, Tjark: Automated engineering of relational and algebraic methods in Isabelle/HOL (invited tutorial) (2011)
- Prisacariu, Cristian: Synchronous Kleene algebra (2010)
- Solin, Kim: A sketch of a dynamic epistemic semiring (2010)
- Solin, Kim; von Wright, Joakim: Enabledness and termination in refinement algebra (2009)
- Aboul-Hosn, Kamal; Kozen, Dexter: Local variable scoping and Kleene algebra with tests (2008)
- McIver, A.K.; Gonzalia, C.; Cohen, E.; Morgan, C.C.: Using probabilistic Kleene algebra pKA for protocol verification (2008)
- Aboul-Hosn, Kamal; Kozen, Dexter: KAT-ML: an interactive theorem prover for Kleene algebra with tests (2006)