HackerPapers

arXiv:1105.2576cs.LO

TRX: A Formally Verified Parser Interpreter

Adam Koprowski, Henri Binsztok

Abstract

Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. We are using parsing expression grammars (PEGs), a formalism essentially representing recursive descent parsing, which we consider an attractive alternative to context-free grammars (CFGs). From this formalization we can extract a parser for an arbitrary PEG grammar with the warranty of total correctness, i.e., the resulting parser is terminating and correct with respect to its grammar and the semantics of PEGs; both properties formally proven in Coq.

arXiv comments
26 pages, LMCS
Journal reference
Logical Methods in Computer Science, Volume 7, Issue 2 (June 24, 2011) lmcs:686
DOI
doi:10.2168/LMCS-7(2:18)2011
Subjects
cs.LOLogic in Computer Science cs.FLFormal Languages and Automata Theory cs.PLProgramming Languages

On Hacker News

Linked by 2 identifiable commenters in 4 comments across 4 threads, from Jul 2015 to Jun 2017.

Comments linking this paper, per year.

Discussed in comments4 threads

  1. Writing Parsers Like it is 2017 [pdf] 1 comment

    • On top of that, we even have some that are formally verified or validating that could be tied into Rust. https://arxiv.org/pdf/1105.2576.pdf http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf http://users.cecs.anu.edu.au/~aditi/esop09_submission_16.pdf One of those…

      nickpsecurityView on HNParent context

  2. Cloudflare Reverse Proxies Are Dumping Uninitialized Memory 1 comment

    • Next time, beware of parsers. Or formally verify them :) https://arxiv.org/pdf/1105.2576.pdf (disclaimer: co-author)

      hbbioView on HNParent context

  3. On the Complexity and Performance of Parsing with Derivatives 1 comment

    • Appreciate the feedback. My plan was to push some formal methodists or LANGSEC types to try to do a verified GLL if the opportunity arises. So far, there's been SLR [1], LR(1) [2], and PEG [3] verified for correctness. Think verified GLL generator is ideal next target given…

      nickpsecurityView on HNParent context

  4. Hammer: Parser Combinators for C 1 comment

    • Great work by the LANGSEC crowd. My recent interest in parsers was those verified for correctness or security. So, they have security and a certain amount of correctness. A great next step would be combining it with work on formal verification of parsers or generators (see…

      nickpsecurityView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.