Reference. CoStar: A verified ALL(*) parser

Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux · PLDI · 2021 · parsing verified · PDF · DOI · pldb
Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, termination properties, or performance characteristics. They are only compatible with a restricted class of grammars, they are not guaranteed to terminate on all inputs, or they are not designed to be performant on grammars for real-world programming languages and data formats. In this work, we present CoStar, a verified parser that addresses these limitations. The parser is implemented with the Coq Proof Assistant and is based on the ALL(*) parsing algorithm. CoStar is sound and complete for all non-left-recursive grammars; it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for commonly used languages and data formats.

Cite
Cite as @lasserCoStarVerifiedALL2021 (helia, typst) · \cite{lasserCoStarVerifiedALL2021} (LaTeX)
BibTeX
bibtex · 15 lines
@inproceedings{lasserCoStarVerifiedALL2021,
 title = {{{CoStar}}: A Verified {{ALL}}(*) Parser},
 author = {Lasser, Sam and Casinghino, Chris and Fisher, Kathleen and Roux, Cody},
 year = {2021},
 isbn = {978-1-4503-8391-2},
 doi = {10.1145/3453483.3454053},
 urldate = {2024-05-01},
 booktitle = {Proceedings of the 42nd {{ACM SIGPLAN International Conference}} on {{Programming Language Design}} and {{Implementation}}},
 pages = {420--434},
 publisher = {ACM},
 address = {Virtual Canada},
 langid = {english},
 month = {June},
 shorttitle = {{{CoStar}}}
}
hayagriva YAML (typst)
yaml · 22 lines
lasserCoStarVerifiedALL2021:
  type: article
  title:
    value: '{CoStar}: A Verified {ALL}(*) Parser'
    short: '{CoStar}'
  author:
  - Lasser, Sam
  - Casinghino, Chris
  - Fisher, Kathleen
  - Roux, Cody
  date: 2021-06
  page-range: 420-434
  serial-number:
    doi: 10.1145/3453483.3454053
    isbn: 978-1-4503-8391-2
  language: en-US
  parent:
    type: proceedings
    title: Proceedings of the 42nd {ACM SIGPLAN International Conference} on {Programming Language Design} and {Implementation}
    publisher:
      name: ACM
      location: Virtual Canada
Download: lasserCoStarVerifiedALL2021.bib · lasserCoStarVerifiedALL2021.yml

Backlinks
Cited by (2)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek𝙳), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek𝙳, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek𝙳 using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation lasserCoStar2023NFM · 2023

Follow up to CoStar.

DOI
Cites 36 works (9 here)
With notes (9)

Zippy LL(1) parsing with derivatives EdelmannZippy2020PLDI · 2020
In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.
DOI · pldb

A Verified LL(1) Parser Generator lasserLL1_2019ITP · 2019
An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.

Predecessor to CoStar and CoStar++.

DOI

Certified Normalization of Context-Free Grammars firsovCertifiedNormalizationContextFree2015CPP · 2015
Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.
PDF · DOI · pldb

Adaptive LL(*) parsing: the power of dynamic analysis parr-2014-adaptiveOOPSLA · 2014
PDF · DOI · pldb

Validating LR(1) Parsers jourdanValidatingLRParsers2012Programming Languages and Systems · 2012
An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
PDF · DOI · pldb

Parsing with derivatives: A functional pearl mightParsingDerivativesFunctional2011ICFP · 2011

We present a functional approach to parsing unrestricted context-free grammars based on Brzozowski’s derivative of regular expressions. If we consider context-free grammars as recursive regular expressions, Brzozowski’s equational theory extends without modification to context-free grammars (and it generalizes to parser combinators). The supporting actors in this story are three concepts familiar to functional programmers - laziness, memoization and fixed points; these allow Brzozowski’s original equations to be transliterated into purely functional code in about 30 lines spread over three functions.

Yet, this almost impossibly brief implementation has a drawback: its performance is sour - in both theory and practice. The culprit? Each derivative can double the size of a grammar, and with it, the cost of the next derivative.

Fortunately, much of the new structure inflicted by the derivative is either dead on arrival, or it dies after the very next derivative. To eliminate it, we once again exploit laziness and memoization to transliterate an equational theory that prunes such debris into working code. Thanks to this compaction, parsing times become reasonable in practice.

We equip the functional programmer with two equational theories that, when combined, make for an abbreviated understanding and implementation of a system for parsing context-free languages.

PDF · DOI · pldb

LL(*): the foundation of the ANTLR parser generator parr-2011-llPLDI · 2011
PDF · DOI · pldb

Total parser combinators danielssonTotalParserCombinators2010ICFP · 2010

A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library’s interface is similar to those of many other parser combinator libraries, with two important differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.

The library comes with a formal semantics, using which it is proved that the parser combinators are as expressive as possible. The implementation is supported by a machine-checked correctness proof.

PDF · DOI · pldb

PADS: a domain-specific language for processing ad hoc data fisher-2005-padsPLDI · 2005
PDF · DOI · pldb
External (27)
lasserCoStarVerifiedALL2021 reference entries/refs/lasserCoStarVerifiedALL2021/lasserCoStarVerifiedALL2021.hel