Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Kleene Algebra with Tests and D...


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC