Deciding regular expressions (in-)equivalence in Coq

• Type: Article in International Conference Proceedings Book
• Date: 2012

Authors

Nelma Moreira (Author) FCUP; David Pereira (Author) Other; Melo De Sousa, S (Author) Other

Conference proceedings International

Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Pages: 98-113

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

Cambridge, 17 September 2012 through 20 September 2012

Indexing

Scopus - 10 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific