
Technical Report: DCC201304
KAT and Hoare Logic with Derivatives
Ricardo Almeida, Sabine Broda, Nelma Moreira
DCCFC & CMUP, Universidade do Porto
email: up030308017@alunos.dcc.fc.up.pt, {sbb,nam}@dcc.fc.up.pt
February 2013
Abstract
Kleene algebra with tests (KAT) is an equational system for program
verification, which is the combination of Boolean algebra (BA) and
Kleene algebra (KA), the algebra of regular expressions. In
particular, KAT subsumes the propositional fragment of Hoare logic
(PHL) which is a formal system for the specification and verification
of programs, and that is currently the base of most tools for checking
program correctness. Both the equational theory of KAT and the
encoding of PHL in KAT are known to be decidable. In this paper we
present a new decision procedure for the equivalence of two KAT
expressions based on the notion of partial derivatives. We also
introduce the notion of derivative modulo particular sets of
equations. With this we extend the previous procedure for deciding
PHL. Some experimental results are also presented.
