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

I will be joining ISTA as an assistant professor and I am looking for motivated PhD students, postdocs, and interns. If you are interested, please send me an email.

Publications

  • 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
    Distinguished Paper
  • VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
    Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
  • 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
  • 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

  • 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

Imprint / Data Protection