### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Automata and formal languages
- Mathematics/Algebra

### Session KAT_and_DRA

- Test_Dioid
- Conway_Tests
- KAT
- DRAT
- DRA_Models
- KAT_Models
- FolkTheorem
- PHL_KAT
- PHL_DRAT
- KAT2
- DRAT2

### Depends on

- Kleene Algebra

### Used by

- Verification Components for Hybrid Systems
- Program Construction and Verification Components Based on Kleene Algebra

### Auto-related entries

- Putting the `K' into Bird’s derivation of Knuth-Morris-Pratt string matching
- The Irrationality of ζ(3)
- Signature-Based Gröbner Basis Algorithms
- Imperative Insertion Sort
- pGCL for Isabelle

## Cite

×

KAT_and_DRA-AFP

    @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   = {January},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/KAT_and_DRA.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jan 29, 2014 : Isabelle2013-2