Marco Eilers
About Me
I recently defended my PhD at the Programming Methodology Group at ETH (supervised by Prof. Peter Müller) where I will continue 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.
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. Additionally, I worked on the VerifiedSCION project whose goal is the full-stack verification of a new internet architecture; my focus was on formally connecting code verification and protocol verification.
Publications
- M. Eilers, T. Dardinier and P. Müller, CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Programming Language Design and Implementation (PLDI), 2023. [PDF] [external pagePublishercall_made] [external pageTalkcall_made] [external pagearXivcall_made] - 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 pagePublishercall_made] [external pageTalkcall_made] [external pageExtended TRcall_made]
- 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 pagePublishercall_made] [external pageTalkcall_made] - 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 pagePublishercall_made] [external pageTalkcall_made] [external pageExtended TRcall_made]
- M. Eilers, P. Müller and S. Hitz, Modular Product Programs
In ACM Transactions on Programming Languages and System (TOPLAS), 2020. [PDF] [external pagePublishercall_made]
- M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [PDF] [external pagePublishercall_made] [DownloadSlides (PDF, 908 KB)vertical_align_bottom]
- 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 pagePublishercall_made] [DownloadSlides (PDF, 975 KB)vertical_align_bottom]
- M. Eilers, P. Müller and S. Hitz, Modular Product Programs
In European Symposium on Programming (ESOP), 2018. [PDF] [external pagePublishercall_made] [DownloadSlides (PDF, 375 KB)vertical_align_bottom]
Tools
- Nagini, a static verifier for Python 3: [external pageGithubcall_made]
- HyperViper, a verifier for information flow security for concurrent programs: [external pageGithubcall_made]
- 2vyper, a verifier for Vyper smart contracts: [external pageGithubcall_made]
- Typpete, SMT-based type inference for Python: [external pageGithubcall_made]
- 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 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:
- Pascal Devenoge, Bachelor's Thesis
Specification of Python Math and Data Science Libraries [DownloadDescription (PDF, 173 KB)vertical_align_bottom]
- Edgars Vitolins, Master's Thesis
Verification of Python Code with a Dynamic Object Model [DownloadDescription (PDF, 126 KB)vertical_align_bottom] - Frédéric Necker, Master's Thesis
Verification of Object Invariants in the Presence of Unverified Code [DownloadDescription (PDF, 135 KB)vertical_align_bottom]
Completed:
- Andrea Keusch, Practical Work Project
Adding Debugging Functionality to Viper [DownloadDescription (PDF, 141 KB)vertical_align_bottom] - 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]
Contact