Marco Eilers

About Me

I defended my PhD in 2022 at the Programming Methodology Group at ETH (supervised by Prof. Peter Müller), where I have since continued to work as a postdoc. I did my Master's degree at the University of Copenhagen, during which I spent one semester at Utrecht University. Before, I received my Bachelor's degree in Business IT from the Berlin School of Economics and Law in a dual programme with IBM.

News

Our paper "Fifteen Years of Viper" was accepted at external page CAV 2025.

Research Interests

My main area of research is automated, deductive program verification, particularly of hyperproperties and information flow security for object-oriented programs. I am the main developer of the Nagini verifier for Python, and have supervised the development of 2vyper, a modular verifier for Ethereum smart contracts. Both are based on Viper, a verification infrastructure for permission-based reasoning that I have contributed to in various ways and am currently one of the main developers of. Additionally, I am involved with the VerifiedSCION project whose goal is the full-stack verification of a new internet architecture; my focus is on formally connecting code verification and protocol verification, as well as improving the underlying code verification tools.

Publications

M. Eilers, M. Schwerhoff and P. Müller, Verification Algorithms for Automated Separation Logic Verifiers
In Computer Aided Verification (CAV), 2024. [PDF] [external page Publisher] [Download Slides (PDF, 783 KB)]
J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. Müller and A. Perrig, Protocols to Code: Formal Verification of a Next-Generation Internet Router
Technical report, 2024. [PDF] [external page arXiv]
M. Eilers, T. Dardinier and P. Müller, CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
In Programming Language Design and Implementation (PLDI), 2023. [PDF] [external page Publisher] [external page Talk] [external page arXiv]
M. Eilers, Modular Specification and Verification of Security Properties for Mainstream Languages
PhD thesis, 2022. [PDF]
C. Bräm, M. Eilers, P. Müller, R. Sierra and Alexander J. Summers, Rich Specifications for Ethereum Smart Contract Verification
In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2021. [PDF] [external page Publisher] [external page Talk] [external page Extended TR]
M. Eilers, S. Meier and P. Müller, Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
In Computer Aided Verification (CAV), 2021. [PDF] [external page Publisher] [external page Talk]
C. Sprenger, T. Klenze, M. Eilers, F. Wolf, P. Müller, M. Clochard and D. Basin, Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020. [PDF] [external page Publisher] [external page Talk] [external page Extended TR]
M. Eilers, P. Müller and S. Hitz, Modular Product Programs
In ACM Transactions on Programming Languages and System (TOPLAS), 2020. [PDF] [external page Publisher]
M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [PDF] [external page Publisher] [Download Slides (PDF, 908 KB)]
M. Hassan, C. Urban, M. Eilers and P. Müller, MaxSMT-based Type Inference for Python 3
In Computer Aided Verification (CAV), 2018. [PDF] [external page Publisher] [Download Slides (PDF, 975 KB)]
M. Eilers, P. Müller and S. Hitz, Modular Product Programs
In European Symposium on Programming (ESOP), 2018. [PDF] [external page Publisher] [Download Slides (PDF, 375 KB)]

Tools

Nagini, a static verifier for Python 3: [external page Github]
HyperViper, a verifier for information flow security for concurrent programs: [external page Github]
2vyper, a verifier for Vyper smart contracts: [external page Github]
Typpete, SMT-based type inference for Python: [external page Github]
I am a contributor to Viper, a verification infrastructure for permission based reasoning

Service

iFM 2024 PC, SOAP 2023 PC, PriSC 2023 PC, PERR 2022 PC, ECOOP 2019 AEC
Reviewed for STTT
Subreviewed for ESOP 2025, POPL 2024, ICALP 2023, ESOP 2023, ICTAC 2022, ISSTA 2022, SEFM 2020, CAV 2020, VMCAI 2020, iFM 2019, LOPSTR 2019, CAV 2019, ISSTA 2019, TACAS 2019, VMCAI 2019, FM 2018, ESOP 2017

Teaching

Program Verification (MSc Computer Science, Spring 2023 and 2024)
Previously TA for Concepts of Object-Oriented Programming, Program Verification , Rigorous Software Engineering, Software Architecture and Engineering, Research Topics in Software Engineering, Software Engineering Seminar, Computer Science I, Computer Science for Mathematicians and Physicists

Supervised Student Projects

Ongoing:

Nicolas Kaletsch
Verification of Information Flow Security in the Presence of Unverified Code [Download Description (PDF, 138 KB)]
Micha Greutmann, Bachelor's Thesis
Enabling Object Equality Reasoning for Python [Download Description (PDF, 211 KB)]
Etienne Birling, Master's Thesis
Cross-Language Verification of Python Modules Written in C [Download Description (PDF, 199 KB)]

Completed:

Victor Canard-Duchêne, Practical Work Project
Exploring Loop Pre- and Postconditions in Viper [Download Description]
Markus Limbeck, Master's Thesis
Enhancing Deductive Verification of Unbounded Heap Data Structures [Download Description (PDF, 186 KB)]
Pascal Devenoge, Bachelor's Thesis
Specification of Python Math and Data Science Libraries [Download Report (PDF, 3.6 MB)]
Edgars Vitolins, Master's Thesis
Verification of Python Code with a Dynamic Object Model [Download Report (PDF, 549 KB)]
Frédéric Necker, Master's Thesis
Verification of Object Invariants in the Presence of Unverified Code [Download Report (PDF, 683 KB)]
Andrea Keusch, Practical Work Project
Adding Debugging Functionality to Viper [Download Report (PDF, 555 KB)]
Patricia Firlejczyk, Bachelor's Thesis
Specifying and Verifying Static Initialization in Deductive Program Verifiers
Raoul van Doren, Bachelor's Thesis
Advanced Counterexample Generation in Viper [Report]
Christian Bräm, Master's Thesis
Verification of Advanced Properties for Real World Vyper Contracts [Report]
Constantin Müller, Master's Thesis
Verification of Programs Written in Libra's Move Language [Report]
Robin Sierra, Master's Thesis
Verification of Ethereum Smart Contracts Written in Vyper [Report]
Mathias Blarer, Bachelor's Thesis
Static Analysis of GPU Kernel Performance Hyperproperties [Report]
Pavel Pozdnyakov, Bachelor's Thesis
Lightweight Automatic Loop Invariant Selection [Report]
Severin Meier, Master's Thesis
Verification of Information Flow Security for Python Programs [Report]
Sascha Forster, Bachelor's Thesis
Static Verification of the SCION Router Implementation [Report]
Christian Knabenhans, Bachelor's Thesis
Automatic Inference of Hyperproperties [Report]
Benjamin Schmid, Bachelor's Thesis
Abstract Read Permission Support for an Automatic Python Verifier [Report]
Benjamin Weber, Master's Thesis
Automatic Verification of Closures and Lambda-Functions in Python [Report]
Mostafa Hassan, Bachelor's Thesis
Static Type Inference for Python [Report]
Vytautas Astrauskas, Master's Thesis
Input/Output Verification in Viper [Report]