BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//P4 - Language Consortium - ECPv6.15.20//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:20250910T160000
DTEND;TZID=UTC:20250910T160000
DTSTAMP:20260503T055726
CREATED:20250912T220323Z
LAST-MODIFIED:20250919T172457Z
UID:10000150-1757520000-1757520000@p4.org
SUMMARY:P4 Developer Days - Mechanizing the P4 Language Specification with P4-SpecTec
DESCRIPTION:Date:  September 10th 4:00pm PST | September 11th – 8:00am KST \nVIEW VIDEO\nVIEW SLIDES \nAbstract\nThe P4 language has four main representations of its syntax and semantics: the official specification\, formalizations\, implementations\, and a test suite. While the four representations are intended to consistently define the P4 language\, they often diverge\, as each is managed by different parties and evolves at a different pace. This lack of alignment complicates both specification evolution and compiler maintenance. \n\n\nTo address this challenge\, we present P4-SpecTec\, a mechanized specification infrastructure for the P4 language. Inspired by successful language mechanization frameworks such as Wasm-SpecTec for WebAssembly and ESMeta for JavaScript\, P4-SpecTec introduces a formal\, complete\, and mechanized P4 language definition. From this single source of truth — the mechanized specification — we aim to generate multiple backends\, such as a type checker\, interpreter\, test suite\, and specification document\, in a consistent and automated manner. \nP4-SpecTec is an ongoing project\, where we currently mechanized the P4 type system. Notably\, our mechanized type system is executable. That is\, the typing rules can be executed\, acting as a P4 type checker. Our mechanized specification passes more than 97% of the applicable tests in the p4c test suite. This process already revealed inconsistencies and underspecified behaviors in both the P4 specification and its reference compiler. Based on the mechanized model\, we further developed a negative test generation technique that automatically produces ill-typed P4 programs that trigger subtle and diverse ill-typed conditions in the P4 type system. This approach has uncovered 11 compiler bugs and 12 soundness issues in the p4c frontend. \nThis talk introduces the design of P4-SpecTec\, current progress\, and long-term vision for a more robust and consistent P4 language ecosystem. \nSpeaker\nJaehyun Lee is a graduate student in the Programming Language Research Group at KAIST\, advised by Sukyoung Ryu. His research focuses on mechanizing programming language definitions to improve their reliability and precision. He leads the P4-SpecTec project\, which is a mechanized specification infrastructure for P4. Previously\, he contributed to the Wasm-SpecTec project\, now part of the official WebAssembly specification authoring toolchain. As part of that effort\, he co-authored the paper “Bringing the WebAssembly Standard Up to Speed with SpecTec”\, presented at PLDI 2024. His goal is to make language specifications reliable and better aligned with the needs of the developer community.
URL:https://p4.org/event/p4-developer-days-mechanizing-the-p4-language-specification-with-p4-spectec/
CATEGORIES:Events
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=UTC:20250917T080000
DTEND;TZID=UTC:20250917T080000
DTSTAMP:20260503T055726
CREATED:20250912T220322Z
LAST-MODIFIED:20250919T175701Z
UID:10000138-1758096000-1758096000@p4.org
SUMMARY:2025 P4 GSoC Wrap-up
DESCRIPTION:Date: September 17\, 2025\nTime: 8:00am Pacific \nThe wrap-up session highlights results of the projects hosted by The P4 Language Consortium during Google Summer of Code (GSoC) 2025. In its second consecutive year of participation\, we are pleased to share the results from each of the projects. During this session\, contributors will present their work\, share key outcomes\, and participate in a live Q&A. \nOfficial GSoC 2025 Profile: The P4 Language Consortium \nVIEW VIDEO \nAgenda \n\nOpening – Bili Dong\, Google \nP4 GSoC project presentation + discussion:\n\nBMv2 with All Possible Output Packets – Xiyu Hao\, New York University\nP4Sim Control Plane Enhancement – Vineet Goel\, Indian Institure of Technology Roorkee\nAccelerating OVS with Gigaflow: A Smart Cache for SmartNICs – Advay Singh\, University of Michigan\nSpliDT: Scaling Stateful Decision Tree Algorithms in P4 – Sankalp Jha\, Ajay Kumar Garg Engineering College\n\n\n\n  \n 
URL:https://p4.org/event/2025-p4-gsoc-wrap-up/
CATEGORIES:Events
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=UTC:20250925T080000
DTEND;TZID=UTC:20250925T080000
DTSTAMP:20260503T055726
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