Certified virtual machine-based regular expression parsing.

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorRibeiro, Rodrigo Geraldo-
Autor(es): dc.contributorRibeiro, Rodrigo Geraldo-
Autor(es): dc.contributorMalaquias, José Romildo-
Autor(es): dc.contributorReis, Leonardo Vieira dos Santos-
Autor(es): dc.creatorDelfino, Thales Antônio-
Data de aceite: dc.date.accessioned2025-08-21T15:27:14Z-
Data de disponibilização: dc.date.available2025-08-21T15:27:14Z-
Data de envio: dc.date.issued2020-07-27-
Data de envio: dc.date.issued2020-07-27-
Data de envio: dc.date.issued2019-
Fonte completa do material: dc.identifierhttp://www.repositorio.ufop.br/handle/123456789/12512-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/1015297-
Descrição: dc.descriptionPrograma 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.-
Descrição: dc.descriptionRegular 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.-
Formato: dc.formatapplication/pdf-
Idioma: dc.languageen-
Direitos: dc.rightsaberto-
Direitos: dc.rightsAutorização concedida ao Repositório Institucional da UFOP pelo(a) autor(a) em 25/06/2019 com as seguintes condições: disponível sob Licença Creative Commons 4.0 que permite copiar, distribuir e transmitir o trabalho desde que sejam citados o autor e o licenciante. Não permite o uso para fins comerciais nem a adaptação.-
Palavras-chave: dc.subjectVM/CMS - sistema operacional de computador-
Palavras-chave: dc.subjectAnálise de redes-
Palavras-chave: dc.subjectCertificado digital-
Palavras-chave: dc.subjectAlgoritmos-
Título: dc.titleCertified virtual machine-based regular expression parsing.-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional - UFOP

Não existem arquivos associados a este item.