BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//P4 - Language Consortium - ECPv6.16.3//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://p4.org
X-WR-CALDESC:Events for P4 - Language Consortium
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20240101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20250925T080000
DTEND;TZID=UTC:20250925T080000
DTSTAMP:20260531T151539
CREATED:20250912T220305Z
LAST-MODIFIED:20250930T162043Z
UID:10000130-1758787200-1758787200@p4.org
SUMMARY:P4 Developer Days - From Semantics to Software: Building a Verification Ecosystem for P4 using HOL4P4
DESCRIPTION:P4 Developer Days webinar\, “From Semantics to Software: Building a Verification Ecosystem for P4 using HOL4P4”\nDate: September 25\, 2025\nTime: 8:00am Pacific \nVIEW VIDEO\nVIEW SLIDES \nAbstract\nWe present a comprehensive formal verification ecosystem for the P4 network programming language\, built upon HOL4P4\, an abstract model of P4 execution embedded in the interactive theorem prover HOL4. The HOL4P4 formalization provides a semantics and a corresponding type system with formally verified progress\, preservation\, and type-soundness theorems. In addition\, it has been validated using a test suite from the P4 reference implementation. \nFrom this robust semantic foundation\, we have developed multiple practical verification tools. Our proof-producing symbolic execution engine enables functional correctness verification of entire real-world P4 programs\, with all results mechanically verified against the HOL4P4 semantics. Additionally\, we present a formally verified P4 software switch that maintains correctness guarantees from source to binary by leveraging both HOL4P4 and the verified CakeML compiler. This switch integrates seamlessly with existing network testing frameworks like Mininet while demonstrating decent performance compared to existing similar solutions.\n \nTogether\, these contributions demonstrate how rigorous formalization can serve as the foundation for a complete ecosystem of verification tools\, bridging the gap between theoretical guarantees and practical network development while meeting the growing demand for formal assurances in critical network infrastructure. \nSpeaker\nDidrik Lundberg combines academic research as a PhD candidate at KTH Royal Institute of Technology with practical engineering experience at Saab AB. He specializes in interactive theorem proving and formal verification\, particularly for low-level and network-related systems. His current focus is developing tools based on the HOL4P4 formalization of P4. \n 
URL:https://p4.org/event/p4-developer-days-from-semantics-to-software-building-a-verification-ecosystem-for-p4-using-hol4p4/
CATEGORIES:Events
END:VEVENT
END:VCALENDAR