About Me

Hi, I am Michael Sammler.

When I am not skiing or traveling the world, I am a post-doc in the Programming Methodology Group at ETH Zürich. Before that, I was a PhD student with Deepak Garg and Derek Dreyer at the Max Planck Institute for Software Systems and Saarland Informatics Campus.

My interests lie in implementing efficient and practical systems and formally proving properties about them. In particular, my research focuses on building formal verification tools for low-level systems code that combine foundational proofs in a proof assistant with a high degree of automation. My main projects in this area are RefinedC, which uses a refinement and ownership type system to verify C code, Islaris, which shows how to scale verification of assembly code to realistic models of real-world architectures, and DimSum, which provides a decentralized approach for reasoning about multi-language programs.

My publications can be either found below or at dblp. Contact details are here.

Publications

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer

PLDI'24 PDF, Website

Distinguished Artifact Award
RefinedRust: A Type System for High-Assurance Verification of Rust Programs

Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer

PLDI'24 PDF, Website
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer

OOPSLA'23 PDF, Website
DimSum: A Decentralized Approach to Multi-language Semantics and Verification

Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer

POPL'23 PDF, Slides, Website, Artifact

Distinguished Paper
Conditional Contextual Refinement

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer

POPL'23 PDF, Website, Artifact
BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg

OOPSLA'22 PDF, Website, Artifact
Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

PLDI'22 PDF, Code, Artifact, Talk
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations

Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer

POPL'22 PDF, Code, Artifact and Appendix, Talk

Distinguished Paper
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell

POPL'22 PDF, Code, Artifact and Appendix, Talk
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

PLDI'21 PDF, Website, Code, Talk

Distinguished Paper and Distinguished Artifact Award
The High-Level Benefits of Low-Level Sandboxing

Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak

POPL'20 PDF, Coq Formalization, VM, Talk
ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK)

Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, Deepak Garg

USENIX Security'19 PDF, Code

Distinguished Paper and Internet Defense Prize

Thesis

Automated and Foundational Verification of Low-Level Programs

PhD Thesis

Defended in December 2023

Screen-optimized PDF, Print-optimized PDF (official final version), hdl:20.500.11880/37089, Website

Runner-Up for Informatics Europe 2024 Best Dissertation Award and Dr. Eduard Martin Prize

Talks

Stories from my PhD at Professional Development Workshop for Early Career Researchers, ECSS'24
Formal Foundations for Translational Separation Logic Verifiers at Big Specification Workshop 2024, Talk
Automated and Foundational Verification of Low-Level Programs at EPFL
Building automated and foundational verification tools with Lithium at Swiss Verification Day 2024, Slides
DimSum: A Decentralized Approach to Multi-language Semantics and Verification at POPL'23 and at CMU's Principles of Programming seminar
Islaris: Verification of Machine Code Against Authoritative ISA Semantics at PLDI'22 (together with Angus Hammond), Talk
Predictable, efficient, and extensible Iris automation with Lithium at Iris Workshop'22, Slides, Code
RefinedC (invited tutorial) at Verify This'22, Slides, Code
RustBelt: A Quick Dive Into the Abyss at RustVerify'21 (invited talk, together with Ralf Jung), Slides
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types at PLDI'21 and at PLDI'22, Talk
The High-Level Benefits of Low-Level Sandboxing at POPL'20, Talk

Awards

Runner-Up for Informatics Europe 2024 Best Dissertation Award for Automated and Foundational Verification of Low-Level Programs
Dr. Eduard Martin Prize for Automated and Foundational Verification of Low-Level Programs
PLDI'24: Distinguished Artifact Award for Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
2020-2023: Google PhD Fellowship
POPL'23: Distinguished Paper Award for DimSum: A Decentralized Approach to Multi-language Semantics and Verification
POPL'22: Distinguished Paper Award for Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
PLDI'21: Distinguished Paper Award and Distinguished Artifact Award for RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
VerifyThis'21: Most distinguished tool feature award for RefinedC
USENIX Security'19: Internet Defense Prize and Distinguished Paper Award for ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK)