Reseña: Mechanization of an algorithm for deciding KAT terms equivalence

Se ha publicado un nuevo trabajo sobre verificación formal en Coq: Mechanization of an algorithm for deciding KAT terms equivalence.

Sus autores son Nelma Moreira, David Pereira y Simao Melo de Sousa (de la Universidade do Porto, Portugal).

Su resumen es

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.

El código de la formalización en Coq se encuentra aquí.