Kleene Algebra with Tests and Demonic Refinement Algebras (Q7361454)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry KAT_and_DRA
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Kleene Algebra with Tests and Demonic Refinement Algebras |
AFP entry KAT_and_DRA |
Statements
23 January 2014
0 references
Alasdair Armstrong
0 references
Victor B. F. Gomes
0 references
Georg Struth
0 references
Kleene Algebra with Tests and Demonic Refinement Algebras (English)
0 references
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.
0 references
