17 DEZEMBRO / DOMINGO / 13:49
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

Technical Report: DCC-2012-04

Mechanization of an Algorithm for Deciding KAT Terms Equivalence

Nelma Moreira

CMUP & DCC-FC, Universidade do Porto
e-mail: nam@dcc.fc.up.pt

David Pereira

LIACC & DCC-FC, Universidade do Porto
e-mail: dpereira@ncc.up.pt

Simão Melo de Sousa

LIACC & DI -- Universidade da Beira Interior
e-mail:desousa@di.ubi.pt
May 2012

Abstract

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.


FCUP 2017