zbMATH — the first resource for mathematics

Validating LR(1) parsers. (English) Zbl 1352.68131
Seidl, Helmut (ed.), Programming languages and systems. 21st European symposium on programming, ESOP 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28868-5/pbk). Lecture Notes in Computer Science 7211, 397-416 (2012).
Summary: 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 \(\mathcal G\) and an automaton \(\mathcal A\), checks that \(\mathcal A\) and \(\mathcal 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 \(\mathcal 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.
For the entire collection see [Zbl 1238.68022].

68Q45 Formal languages and automata
68N20 Theory of compilers and interpreters
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Coq; Menhir
Full Text: DOI