About Me

Hi, I am Michael Sammler.

When I am not skiing or traveling the world, I am a PhD Student with Deepak Garg and Derek Dreyer at the Max Planck Institute or Software Systems and Saarland Informatics Campus.

My interests lie in implementing efficient and practical systems and formally proving properties about them. For this, I am currently developing RefinedC. RefinedC combines automated verification (via a refinement and ownership type system) of C code with foundational guarantees (based on the Iris framework).

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

Publications

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
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

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
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

Talks

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, Talk
The High-Level Benefits of Low-Level Sandboxing at POPL'20, Talk

Awards

2020-today: Google PhD Fellowship
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)