Skip to ContentSkip to Navigation
Research Bernoulli Institute Calendar

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

When:Tu 28-06-2022 13:00 - 14:00
Where:5161.0289 Bernoullliborg

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.