Nagini: A Static Verifier for Python. - Marco Eilers; Peter Müller 001 (CAV (1), 2018)

MaxSMT-Based Type Inference for Python 3. - Mostafa Hassan; Caterina Urban; Marco Eilers; Peter Müller 001 (CAV (2), 2018)

Igloo: soundly linking compositional refinement and separation logic for distributed system verification. - Christoph Sprenger 001; Tobias Klenze; Marco Eilers; Felix A. Wolf; Peter Müller 001; Martin Clochard; David A. Basin (Proc. ACM Program. Lang., 2020)

Modular Product Programs. - Marco Eilers; Peter Müller 001; Samuel Hitz (ACM Trans. Program. Lang. Syst., 2020)

Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. - Marco Eilers; Severin Meier; Peter Müller 001 (CAV (1), 2021)

Modular Verification of Collaborating Smart Contracts. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (CoRR, 2021)

Rich specifications for Ethereum smart contract verification. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

Modular Specification and Verification of Security Properties for Mainstream Languages. - Marco Eilers (2022)

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. - Marco Eilers; Thibault Dardinier; Peter Müller 001 (Proc. ACM Program. Lang., 2023)

Verification Algorithms for Automated Separation Logic Verifiers. - Marco Eilers; Malte Schwerhoff; Peter Müller 001 (CAV (1), 2024)

Protocols to Code: Formal Verification of a Next-Generation Internet Router. - João C. Pereira; Tobias Klenze; Sofia Giampietro; Markus Limbeck; Dionysios Spiliopoulos; Felix A. Wolf; Marco Eilers; Christoph Sprenger 001; David A. Basin; Peter Müller 001; Adrian Perrig (CoRR, 2024)

Fifteen Years of Viper. - Marco Eilers; Malte Schwerhoff; Alexander J. Summers; Peter Müller 001 (CAV (1), 2025)