About Me

I am a research engineer working in program verification at the Chair of Programming Methodology at ETH Zurich, where I also obtained my PhD, under the supervision of Prof. Peter Müller. From September to December 2013 I was a visiting scholar at KU Leuven in the group of Prof. Bart Jacobs, where I worked on using VeriFast to verify inter-thread contention problems. 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

Most of my work is centred around the Viper verification infrastructure (VMCAI'16 paper, project page); in particular, I am 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 includes 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.

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

  • 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

  • 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:

  • Robin Sierra (B.Sc.) - Towards Customizability of a Symbolic-Execution-Based Program Verifier
  • Patrick Gruntz (B.Sc.) - Checking Termination of Abstraction Functions
  • Nils Becker (B.Sc.) - Generalized Verification Support for Magic Wands

Previously:

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

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