The automation of verification techniques based on first-order logic specifications has benefited greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools such as verification condition generators.

However, these infrastructures are not ideal for verification techniques based on separation logic and other permission logics, because they do not provide direct support for permissions and because existing tools for these logics often prefer symbolic execution over verification condition generation. Consequently, tool support for these logics is typically developed independently for each technique, dramatically increasing the burden of developing automatic tools for permission-based verification.

In this talk, we present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide tool support, including two back-end verifiers – one based on symbolic execution and one on verification condition generation – and a specification inference tool based on abstract interpretation. Various existing verification techniques can be implemented via this infrastructure, alleviating much of the burden of building permission-based verifiers, and allowing the developers of higher-level techniques to focus their efforts at the appropriate level of abstraction.

Since August 2008 Peter Müller has been full Professor in Computer Science (since 2003 Assistant Professor for Software Component Technology) at ETH Zurich.

He was born in 1972 in Ingolstadt, Germany. In 1991 he started his studies in Computer Science at the Technical University of Munich, where he finished his undergraduate studies with a Diploma in Computer Science in 1996. From 1996 to 2001 he worked on his Ph.D. with Prof. Arnd Poetzsch-Heffter as supervisor, first at the Technical University Munich and later at the University of Hagen. In 2001 he received the title Dr. rer. nat. from the University of Hagen with a dissertation on “Modular Specification and Verification of Object-Oriented Programs”. Before joining ETH, Peter Müller worked as an IT project manager at Deutsche Bank in Frankfurt. From June 2007 to July 2008, he held a position as Researcher at Microsoft Research, Redmond.

The objective of Peter Müller-s research is to enable programmers to develop correct software. To achieve this goal, he works on programming languages, methods, and tools.