Certified virtual machine-based regular expression parsing.
Nenhuma Miniatura disponível
Data
2019
Autores
Título da Revista
ISSN da Revista
Título de Volume
Editor
Resumo
Regular expressions (REs) are pervasive in computing. We use REs in text editors, string
search tools (like GNU-Grep) and lexical analyzers generators. Most of these tools rely
on converting REs to its corresponding finite state machine or use REs derivatives for
directly parse an input string. In this work, we investigated the suitability of another
approach: instead of using derivatives or generating a finite state machine for a given
RE, we developed a certified virtual machine-based algorithm (VM) for parsing REs, in
such a way that a RE is merely a program executed by the VM over the input string.
First, we developed a small-step operational semantics for the algorithm, implemented
it in Haskell, tested it using QuickCheck and provided proof sketches of its correctness
with respect to RE standard inductive semantics. After that, we developed a big-step
operational semantics, an evolution of the small-step one. Unlike the small-step, the bigstep semantics can deal with problematic REs. We showed that the big-step semantics
for our VM is also sound and complete with regard to a standard inductive semantics
for REs and that the evidence produced by it denotes a valid parsing result. All of our
results regarding the big-step semantics are formalized in Coq proof assistant and, from
it, we extracted a certified algorithm, which we used to build a RE parsing tool using
Haskell programming language. Experiments comparing the efficiency of our algorithm
with another Haskell tool are reported.
Descrição
Programa de Pós-Graduação em Ciência da Computação. Departamento de Ciência da Computação, Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto.
Palavras-chave
VM/CMS - sistema operacional de computador, Análise de redes, Certificado digital, Algoritmos
Citação
DELFINO, Thales Antônio. Certified virtual machine-based regular expression parsing. 2019. 69 f. Dissertação (Mestrado em Ciência da Computação) - Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto, Ouro Preto, 2019.