Deciding regular expressions (in-)equivalence in Coq

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2012

Autores

Nelma Moreira (Autor) FCUP; David Pereira (Autor) Outra; Melo De Sousa, S (Autor) Outra

Ata de Conferência Internacional

Título: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Páginas: 98-113

13th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2012

Cambridge, 17 September 2012 through 20 September 2012

Indexação

Scopus - 10 Citações

Outras Informações

ID Authenticus: P-008-6SB

DOI: 10.1007/978-3-642-33314-9_7

Abstract (EN): This work presents a mechanically verified implementation of an algorithm for deciding regular expression (in-)equivalence within the Coq proof assistant. This algorithm decides regular expression equivalence through an iterated process of testing the equivalence of their partial derivatives and also does not construct the underlying automata. Our implementation has a refutation step that improves the general efficiency of the decision procedure by enforcing the in-equivalence of regular expressions at early stages of computation. Recent theoretical and experimental research provide evidence that this method is, on average, more efficient than the classical methods based in automata. We present some performance tests and comparisons with similar approaches. © 2012 Springer-Verlag.

Idioma: Inglês

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