jourdanValidatingLRParsers2012:
  type: anthos
  title: Validating {LR}(1) {Parsers}
  author:
  - Jourdan, Jacques-Henri
  - Pottier, François
  - Leroy, Xavier
  date: 2012
  editor:
  - Hutchison, David
  - Kanade, Takeo
  - Kittler, Josef
  - Kleinberg, Jon M.
  - Mattern, Friedemann
  - Mitchell, John C.
  - Naor, Moni
  - Nierstrasz, Oscar
  - Pandu Rangan, C.
  - Steffen, Bernhard
  - Sudan, Madhu
  - Terzopoulos, Demetri
  - Tygar, Doug
  - Vardi, Moshe Y.
  - Weikum, Gerhard
  - Seidl, Helmut
  page-range: 397-416
  url:
    value: http://link.springer.com/10.1007/978-3-642-28869-2_20
    date: 2024-04-22
  serial-number:
    doi: 10.1007/978-3-642-28869-2_20
    isbn: 978-3-642-28868-5 978-3-642-28869-2
  note: 'Series Title: Lecture Notes in Computer Science'
  abstract: 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.
  parent:
    type: anthology
    title: Programming {Languages} and {Systems}
    publisher:
      name: Springer Berlin Heidelberg
      location: Berlin, Heidelberg
    volume: 7211