Marco Eilers

About Me

Photo

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

 

Tools

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:

Completed:

  • Andrea Keusch, Practical Work Project
    Adding Debugging Functionality to Viper [DownloadDescription (PDF, 141 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]

Contact


JavaScript has been disabled in your browser