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

BSD License