Please use this identifier to cite or link to this item:
Author(s): Nelma Moreira
David Pereira
Simao Melo de Sousa
Title: Deciding Kleene algebra terms equivalence in Coq
Issue Date: 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 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.
Subject: Ciências da computação e da informação
Computer and information sciences
Scientific areas: Ciências exactas e naturais::Ciências da computação e da informação
Natural sciences::Computer and information sciences
Document Type: Artigo em Revista Científica Internacional
Rights: openAccess
Appears in Collections:FCUP - Artigo em Revista Científica Internacional

Files in This Item:
File Description SizeFormat 
110959.pdf170.67 kBAdobe PDFThumbnail

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.