Kleene Algebra with Tests and Demonic Refinement Algebras.
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth · 2014
We formalise Kleene algebra with tests (KAT) and demonic refine-ment algebra (DRA) in Isabelle/HOL. KAT is relevant for program verification and correctness proofs in the partial correctness setting. While DRA targets similar applications in the context of total cor-rectness. Our formalisation contains the two most important models of these algebras: binary relations in the case of KAT and predicate transformers in the case of DRA. In addition, we derive the inference rules for Hoare logic in KAT and its relational model and present a simple formally verified program verification tool prototype based on