CS 789 THEORY SEMINAR [home]

Speaker:  Dexter Kozen
Affiliation: CS, Cornell University
Date: Monday, September 15, 2003
Title: On the Representation of Kleene Algebra with Tests

Abstract:

Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra with Boolean algebra. One can model basic programming language constructs such as conditionals and while loops, verification conditions, and partial correctness assertions. KAT has been applied successfully in verification tasks involving communication protocols, basic safety analysis, source-to-source program transformation, concurrency control, compiler optimization, and dataflow analysis. The system subsumes Hoare logic and is deductively complete for partial correctness over relational models.

KAT has many interesting and useful models: language-theoretic, relational, trace-based, matrix. In programming language semantics and verification, the relational models are of primary importance, because correctness conditions are often expressed as input/output conditions on the start and final state of the computation. It is therefore of interest to characterize the relational models axiomatically or otherwise. 

In this talk, I will explore the question: under what conditions is a given abstract KAT isomorphic to an algebra of binary relations? Not all KATs are so representable. I will identify two simple separation properties that are sufficient for a nonstandard relational representation.