2nd Workshop on Formal Methods Aided Network Operation (FMANO)
Monday, September 8th | Half-day Workshop (Morning)
Location
The workshop will take place at Room Terceira.
Program
|
08:00 — 08:45 | Registration |
|
09:00 — 09:10 | Openning remarks |
|
09:10 — 09:45 | Keynote 1: Verifying configurations was the easy part: my ongoing quest toward correct network operations and musings about how AI could help | Laurent Vanbever (ETH Zürich) Abstract: We all know the story too well: complex systems fail in complex ways, and networks are no exception. As most of these failures can be traced back to misconfigurations, a lot of research in the last decade has gone into verifying configurations, with great success. And yet, networks _still_ routinely fail. In the first part of this talk, I'll highlight some of the reasons behind this. I'll argue that configuration verification is only a small piece of the puzzle, and that a lot of work still needs to be done to make it more usable. In doing so, I'll showcase some of our recent works which aim at: broadening the types of properties that can be verified; safely deploying verified configurations network-wide; and figuring out what to verify in the first place. In the second part, I'll speak about some of the opportunities—and pitfalls—of applying AI to network operations. Biography: Laurent Vanbever is an associate professor at ETH Zürich, where he leads the Networked Systems Group (NSG). His research focuses on making large network infrastructures more manageable, scalable, and secure. He has received several awards for his research including the SIGCOMM Rising Star Award, two SIGCOMM best paper awards, the NSDI community award, six IETF/IRTF Applied Networking Research Prizes, and an ERC Starting Grant. In June 2024, Laurent co-founded NetFabric.ai, a startup focused on smart network observability where he serves as chief scientist. He completed his PhD under Prof. Olivier Bonaventure at the University of Louvain (Belgium) and was a postdoctoral researcher with Prof. Jennifer Rexford at Princeton University. |
|
09:45 — 10:35 | Session 1 | Chair: TBA 09:45 - 09:55 DNScope: Detecting DNS Misconfigurations through Graph Neural Static Reasoning Kaiqiang Hu, Haizhou Du (Shanghai University of Electric Power); Ziyi Wang (Xiamen University) 09:55 - 10:05 ConfSum: Towards Automatic Summarization of Network-scale Operational Intents from Device Configurations Rundi Zhai (Beijing University of Posts and Telecommunications, Zhongguancun Laboratory); Jianmin Liu (Tsinghua University); Yukai Miao, Li Chen (Zhongguancun Laboratory); Dan Li (Tsinghua University); Baojiang Cui (Beijing University of Posts and Telecommunications); Peng Zhang (Xi'an Jiaotong University); Ennan Zhai (Alibaba); Zishuo Ding (The Hong Kong University of Science and Technology (Guangzhou)) 10:05 - 10:15 SafeMigration: Safe Large-scale Migration Planning via Symbolic Execution Zibin Chen, Lixin Gao (Univ. of Massachusetts); Ying Zhang (Meta) 10:15 - 10:25 A Forwarding-Path-Aware Sampling Strategy for Config2Spec Shangsen Li, Lailong Luo, Changhao Qiu, Bangbang Ren (National University of Defense Technology); Deke Guo (Sun Yat-sen University) 10:25 - 10:30 Incremental Network Configuration Verification via Localized Subspecification Haoxian Chen (ShanghaiTech University) 10:30 - 10:35 Scalable BGP Simulation of Hyper-Scale Data Center Networks Mengrui Zhang, Xiaoqiang Zheng, Lizhao You (Xiamen University); Ziyang Yao, Yang Wang, Rui Wen, Zhi Zhang, Ronghua Sun, Yuanhui Zhong, Haihua Li (Huawei Technologies Co. Ltd); Fei Yuan (Xiamen University); Yuanxun Kang (Yealink Technologies Co. Ltd); Qiao Xiang (Xiamen University) |
|
10:35 — 11:00 | Morning coffee break |
|
11:00 — 11:35 | Keynote 2: Towards AI-Augmented Formal Methods in Networking | Matthew Caesar (UIUC) Abstract: Artificial Intelligence has transformed what we believe is possible in computing, yet its strengths in adaptability, generality, and breadth often contrast with the foundational priorities of the systems and networking community: correctness, rigor, and explainability. In this talk, I explore a complementary path forward that leverages AI to augment formal methods. By integrating learning-based techniques with automated reasoning, we can reimagine formal verification as a more creative, scalable, and interactive process. This synergy opens the door to a new class of tools that retain the precision of proofs while embracing the flexibility of AI. I will outline a vision for this integration, share early breakthroughs, and discuss how this approach can enhance the reliability and robustness of future systems infrastructure. Biography: Matthew Caesar is a Professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He received his Ph.D. at UC Berkeley in 2007. He currently serves as Chair of ACM SIGCOMM, co-founder and organizing committee member of the Networking Channel, and co-Principal Investigator of the TSCP-DC project at UIUC's IARCS center in Singapore. Prior to his Ph.D, he spent multiple years as an engineer in the telecom sector. He has worked in the area of networked systems for over two decades, publishing over 50 technical papers, which appear in highly selective academic conferences and have resulted in multiple best paper awards. He received the NSF CAREER award, DARPA CSSG membership, is a CAS Fellow, an IEEE Fellow and received Test of Time Awards from SIGSIM-PADS for his landmark work on distributed time synchronization, and USENIX NSDI for his foundational contributions to software-defined networking. Matthew has a long history of successful technology transfer. His startup company Veriflow produced the first practical network verification system and was sold to VMware in 2019. At AT&T he co-developed the Routing Control Platform, a route management technology which was deployed on their North American IP backbone. |
|
11:35 — 12:25 | Session 2 | Chair: TBA 11:35 - 11:45 LTL-based Specifications for P4 Program Synthesis Lorenzo Theunissen, Sebastijan Dumančić, Fernando Kuipers (Delft University of Technology) 11:45 - 11:55 Protocol Vulnerability Detection Method Based on Fuzzing in Low Earth Orbit Satellite Network Chuntao Lan, Lin Yao, Guowei Wu (Dalian University of Technology); Ziyuan Tian (Shanghai Dahua Surveying & Mapping Company) 11:55 - 12:05 Modeling and Evaluation of Elastic SFC Based on HCPN Rulin Zhang, Hui Dong, Ju Zhang, Hua Li (College of Computer Science, Inner Mongolia University) 12:05 - 12:15 Refining specifications for configuration repair with side effect diagnosis Ryusei Shiiba (Sokendai); Satoru Kobayashi (Okayama University); Osamu Akashi (National Institute of Informatics); Kensuke Fukuda (NII/Sokendai) 12:15 - 12:20 Formal Specifications for Data Plane Programs Keyu Yuan, Baber Rehman (Huawei Technologies) 12:20 - 12:25 Poster: High-Performance Centralized Parallel Data-Plane Verification for Hyper-Scale DCNs Peng Peng, Xun Sun (Xiamen University); Zhengtao Shen (ByteDance, China); Feiyang Ding (Xiamen University); Jiawei Chen (ByteDance, China); Lizhao You (Xiamen University); Weirong Jiang, Yongping Tang (ByteDance); Feng Luo (ByteDance, China) |
|
12:25 — 12:30 | Closing remarks |
|
12:45 — 14:00 | Lunch Break |
|
15:45 — 16:15 | Afternoon Coffee Break |
Call for Papers
There has been a growing interest from networking researchers, equipment vendors, and Internet service providers to apply formal methods in network operation to improve the availability, reliability, and performance of networks. Starting from the pioneering work on data plane verification (i.e., Anteater, HSA and Veriflow), researchers have invented many novel approaches to utilize formal methods in a wide range of aspects of network operation, including but not limited to routing configuration verification, diagnosis and synthesis, verification and testing of programmable networks, DNS configuration and implementation verification, and congestion control and scheduling verification. Many of these innovations have been published in top-tier venues such as SIGCOMM, NSDI, SOSP, and OSDI. The percentage of papers on network formal methods in SIGCOMM and NSDI for the past ten years shows a steady interest in network formal methods in our community (e.g., up to 16.4% in SIGCOMM 2021 and up to 16.9% in NSDI 2020).
Although it is a relatively new research area, the impact of this line of research has already gone beyond publications. Not only several startups (e.g., Intentionet) have emerged, but multiple mega-scale Internet companies (e.g., Microsoft, Amazon, and Alibaba) have deployed formal-methods-based operation tools (e.g., Batfish, RCDC, and Hoyan) in their production networks.
The goal of the formal methods aided network operation (FMANO) workshop is to (1) provide a venue for the community to engage in a lively discussion on the challenges, opportunities, and future research agendas in the intersection of networking and formal methods and (2) make this emerging and exciting research area accessible to a broader audience.
In this workshop, we seek contributions to the design principles, implementations, and operation experiences of formal-methods-based network operating systems. Selected keynotes and a panel of experts from both academia and industry will be included to complement more traditional paper sessions, to set the research agenda, debate the issues, and share the most recent progress.
Topics of Interest
We welcome submissions on all aspects of formal-methods-based network operating systems. Topics include, but are not limited to:
- Deployment and operation requirements
- Network design
- Network diagnosis
- Network modeling
- Network monitoring
- Network protocol design and analysis
- Network repair
- Network security
- Network simulation
- Network synthesis
- Network verification
- Operation across multiple domains
Submission Instructions
Submissions must be original, unpublished work, and not under consideration at another conference or journal. We accept two types of submissions: regular papers that are at most six (6) pages long, including all figures, tables, references, and appendices in two-column 10pt ACM format; and extended abstracts that are at most two (2) pages long with a maximum of one additional page for references only.
Papers and extended abstracts must include author names and affiliations for single-blind peer reviewing by the PC. Authors of accepted submissions are expected to present and discuss their work at the workshop.
Please submit your paper via https://fmano25.hotcrp.com
Important Dates
| Submission deadline | May 30th, 2025 AoE (Updated) |
|---|---|
| Acceptance notification | June 13th, 2025 |
| Camera-ready deadline | July 13th, 2025 AoE (Updated) |
| Workshop date | September 8th, 2025 |
Organizers
| General Co-Chairs | Institution |
|---|---|
| Qiao Xiang | Xiamen University |
| Ennan Zhai | Alibaba |
| Technical Program Co-Chairs | Institution |
| Peng Zhang | Xi’an Jiaotong University |
| Qiang Su | The Chinese University of Hong Kong |
| Technical Program Committee | Institution |
| Li Chen | ZGC Lab |
| Kaihui Gao | Tsinghua University |
| Xin Jin | Peking University |
| Franck Le | IBM |
| Fuliang Li | Northeast University |
| Geng Li | China Telecom |
| Alan Liu | UMD |
| Chang Lou | Virginia Tech |
| Ning Luo | UIUC |
| Congcong Miao | Tencent |
| Ruzica Piskac | Yale |
| Miguel Rio | UCL |
| Tao Sun | China Mobile |
| Qin Wu | IETF IAB |
| Ennan Zhai | Alibaba |
| Peng Zhang | Xi’an Jiaotong University |
