Formal Verification of a Software Defined Delay-Tolerant Network
This program is tentative and subject to change.
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 JanDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 22mTalk | 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 22mTalk | A Framework of Differential Operators CoqPL | ||
14:45 22mTalk | 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 22mTalk | Formal Verification of a Software Defined Delay-Tolerant Network CoqPL Jan-Paul Ramos-Davila Cornell University |