Email Gateway (Aug 19 2022 at 13:23): Email Gateway (Aug 19 2022 at 13:23):From: Tobias Nipkow <nipkow@in.tum.de>
Kleene Algebra with Tests and Demonic Refinement Algebras
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
We formalise Kleene algebra with tests (KAT) and demonic refinement
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 correctness. 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 the algebraic approach.
http://afp.sourceforge.net/entries/KAT_and_DRA.shtml
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC