About Me
I am a lecturer at the Department of Computer Science at ETH, and part of the EduTec team of lecturers and developers. I very much enjoy teaching, and have been/am involved in numerous different courses over the years, including large introductory computer science courses, project-based software engineering courses for students and managers, and more specialised courses, e.g. on program verification.
My research, if time permits, is centred on automating deductive, separation-logic-based program verification using SMT solvers, and I am a senior member of the Viper research team. I obtained my PhD from ETH Zurich in 2016 under the supervision of Prof. Peter Müller, during which I developed the symbolic-execution-based verifier Silicon. Year's ago, I started my working life by becoming a media designer.
Teaching
2026
- Introduction to Programming (computer scientists; to come)
- Preparatory Course in CS (electrical engineers; to come)
- Software Engineering (mathematicians, engineers; to come)
- Computer Science I (electrical engineers; 300 students)
- Rigorous Software Engineering (computer scientists; 250 students)
- Software Engineering Fundamentals (continuous education; 40 students)
- Program Verification (computer scientists; 30 students)
2025
- Introduction to Programming (computer scientists; 580 students)
- Preparatory Course in CS (electrical engineers; 290 students)
- Computer Science I (electrical engineers; 280 students)
- Software Engineering (mathematicians, engineers; 80 students)
- Software Engineering Fundamentals (continuous education; 40 students)
- Rigorous Software Engineering (computer scientists; 250 students)
2024
- Introduction to Programming (computer scientists; 620 students)
- Computer Science II (electrical engineers; 280 students)
- Preparatory Course in CS (electrical engineers; 260 students)
- Numerical Methods for CS (computer scientists; 390 students; first two weeks)
- Computer Science I (electrical engineers; 250 students)
- Software Engineering (mathematicians, engineers; 90 students)
- Software Engineering Fundamentals (continuous education; 40 students)
- Rigorous Software Engineering (computer scientists; 260 students)
2023
- Computer Science II (electrical engineers; 280 students)
- Engineering Tool: Parallel and Concurrent Programming in C++ (mechanical engineers; 70 students)
- Preparatory Course in CS (electrical engineers; 230 students)
- Numerical Methods for CS (computer scientists; 400 students; first two weeks)
- Engineering Tool: Modelling (mechanical engineers; 180 students)
- Computer Science I (electrical engineers; 240 students)
- 2x Software Engineering (mathematicians, engineers; 70 + 80 students)
- Rigorous Software Engineering (computer scientists; 280 students)
2022
- Computer Science II (electrical engineers; 260 students)
- Engineering Tool: Parallel and Concurrent Programming in C++ (mechanical engineers; 40 students)
- Preparatory Course in CS (electrical engineers; 210 students)
- Numerical Methods for CS (computer scientists; 440 students; first two weeks)
- Engineering Tool: Modelling (mechanical engineers; 80 students)
- Computer Science I (electrical engineers; 270 students)
- Computer Science (mechanical engineers; 640 students)
- Software Engineering (mathematicians, engineers; 40 students)
- Rigorous Software Engineering (computer scientists; 220 students)
2021
- Computer Science II (electrical engineers; 260 students)
- Engineering Tool: Parallel and Concurrent Programming in C++ (mechanical engineers; 40 students)
- Preparatory Course in CS (electrical engineers; 250 students)
- Engineering Tool: Modelling (mechanical engineers; 160 students)
- Computer Science I (electrical engineers; 280 students)
- Computer Science (mechanical engineers; 580 students)
- Software Engineering (mathematicians, engineers; 40 students)
2020
- Computer Science (mathematicians, physicists; 630 students)
- Engineering Tool: Parallel and Concurrent Programming in C++ (mechanical engineers; 30 students)
- Preparatory Course in CS (electrical engineers; 250 students)
- Software Engineering Seminar (computer scientists; 20 students)
- Parallel Programming (computer scientists; 480 students)
- Rigorous Software Engineering (computer scientists; 150 students)
- Computer Science I (electrical engineers; 330 students)
- Computer Science (mechanical engineers; 550 students)
- Engineering Tool: Modelling (mechanical engineers; 60 students)
2019
- Computer Science (mathematicians, physicists; 570 students)
- Engineering Tool: Parallel and Concurrent Programming in C++ (mechanical engineers; 30 students)
- Preparatory Course in CS (electrical engineers; 310 students)
- Software Engineering Seminar (computer scientists; 20 students)
- Computer Science I (electrical engineers; 250 students)
- Computer Science (mechanical engineers; 564 students)
- Engineering Tool: Modelling (mechanical engineers; 80 students)
2018
- Computer Science (mathematicians, physicists; 570 students)
- Preparatory Course in CS (electrical engineers; 250 students)
- Informatics (mechanical engineers; 610 students)
Student Supervision
Currently
- Paul Winkler (P.W.) - Adding Support for Algebraic Data Types to a Kotlin Verifier
Previously
- Alexander Falter (B.Sc.) - Adding Specification Functions to a Kotlin Verifier [PDF]
- Paul Eibensteiner (M.Sc.) - Optimizing Program Verification Performance with Reinforcement Learning [PDF]
- Sonja Joost (B.Sc.) - Verification of Unbounded Dynamic Programming Problems [PDF]
- Glenn Schönbächler (B.Sc.) - Algebraic Data Types with Equational Theories [PDF]
- João Patrick Lopes Müller (B.Sc.) - Developing a Best-Practice Student Project Template for a Software Engineering Course [PDF]
- Athena Wang (B.Sc.) - Formal Verification of Dynamic Programming Algorithms [PDF]
- Nicola Widmer (B.Sc.) - Sound Automation of Magic Wands in a Symbolic-Execution Verifier [PDF]
- Daniel Zhang (P.W.) - Adding Native Support for Havoc in Viper [PDF]
- Lasse Anthony (P.W.) - Supporting Alternative SMT Solvers in Viper [PDF]
- Alessandro Maissen (P.W.) - Adding Algebraic Data Types to a Verification Language [PDF]
- Fabian Bösiger (B.Sc.) - Performance Improvements of a Program Verifier [PDF]
- Josua Stuck (B.Sc.) - Recovering from Verication Failures [PDF]
- Pascal Strebel (B.Sc.) - Explaining Unsatisfiability Proofs through Examples [PDF]
- Nico Hänggi (B.Sc.) - A Better SMT Language: Design & Tooling [PDF]
- Bogdan Gadzhylov (B.Sc.) - Reasoning about Nondeterministic Collections [PDF]
- Mauro Bringolf (B.Sc.) - Towards better Function Axiomatization in a Symbolic-execution-based Verifier [PDF]
- Fabio Streun (B.Sc.) - Tool Support for Termination Proofs [PDF]
- Linard Arquint (M.Sc.) - Profiling Symbolic Execution [PDF]
- Moritz Knüsel (B.Sc.) - Optimization of a Symbolic Execution based Program Verifier [PDF]
- Philippe Voinov (B.Sc.) - Optimising a Verification-Condition-Generation-based Deductive Verifier [PDF]
- Felix Wolf (M.Sc.) - Verifying Lock-Free Data Structures and Algorithms [PDF]
- Tobias Brodmann (B.Sc.) - Advancing Non-Standard Permission Utilisation in Program Verification [PDF]
- Ahmed Gamal (B.Sc.) - Adding Generalized Magic Wand Support in Carbon [PDF]
- 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]
Publications
Recent Years
- Fifteen Years of Viper Computer Aided Verification (CAV) 2025 [PDF] [BIB]
- Verification Algorithms for Automated Separation Logic Verifiers Computer Aided Verification (CAV) 2024 [PDF] [BIB]
- Verification Algorithms for Automated Separation Logic Verifiers (Extended Version) CoRR abs/2405.10661 2024 [PDF]
- A Generic Methodology for the Modular Verification of Security Protocol Implementations Conference on Computer and Communications Security (CCS) 2023 [PDF] [BIB]
- Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA Formal Methods in System Design (FMSD) 2023 [PDF] [BIB]
Previously
- A Generic Methodology for the Modular Verification of Security Protocol Implementations (Extended Version) CoRR abs/2212.02626 2022 [PDF]
- Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA Formal Methods (FM) 2021 [PDF] [BIB]
- Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Extended Version) CoRR abs/2010.07080 2020 [PDF]
- Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution Computer Aided Verification (CAV) 2016 [PDF] [BIB]
- Viper: A Verification Infrastructure for Permission-Based Reasoning Verification, Model Checking, and Abstract Interpretation (VMCAI) 2016 [PDF] [BIB]
- Lightweight Support for Magic Wands in an Automatic Verifier European Conference on Object-Oriented Programming (ECOOP) 2015 [PDF] [BIB]
- Constraint Semantics for Abstract Read Permissions Formal Techniques for Java-like Programs (FTfJP) 2014 [PDF] [BIB]
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Superseded by the VMCAI'16 paper) Technical Report, ETH Zurich 2014 [PDF] [BIB]
- Comparing Verification Condition Generation with Symbolic Execution: an Experience Report Verified Software Theories Tools Experiments (VSTTE) 2012 [PDF] [BIB]