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

  • 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

Awards

Imprint / Data Protection