The design of a verified derivative-based parsing tool for regular expressions.

Cardoso, Elton MáximoAmaro, Maycon José JorgeFeitosa, Samuel da SilvaReis, Leonardo Vieira dos SantosBois, André Rauber DuRibeiro, Rodrigo Geraldo2022-12-062022-12-062021CARDOSO, E. M. et al. The design of a verified derivative-based parsing tool for regular expressions. CLEI Eletronic Journal, v. 24, n. 3, 2021. Disponível em: <http://www.clei.org/cleiej/index.php/cleiej/article/view/521/417>. Acesso em: 06 jul. 2022.0717-5000http://www.repositorio.ufop.br/jspui/handle/123456789/15838We 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.en-USabertoCertified algorithmsDependent typesThe design of a verified derivative-based parsing tool for regular expressions.Artigo publicado em periodicoThis work is licensed under a Creative Commons Attribution 4.0 International License. Fonte: Clei Eletronic Journal. <http://www.clei.org/cleiej/index.php/cleiej/article/view/521>. Acesso em: 28 set. 2022.