[isabelle] New AFP entry: Kleene Algebra with Tests and Demonic Refinement Algebras



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!




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.