Validating LR(1) Parsers - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Validating LR(1) Parsers

Résumé

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 pro-vides 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.
Fichier principal
Vignette du fichier
validated-parser.pdf (513.47 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01077321 , version 1 (24-10-2014)

Identifiants

Citer

Jacques-Henri Jourdan, François Pottier, Xavier Leroy. Validating LR(1) Parsers. ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩. ⟨hal-01077321⟩
204 Consultations
367 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More