### Abstract

Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Algebraic_VCs

- VC_KAT_scratch
- VC_KAD_scratch
- P2S2R
- VC_KAT
- VC_KAT_Examples
- VC_KAT_Examples2
- RKAT
- RKAT_Models
- VC_RKAT
- VC_RKAT_Examples
- VC_KAD
- VC_KAD_Examples
- VC_KAD_Examples2
- VC_KAD_dual
- VC_KAD_dual_Examples
- VC_KAD_wf
- VC_KAD_wf_Examples
- Path_Model_Example
- Pointer_Examples
- KAD_is_KAT
- Domain_Quantale

### Depends on

- Kleene Algebras with Domain
- Kleene Algebra with Tests and Demonic Refinement Algebras

## Cite

×

Algebraic_VCs-AFP

    @article{Algebraic_VCs-AFP,
      author  = {Victor B. F. Gomes and Georg Struth},
      title   = {Program Construction and Verification Components Based on Kleene Algebra},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Algebraic_VCs.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
- Jun 18, 2016 : Isabelle2016