A Verified Parser Generator

Abstract

Many software systems employ parsing techniques to map sequential input to structured output. Often, a parser is the system component that consumes data from an untrusted source. Because parsers mediate between the outside world and application internals, they are good targets for formal verification; parsers that come with strong correctness guarantees are likely to increase the overall security of applications that rely on them.

In this talk, I will present a verified parser generator based on the linear-time LL(1) parsing algorithm. When applied to a context-free grammar, the tool produces an LL(1) parser for the grammar if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete with respect to the input grammar’s semantics, and that they terminate with meaningful results on all inputs.

https://tufts.zoom.us/j/377889925?pwd=eXdDcU5wQnY3ejVwdzVjakN1TjYvUT09

meeting ID: 377-889-925

password: CS_PL_2020