Network Abstractions for Modularity and Performance Verification
Aarti Gupta
Princeton University, USA
Abstract: Networks interconnect the digital world and provide numerous services we all depend upon. Due to ever-growing complexity in network sizes and design features, it is important but challenging to ensure their correct operation. In this talk, I will describe two recent efforts where we use network abstractions to improve methods for formal reasoning about network behavior. In the first, I will focus on modular reasoning about network routing, where a user annotates each router by an abstract interface and our tool automatically checks that these interfaces are inductive and correct. In the second, we use an abstraction over input packet queues on a switch, and combine it with a reduction to answer queries related to network switch performance. In both methods, the abstractions are sound and provide improvements by orders of magnitude in comparison to baseline approaches.
This talk describes joint work with Dexin Zhang, Divya Raghunathan, Maria Apostolaki and David Walker.
Bio: Aarti Gupta is a Professor in the Department of Computer Science at Princeton University. She received a PhD in Computer Science from Carnegie Mellon University. Her research is in the areas of formal verification of programs and systems, automatic decision procedures, and electronic design automation. She has served as an Associate Editor for Formal Methods in System Design (since 2005) and for the ACM Transactions on Design Automation of Electronic Systems (2008-2012). She is serving on the Steering Committee of the Computer Aided Verification (CAV) Conference (since 2013). She has received several Best Paper Awards from leading conferences and journals, and has been recognized as an ACM Fellow.
15 Years of Viper: Building and Evolving a Verification Infrastructure
(Joint APLAS-ATVA Invited Talk)
Peter Müller
ETH Zurich, Switzerland
Abstract: Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respectively. It has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language and automate verification using the Viper backends. In this talk, we summarize the core ideas behind Viper, give an overview of its applications, and explain our principles for evolving the system.
Bio: Peter Müller has been Full Professor and head of the Programming Methodology Group at ETH Zurich since August 2008. His research focuses on languages, techniques, and tools for the development of correct software. His previous appointments include a position as Researcher at Microsoft Research in Redmond, an Assistant Professorship at ETH Zurich, and a position as Project Manager at Deutsche Bank in Frankfurt. Peter Müller received his PhD from the University of Hagen.
Important Note: Peter Mueller’s invited talk is a joint invited talk with APLAS 2025.
LLMs meet Program Synthesis
Rahul Sharma
Microsoft Research, India
Abstract: This task will explore the speaker’s experience with LLMs in annotation inference and program synthesis.
Bio: Rahul Sharma is a principal researcher at Microsoft Research India. Prior to joining MSR, he obtained his PhD in Computer Science from Stanford University and BTech from IIT Delhi.