Kleene Algebra with Tests and Demonic Refinement Algebras

Title:	Kleene Algebra with Tests and Demonic Refinement Algebras
Authors:	Alasdair Armstrong, Victor B. F. Gomes (vb358 /at/ cl /dot/ cam /dot/ ac /dot/ uk) and Georg Struth
Submission date:	2014-01-23
Abstract:	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.
BibTeX:	@article{KAT_and_DRA-AFP, author = {Alasdair Armstrong and Victor B. F. Gomes and Georg Struth}, title = {Kleene Algebra with Tests and Demonic Refinement Algebras}, journal = {Archive of Formal Proofs}, month = jan, year = 2014, note = {\url{https://isa-afp.org/entries/KAT_and_DRA.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Kleene_Algebra
Used by:	Algebraic_VCs, Hybrid_Systems_VCs
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.