P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed to be simple and to facilitate efficient development of certified tools, while still retaining the essential domain-specific features of P4 itself. P4Cub has a front-end based on Petr4 [Doenges et al., 2021], and has been fully mechanized in Coq including large-step and small-step semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool.
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 22mTalk | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL CPP Katherine Kosaian Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology | ||
14:22 22mTalk | P4Cub: A Little Language for Big Routers CPP Rudy Peterson Cornell University, Eric Campbell Cornell University, John Chen Cornell University, Natalie Isak Microsoft, Calvin Shyu Cornell University, Ryan Doenges Cornell University, Parsia Ataei Cornell University, Nate Foster Cornell University | ||
14:45 22mTalk | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER CPP Haobin Ni Cornell University, Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research | ||
15:07 22mTalk | Verifying term graph optimizations using Isabelle/HOL CPP Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland, Mark Utting The University of Queensland | ||