Extensions Of Kleene Algebra For Program Verification

Other Titles


Kleene algebra (KA) is an algebraic system that captures completely the laws of equivalence for regular expressions. It is also useful for reasoning about a multitude of computationally interesting structures. Of central interest in KA is a "star" operation that typically describes some kind of repetition or iteration. A combination of Kleene algebra with Boolean algebra has been proposed under the name of Kleene algebra with tests (KAT). This logical system can model the conventional programming constructs of imperative iterative programs, e.g. while loops and conditionals, and it has proven useful for various program verification tasks. In this dissertation we investigate variations and extensions of KA and KAT that are useful for program verification and for reasoning about mathematical structures that appear in computer science. At a technical level, we are interested in establishing completeness theorems, which assert that a proposed logical system is strong enough to capture all properties that are true in a mathematical structure or in a class of mathematical structures. Such results assure us of the quality of a logical system, and their proof often (certainly for the systems that we study here) reveals a systematic way of creating proof objects that certify properties of interest. The first part of this thesis explores generic extensions of KA and KAT with extra equational assumptions. Such extensions are meant to capture in the context of program verification some crucial properties of the domain of computation. We present a very general completeness meta-theorem that instantiates into several useful concrete completeness results. The second part focuses on extensions of KAT with extra mutable state that enable many useful semantics-preserving program transformations. The transformations we intend to cover are motivated by classical examples from the area of program schematology. We offer a rigorous and mathematically appealing algebraic approach, which replaces the typical combinatorial arguments about flowchart schemes with equational reasoning. Finally, a typed variation of KA is investigated that intends to capture properties of mathematical structures that appear in domain theory. The main result is that our proposed typed KA with products is strong enough to establish all the abstract properties of parametric fixpoints in the standard semantic model CPO, which is the category of [omega]-CPOs and [omega]-continuous maps.

Journal / Series

Volume & Issue



Date Issued




Kleene algebra; program verification; completeness


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Kozen,Dexter Campbell

Committee Co-Chair

Committee Member

Constable,Robert Lee
Shore,Richard A

Degree Discipline

Computer Science

Degree Name

Ph. D., Computer Science

Degree Level

Doctor of Philosophy

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


dissertation or thesis

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record