| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 398.09 KB | Adobe PDF |
Advisor(s)
Abstract(s)
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.
Description
Keywords
Proof assistants Regular expressions Kleene algebra with tests Program verification
Citation
Publisher
Elsevier