Colloquium Computer Science - dr. Tobias Kappé University of Amsterdam

Title: Leapfrog: Certified Equivalence for Protocol Parsers

Abstract:

Because network protocol parsers have to meet strict performance targets, they are typically subjected to a wide range of optimizations, applied by programmer and compiler alike. These optimizations complicate the code, and by extension its verification. We present Leapfrog, a Coq-based framework for verifying the equivalence of parsers, including reference and optimized implementations of the same protocol. By combining symbolic representations, up-to techniques, and integration with off-the-shelf SMT solvers, Leapfrog is able to automatically verify many common parser optimizations, and scales up to do translation verification of a third-party parser compiler.

This is joint work with Ryan Doenges, John Sarracino, Nate Foster, and Greg Morrisett.