The Design of a Verified Derivative-Based Parsing Tool for Regular Expressions

Authors

  • Elton Cardoso
  • Maycon Amaro
  • Samuel Feitosa
  • Leonardo Reis
  • André Du Bois
  • Rodrigo Ribeiro Universidade Federal de Ouro Preto

DOI:

https://doi.org/10.19153/cleiej.24.3.2

Abstract

We describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.

Downloads

Published

2021-12-20

Issue

Vol. 24 No. 3 (2021): Regular papers and Special Issue For Digital Healthcare

Section

Articles

License

Copyright (c) 2021 Rodrigo Ribeiro

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).