Utilize este identificador para referenciar este registo: http://hdl.handle.net/10400.22/7356
Título: Deciding Kleene Algebra Terms Equivalence in Coq
Autor: Pereira, David
Moreira, Nelma
Sousa, Simão Patrício Melo de
Palavras-chave: Proof assistants
Regular expressions
Kleene algebra with tests
Program verification
Data: Mai-2015
Editora: Elsevier
Relatório da Série N.º: Journal of Logical and Algebraic Methods in Programming;Vol. 84, Issue 3
Resumo: 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.
Peer review: yes
URI: http://hdl.handle.net/10400.22/7356
DOI: http://dx.doi.org/10.1016/j.jlamp.2014.12.004
Versão do Editor: http://www.sciencedirect.com/science/article/pii/S235222081400100X
Aparece nas colecções:ISEP – CISTER – Artigos

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ART_CISTER_2015.pdf398,09 kBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.