Summary

I am a research engineer working in program verification at the Chair of Programming Methodology at ETH Zurich, with a strong desire for building better software, and a passion for teaching. As a researcher, I develop theories that help assuring the correctness of concurrent programs; as an engineer, I develop tools that automate this assurance process; and as a networker, I seek to convince potential cooperation partners of the advantages of these theories and tools.

Education

PhD in Computer Science

, ETH Zurich, Switzerland 05/2011 – 11/2016

PhD thesis: Advancing Automated, Permission-Based Program Verification Using Symbolic Execution [PDF]: Designed a language and developed a verifier for automated, static verification of concurrent programs with shared mutable state (Scala)

Supervisor: Prof Peter Müller (co-supervisor: Prof Martin Vechev)

Responsibilities: In addition to my position as a researcher and teaching assistant, I was one of two lead developers of our program verification infrastructure called Viper (written in Scala). I coordinated subprojects and feature branches, reviewed student contributions and acted as a contact person for cooperation partners at other universities.

Included a four-month stay as a visiting scholar at KU Leuven, Belgium

MSc in Computer Science

, ETH Zurich, Switzerland 05/2009 – 04/2011

Specialisation: Software Engineering

Master’s thesis: Symbolic Execution for Chalice: [PDF]: Developed an automatic static verifier for a concurrency-research language enforcing data-race- and deadlock-freedom (Scala)

Term paper: Verifying Scala Traits: Developed and formalised a specification language for the automatic static verification of traits (Scala)

Required additional 55 ECTS credits due to my BSc from a University of Applied Sciences (FH)

MSc in Applied Computer Science

, FH Gelsenkirchen, Germany 03/2008 — 01/2009

Discontinued, moved on to ETH Zurich

Specialisation: Information Systems and Software Engineering

Term papers:

  • Image Retrieval Using Shape: Applying the Canny algorithm to extract feature vectors to efficiently index and retrieve images from image databases (Matlab)
  • Software Visualisation with IMSOVision: Using a collaborative immersive virtual environment to visualise different aspects of the software development process
  • The Internet’s Potential for Immigrants: Integrative and segregative possibilities of the internet for people with an immigration background

BSc in Computer Science & Media

, FH Gelsenkirchen, Germany 04/2004 — 02/2008

Bachelor’s thesis: Kartina — Ein Framework zur Algorithmenvisualisierung [PDF]: Runtime inspection and visualisation of algorithms (Java)

Included a semester abroad at the Tomsk Polytechnic University, Russia (winter semester 2006/07)

Apprenticeship in Media Design

, Cynapsis GmbH, Münster, Germany 08/2001 — 01/2004

Web application and browser game development; Customer support; Image editing (Flash, PHP, MySQL, Photoshop, Illustrator)

Employment

Research Engineer

, ETH Zurich, Switzerland since 11/2016

Research and development in automated verification of concurrent programs that manipulate shared state (Scala); Interviewed candidates for different open positions (internships, PhDs, Postdocs, research programmers)

Researcher and Teaching Assistant

, ETH Zurich, Switzerland 05/2011 — 11/2016

Student Assistant

, ETH Zurich, Switzerland 02/2010 — 10/2010

Developed an automated checkout, build, test and report system for multiple interdependent projects (Python)

Web Developer

, Locbook GmbH, Haltern, Germany 11/2007 — 01/2009

Development of a highly dynamic, social network site integrating Google Maps; Focus on quality assurance and documentation (Javascript, HTML)

Student Assistant

, FH Gelsenkirchen, Germany 2006 — 2007

Conceptional and prototypical work on the development of a promotional video about the trusted computing platform Turaya; Development of a virtual notice board for a stand at the CeBIT exhibition (Flash)

Web Developer

, Cynapsis GmbH, Münster, Germany 02/2004 — 08/2004

Miscellaneous Short-Term or Project-Based Side Jobs

Web developer for Hammer.Runge Designpartner; Media designer for the Department of Physical Science and Technology, FH Gelsenkirchen; Media designer at the communication agency henworx

IT Skills

Languages: Scala; Javascript, Python; Java, Matlab, C++, PHP, Haskell, Prolog, Perl; SQL, HTML, CSS

Software Engineering Tools: Mercurial, Git, SVN (code versioning); Bitbucket, GitHub (collaboration, code review, issue tracking); sbt, Ivy, Maven (project & dependency management); Jenkins, Travis (continuous integration); ScalaTest, JUnit, JMock, Checkstyle (testing, quality assurance)

General Interests: Program verification and formal methods; Software engineering; Quality assurance; Domain-specific languages; Teaching computer science

Personal Skills & Interests

Languages: German (native), English (fluent), Russian (basic, 2006), Dutch (basic, 2013)

International Experience: Belgium (visiting scholar, 2013), Russia (group leader in an international youth camp 2010, semester abroad 2006, language course 2006), England (Whitstable Twinning Association, stays with host families, 1990s), France (judo club’s exchange programme, 1990s)

Extracurricular: Fitness, cardio; Music; Reading; Design and typography; Previously: Organised events in my dormitory and helped international students

Academic Achievements

See my academic CV for a detailed overview of my academic achievements.

Teaching

  • Formal Methods and Functional Programming (2010, '12, '13, '15, '17)
  • Concepts of Object-Oriented Programming (2014, '16)
  • Type Systems (2014)
  • Informatik für Mathematiker und Physiker (2011, '12)
  • Computer Vision and Robotics 1 (2008)

Student Supervision

I particularly enjoy teaching and student supervision, and during the course of my PhD, I offered numerous student projects. In total, I so far supervised five master’s students and nine bachelor’s students.

Publications

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

Other Achievements

I repeatedly gave high-level presentations about my research area at various occasions — such as the cantonal computer science days ("Informatiktage"), ETH’s pre-study events, computer science weeks at schools and school classes visiting ETH — and to an audience varying in age and degree of familiarity with computer science.

My academic services include duties as an external paper reviewer, and serving on program and artefact evaluation committees. I have also given many talks and tool demos; the slides of some of the talks can be downloaded from my academic CV page.

Scholarships and Honours

  • Scholarship for Academic Excellence from the Cusanuswerk, 2009 – 2011
  • Best Student Award for course of studies and bachelor’s thesis, FH Gelsenkirchen, 2008
  • German Academic Exchange Service (DAAD) scholarship for a language course in Russia, 2006
“If I had asked people what they wanted, they would have said faster horses.” — Henry Ford