About Me

I am a lecturer at the Department of Computer Science at ETH Zurich. In 2016, I obtained my PhD in the area of (semi-)automated verification of concurrent imperative programs, under the supervision of Prof. Peter Müller. During my PhD, I spent four months as a visiting scholar at KU Leuven in the group of Prof. Bart Jacobs. Even earlier, I did my Master's at ETH Zurich and my Bachelor's at the Westfälische Hochschule (previously called FH Gelsenkirchen). During my Bachelor's, I spent a great semester abroad at TPU in Tomsk, Russia. Before going to university I completed an apprenticeship as a media designer.

Areas of Work

As a lecturer, I mostly teach service courses, that is, computer science courses at other departments. These are typically introductory courses that cover general computer science concepts but also serve as an introduction to programming languages such as C++ or Java.

My PhD research was centred around the Viper verification infrastructure (VMCAI'16 paper, project page); in particular, I was the main researcher and developer behind the Silicon verifier, which is a (semi)-automatic, symbolic-execution-based verifier for Viper's expressive, permission-based intermediate verification language. My work included developing language features on the level of Viper that enable the specification, encoding and verification of high-level programming language features, and finding ways to automate the verification using symbolic execution and SMT solvers.

After my PhD I started investigating the potential of using Viper to automate "modern" separation logics, in particular those developed for reasoning about fine-grained concurrency algorithms and data structures.

Publications

  • P. Müller, M. Schwerhoff, A. J. Summers Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution Computer Aided Verification (CAV) 2016 [PDF] [BIB]
  • P. Müller, M. Schwerhoff, A. J. Summers Viper: A Verification Infrastructure for Permission-Based Reasoning Verification, Model Checking, and Abstract Interpretation (VMCAI) 2016 [PDF] [BIB]
  • M. Schwerhoff, A. J. Summers Lightweight Support for Magic Wands in an Automatic Verifier European Conference on Object-Oriented Programming (ECOOP) 2015 [PDF] [BIB]
  • J. Boyland, P. Müller, M. Schwerhoff, A. J. Summers Constraint Semantics for Abstract Read Permissions Formal Techniques for Java-like Programs (FTfJP) 2014 [PDF] [BIB]
  • U. Juhasz, I. T. Kassios, P. Müller, M. Novacek, M. Schwerhoff, A. J. Summers Viper: A Verification Infrastructure for Permission-Based Reasoning (Superseded by the VMCAI'16 paper) Technical Report, ETH Zurich 2014 [PDF] [BIB]
  • I. T. Kassios, P. Müller, M. Schwerhoff Comparing Verification Condition Generation with Symbolic Execution: an Experience Report Verified Software Theories Tools Experiments (VSTTE) 2012 [PDF] [BIB]

Talks

Choose the PowerPoint (PPTX) versions if possible, the PDFs can be incomplete because of missing animations.

  • Advancing Automated, Permission-Based Program Verification Using Symbolic Execution PhD Defence, ETH Zurich 2016-11 [PPTX] [PDF]
  • Viper and Quantified Permissions JML Workshop, Bad Herrenalb 2016-11 [PPTX] [PDF]
  • Viper: A Verification Infrastructure for Permission-based Reasoning Charles University, Prague 2016-10 [PPTX] [PDF]
  • Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution CAV 2016-07 [ZIP (PPTX)] [PDF]
  • Lightweight Support for Magic Wands in an Automatic Verifier ECOOP 2015-07 [PPTX] [PDF]
  • An Introduction to Automated Software Verification with Permission Logics ETH Zurich 2015-05 [PPTX] [PDF]
  • Viper: A Verification Infrastructure for Permission-Based Reasoning (longer than the ECOOP PC Meeting talk) JML Workshop, Leiden 2015-03 [PPTX] [PDF]
  • Viper: A Verification Infrastructure for Permission-Based Reasoning ECOOP PC Meeting 2015-02 [PPTX] [PDF]
  • Constraint Semantics for Abstract Read Permissions FTfJP 2014-07 [PPTX] [PDF]
  • Automated Software Verification with Implicit Dynamic Frames KU Leuven 2013-12 [PPTX] [PDF]
  • Comparing Verification Condition Generation with Symbolic Execution (slightly longer than the VSTTE talk) Dagstuhl 2012-12 [PPTX] [PDF]
  • Comparing Verification Condition Generation with Symbolic Execution VSTTE 2012-01 [PPTX] [PDF]

Services

  • AVoCS'18: External reviewer
  • POPL'18: External reviewer
  • FTfJP'17: Program committee member
  • ECOOP'17: External reviewer
  • ESOP'17: External reviewer
  • OOPSLA'15: Artefact evaluation committee member
  • ECOOP'15: Student volunteer for the PC meeting
  • VSTTE'15: External reviewer
  • IWACO'14: External reviewer
  • OOPSLA'13: External reviewer
  • POPL'13: External reviewer

Teaching

  • Informatics at the Dept. of Mechanical Engineering (SS 2018)
  • Formal Methods and Functional Programming (SS 2017)
  • Concepts of Object-Oriented Programming (AS 2016)
  • Concepts of Object-Oriented Programming (AS 2015)
  • Formal Methods and Functional Programming (SS 2015)
  • Concepts of Object-Oriented Programming (AS 2014)
  • Type Systems (SS 2014)
  • Formal Methods and Functional Programming (SS 2013)
  • Informatik für Mathematiker und Physiker (SS 2012)
  • Formal Methods and Functional Programming (SS 2012)
  • Informatik für Mathematiker und Physiker (AS 2011)
  • Formal Methods and Functional Programming (SS 2010, as a student)

Student Supervision

Currently:

  • Felix Wolf (M.Sc.) - Verifying Lock-Free Data Structures and Algorithms
  • Tobias Brodmann (B.Sc.) - Advancing Non-Standard Permission Utilisation in Program Verification
  • Ahmed Gamal (B.Sc.) - Adding Generalized Magic Wand Support in Carbon

Previously:

  • Robin Sierra (B.Sc.) - Towards Customizability of a Symbolic-Execution-Based Program Verifier [PDF]
  • Patrick Gruntz (B.Sc.) - Checking Termination of Abstraction Functions [PDF]
  • Nils Becker (B.Sc.) - Generalized Verification Support for Magic Wands [PDF]
  • Simon Fritsche (M.Sc.) - A Framework for Bi-directional Program Transformations [PDF]
  • Flavio Goldener (B.Sc.) - Developing a Web-Based Hoare Logic Proof Assistant [PDF]
  • Mathias Birrer (B.Sc.) - Developing an Interactive, Web-Based Tutorial for an Intermediate Verification language [PDF]
  • Andreas Buob (B.Sc.) - Recording Symbolic Executions [PDF]
  • Roger Koradi (B.Sc.) - Incremental Symbolic Execution [PDF]
  • Simon Fritsche (B.Sc.) - Verifying Scala's Vals and Lazy Vals [PDF]
  • Bernhard Brodowsky (M.Sc.) - Translating Scala to SIL [PDF]
  • Andres Bühlmann (M.Sc.) - Supporting Subclassing and Traits in Syxc [PDF]
  • Roland Meyer (B.Sc.) - Developing a Common Web Interface to Various Verification Tools [PDF]
  • Ivo Colombo (M.Sc,) - Debugging Symbolic Execution [PDF]
  • Rokas Matulis (M.Sc.) - Extensible Code Contracts for Scala [PDF]

Theses

  • PhD: Advancing Automated, Permission-Based Program Verification Using Symbolic Execution, 2016 [PDF]
  • MSc: Symbolic Execution for Chalice, 2011 [PDF]
  • BSc: Kartina --- Ein Framework zur Algorithmenvisualisierung, 2008 [PDF]
“If I had asked people what they wanted, they would have said faster horses.” — Henry Ford