ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK). - Anjo Vahldiek-Oberwagner; Eslam Elnikety; Nuno O. Duarte; Michael Sammler; Peter Druschel; Deepak Garg 001 (USENIX Security Symposium, 2019)

The high-level benefits of low-level sandboxing. - Michael Sammler; Deepak Garg 001; Derek Dreyer; Tadeusz Litak (Proc. ACM Program. Lang., 2020)

RefinedC: automating the foundational verification of C code with refined ownership types. - Michael Sammler; Rodolphe Lepigre; Robbert Krebbers; Kayvan Memarian; Derek Dreyer; Deepak Garg 001 (PLDI, 2021)

Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

VIP: verifying real-world C idioms with integer-pointer casts. - Rodolphe Lepigre; Michael Sammler; Kayvan Memarian; Robbert Krebbers; Derek Dreyer; Peter Sewell (Proc. ACM Program. Lang., 2022)

BFF: foundational and automated verification of bitfield-manipulating programs. - Fengmin Zhu; Michael Sammler; Rodolphe Lepigre; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2022)

Automated and foundational verification of low-level programs. - Michael Sammler (2023)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Conditional Contextual Refinement. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2023)

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 (Proc. ACM Program. Lang., 2023)

Formal Foundations for Translational Separation Logic Verifiers (extended version). - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (CoRR, 2024)

RefinedRust: A Type System for High-Assurance Verification of Rust Programs. - Lennard Gäher; Michael Sammler; Ralf Jung 002; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2024)

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. - Simon Spies; Lennard Gäher; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2024)

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers. - Kimaya Bedarkar; Laila Elbeheiry; Michael Sammler; Lennard Gäher; Björn B. Brandenburg; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2025)

Formal Foundations for Translational Separation Logic Verifiers. - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 2025)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Program Logics à la Carte. - Max Vistrup; Michael Sammler; Ralf Jung 002 (Proc. ACM Program. Lang., 2025)