Deciding Kleene algebra terms equivalence in Coq

• Tipo: Artigo em Revista Científica Internacional
• Data: 2015

Autores

Nelma Moreira (Autor) FCUP; David Pereira (Autor) Outra; Simao Melo de Sousa (Autor) Outra

Revista

Título: Journal of Logical and Algebraic Methods in Programming

Vol. 84

Páginas: 377-401

ISSN: 2352-2208

Editora: Elsevier

Indexação

ISI Web of Knowledge - 2 Citações

Scopus - 2 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: P-00A-CBQ

DOI: 10.1016/j.jlamp.2014.12.004

Abstract (EN): 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 on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 25