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 and an automaton , checks that and 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 . 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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Jourdan, J. H., Pottier, F., & Leroy, X. (2012). Validating LR(1) parsers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7211 LNCS, pp. 397–416). https://doi.org/10.1007/978-3-642-28869-2_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
