Technical Report: DCC-2012-04

Mechanization of an Algorithm for Deciding KAT Terms Equivalence

Nelma Moreira

CMUP & DCC-FC, Universidade do Porto

David Pereira

LIACC & DCC-FC, Universidade do Porto

Simão Melo de Sousa

LIACC & DI -- Universidade da Beira Interior
May 2012


This work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence of Kleene algebra with tests (KAT) terms. This mechanization was carried out in the Coq proof assistant. The algorithm decides KAT terms equivalence through an iterated process of testing the equivalence of their partial derivatives. It is a purely syntactical decision procedure and so, it does not construct the underlying automata. The motivation for this work comes from the possibility of using KAT encoding of propositional Hoare logic for reasoning about the partial correctness of imperative programs.