UDP: A Tale of Verification
Thu Apr 09 2026 1:00PM – 1:50PM
Event Description:
Speaker: Alain Kägi, Assistant Professor of Computer Science at Lewis & Clark College Abstract: My students and I have implemented a fast UDP-based networking stack in C and mechanically verified some important invariants of its UDP layer implementation. To achieve our performance goals, our implementation makes repeated small mutations to memory, and relies on pointer arithmetics and coercions. This approach presents challenges for the verification efforts, requiring manual treatment of pointer aliasing. In this talk, I will recount some of the challenges faced and the solutions adopted towards proving the functional correctness of a high-performance networking stack using the Isabelle/HOL interactive theorem prover. No knowledge of Isabelle and limited knowledge of C are required.