Login
HomePublicationsJournal Paper

Deciding Kleene Algebra Terms Equivalence in Coq
Ref: CISTER-TR-141205       Publication Date: May 2015

Deciding Kleene Algebra Terms Equivalence in Coq

Ref: CISTER-TR-141205       Publication Date: May 2015

Abstract:
This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based in automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalisation of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Authors:
David Pereira
,
Nelma Moreira
,
Simão Patrício Melo de Sousa


Published in Journal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier, Volume 84, Issue 3, pp 377-401.

DOI:10.1016/j.jlamp.2014.12.004.
ISSN: 2352-2208.



Record Date: 9, Dec, 2014