Public Tech Talk: A Verified LL(1) Parser Generator

  • Date Wednesday, September 11, 2019  Time 11:00 AM
  • Speaker Sam Lasser, PhD student at Tufts University
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

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 both valid and invalid inputs.

Bio:

Sam Lasser is a third-year computer science PhD student at Tufts University, where he is advised by Dr. Kathleen Fisher. His research involves using interactive theorem proving techniques to produce verified software for data processing and programming language implementation. He is a Draper Fellowship recipient.