Formal Methods Aided Network Operation

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).

  For more information, visit the workshop website