Defesa de Dissertação Raul Lopes, dia 23/02/2018, as 15:00, sala de seminários DECOM

Defesa de Dissertação Raul Lopes, dia 23/02/2018, as 15:00, sala de seminários DECOM

Título:
Certified Derivative-based Parsing of Regular Expressions

Resumo:
Parsing is pervasive in computing and fundamental in several software artifacts. This dissertation reports the first step in our ultimate goal: a formally verified toolset for parsing regular and context free languages based on derivatives. Specifically, 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 using the certified algorithms. Practical experiments conducted using this tool are reported.