15 Years of Viper: Building and Evolving a Verification Infrastructure
Talk by Peter Müller
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 is a Full Professor and head of the Programming Methodology Group at ETH Zurich. 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. He is a Fellow of the ACM.
