Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This video presents a research talk from the CoqPL 2025 workshop where Jan-Paul Ramos-Davila from Cornell University discusses the formal verification of Software-Defined Delay-Tolerant Networks (SDDTNs). Learn about NetQIR, a domain-specific intermediate representation designed specifically for SDDTN algorithms that provides a formal framework for capturing the behavior of certain P4 programs without requiring verification of all language aspects. The presentation explores how NetQIR reasons about properties targeting the Match-Action Pipeline algorithm and provides a canonical representation for it. Discover how the researchers formalized NetQIR's semantics and type system in the Coq proof assistant, deriving a sound, executable semantics that supports verified execution of a subset of P4 programs. This 25-minute talk addresses the challenges of formal verification in environments with high latency and intermittent connectivity, demonstrating how SDDTNs integrate Software-Defined Networking principles with Delay Tolerant Networks to improve scalability and handle dynamic network conditions.
