KeynotesAPLAS 2025

Keynote Speaker

Prof. Dr. Peter Müller (joint keynote for APLAS and ATVA 2025)

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.

15 Years of Viper: Building and Evolving a Verification Infrastructure

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.