Title: Automatic Proof Generation in Kleene Algebra with Tests

Speaker: James Worthington
Mathematics Department
Malott Hall
Cornell University
Ithaca, NY 14850
USA
worthing@math.cornell.edu

Kleene algebra (KA) is the algebra of regular events.  Familiar examples of 
Kleene algebras include regular sets, relation algebras, and trace algebras.  A 
Kleene algebra with tests (KAT) is a Kleene algebra with an embedded Boolean 
subalgebra.  The addition tests allows one to encode while programs as KAT 
terms, thus the equational theory of KAT allows one to reason about 
(propositional) program equivalence.  More complicated
statements about programs can be expressed in the Hoare theory of KAT, which 
suffices to encode Propositional Hoare Logic.

In our paper, we prove the following results.  First, there is a PSPACE 
transducer which takes equations of Kleene Algebra as input
and outputs proofs of them in an algebraic proof system based on a form of 
bisimulation.  Second, we give a feasible reduction
from the equational theory of KAT to the equational theory of KA. Combined with 
the fact that the Hoare theory of KAT reduces efficiently to the equational 
theory of KAT, this yields an algorithm capable of generating proofs of a large 
class of statements about programs.

Our result has applications to areas such as Proof-Carrying Code, where it is 
necessary that a formal proof be produced.  There are two traditional 
approaches to the equational theory of KA: interactive protocols for generating 
proofs and the decision procedure of Stockmeyer and Meyer to determine finite 
automata equivalence.  Each has its own drawbacks: interactive protocols are by 
definition not automatic, and the output of a decision procedure is just one 
bit, and therefore not efficiently verifiable.  Our method, which is completely 
automatic and outputs a proof, combines the best features of each.