Speaker : Prof Peter Muller, ETH Zürich, Switzerland
Date : 2025. 06. 17(Tue) 10:00 ~ 10:50
Location : #609, Jung Woonoh IT & General Education Center

Title: Automated Modular Program Verification Using Viper

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.

Abstract:
Imperative programs are notoriously difficult to reason about. Shared mutable state may lead to subtle interactions between program components and cause memory errors, unintended side effects, data races, and other bugs. This talk introduces Viper, a verification infrastructure that automates the modular verification of imperative programs. Viper provides an intermediate language to express verification problems in a variation of separation logic, and two verification back-ends that automate verification using an SMT solver. Program verifiers for mainstream languages are implemented as front-ends, which translate an input program and specification into Viper. The talk will provide an overview of the Viper language and ecosystem.