Deciding Kleene algebra terms equivalence in Coq

• Type: Article in International Scientific Journal
• Date: 2015

Authors

Nelma Moreira (Author) FCUP; David Pereira (Author) Other; Simao Melo de Sousa (Author) Other

Journal

Title: Journal of Logical and Algebraic Methods in Programming

Vol. 84

Pages: 377-401

ISSN: 2352-2208

Publisher: Elsevier

Indexing

ISI Web of Knowledge - 2 Citations

Scopus - 2 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

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

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 25