This program is tentative and subject to change.
We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and—most importantly—access to a stack with accompanying push and pop operations.
By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT.
We develop a decision procedure for StacKAT program equivalence, based on finite automata.
This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs.
Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.
This program is tentative and subject to change.
Wed 18 JunDisplayed time zone: Seoul change
16:00 - 17:20 | |||
16:00 20mTalk | Active Learning of Symbolic NetKAT Automata PLDI Research Papers Mark Moeller Cornell University, Tiago Ferreira University College London, Thomas Lu Cornell University, Nate Foster Cornell University; Jane Street, Alexandra Silva Cornell University DOI | ||
16:20 20mTalk | StacKAT: Infinite State Network Verification PLDI Research Papers Jules Jacobs Cornell University, Nate Foster Cornell University; Jane Street, Tobias Kappé Leiden University, Dexter Kozen Cornell University, Lily Saada Cornell University, Alexandra Silva Cornell University, Jana Wagemaker Radboud University Nijmegen DOI | ||
16:40 20mTalk | Probabilistic Kleene Algebra with Angelic Nondeterminism PLDI Research Papers DOI | ||
17:00 20mTalk | Membership Testing for Semantic Regular Expressions PLDI Research Papers Yifei Huang University of Southern California, Matin Amini University of Southern California, Alexis Le Glaunec Rice University, Konstantinos Mamouras Rice University, Mukund Raghothaman University of Southern California DOI | ||