## Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In *ESOP 2012: Programming Languages and Systems, 21st European
Symposium on Programming*, number 7211 in LNCS, pages 397--416. Springer,
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. This validation of 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.

[ bib |
DOI |
Local copy |
At publisher's site ]
Back

*This file was generated by
bibtex2html 1.99.*