POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Sat 25 Jan 2025 15:07 - 15:30 at Peek-A-Boo - Session 3

Software-Defined Delay Tolerant Networks (SDDTNs) integrate the principles of Software-Defined Networking with Delay Tolerant Networks to address challenges of scalability and dynamic network conditions in environments with high latency and intermittent connectivity. While programming languages like P4 have been used to program SDDTNs, formal verification of these systems remains challenging. In this paper, we present NetQIR, a domain-specific intermediate representation that targets SDDTN algorithms. NetQIR provides a formal framework that captures the behavior of certain P4 programs without needing to verify all aspects of the language. Our approach reasons about these properties to target the Match-Action Pipeline algorithm, providing a canonical representation for it. We formalize NetQIR’s semantics and type system in the Coq proof assistant and derive a sound, executable semantics that supports verified execution of a subset of P4 programs.

I’m an undergrad @ Cornell University working towards computer science and philosophy degrees. My main research goals involve developing practical tools for software verification in general and domain-specific cases through programming language theory.

This program is tentative and subject to change.

Sat 25 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Session 3CoqPL at Peek-A-Boo
14:00
22m
Talk
Towards Verified Linear Algebra Programs Through Equivalence
CoqPL
Yihan Yang Harvey Mudd College, Mohit Tekriwal Lawrence Livermore National Laboratory, John Sarracino Lawrence Livermore National Laboratory, Matthew Sottile Lawrence Livermore National Laboratory, Ignacio Laguna Lawrence Livermore National Laboratory
14:22
22m
Talk
A Framework of Differential Operators
CoqPL
14:45
22m
Talk
A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
CoqPL
Tarakaram Gollamudi None, Jules Jacobs Cornell University, Yue Yao Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University
15:07
22m
Talk
Formal Verification of a Software Defined Delay-Tolerant Network
CoqPL
Jan-Paul Ramos-Davila Cornell University