Validating LR(1) Parsers

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 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.
Type de document :
Communication dans un congrès
ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. Springer, 7211, pp.397-416, Lecture Notes in Computer Science. <10.1007/978-3-642-28869-2_20>
Liste complète des métadonnées

https://hal.inria.fr/hal-01077321
Contributeur : Xavier Leroy <>
Soumis le : vendredi 24 octobre 2014 - 14:22:58
Dernière modification le : mercredi 28 septembre 2016 - 14:05:47
Document(s) archivé(s) le : dimanche 25 janvier 2015 - 10:26:29

Fichier

validated-parser.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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. Springer, 7211, pp.397-416, Lecture Notes in Computer Science. <10.1007/978-3-642-28869-2_20>. <hal-01077321>

Partager

Métriques

Consultations de
la notice

87

Téléchargements du document

112