Michael Sammler

21 papers A* 3B 1Journal 16
YearRankTypeTitle / Venue / Authors
2026 B conf
A Recipe for Modular Verification of Generic Tree Traversals.
CPP
Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg
2026 J jnl
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation.
Proc. ACM Program. Lang.
Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler
2025 J jnl
Destabilizing Iris.
Proc. ACM Program. Lang.
Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer
2025 J jnl
Formal Foundations for Translational Separation Logic Verifiers.
Proc. ACM Program. Lang.
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
2025 J jnl
HITrees: Higher-Order Interaction Trees.
CoRR
Amir Mohammad Fadaei Ayyam, Michael Sammler
2025 J jnl
Program Logics à la Carte.
Proc. ACM Program. Lang.
Max Vistrup, Michael Sammler, Ralf Jung
2025 J jnl
RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.
Proc. ACM Program. Lang.
Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn B. Brandenburg, Derek Dreyer, Deepak Garg
2024 J jnl
Formal Foundations for Translational Separation Logic Verifiers (extended version).
CoRR
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
2024 J jnl
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.
Proc. ACM Program. Lang.
Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
2024 J jnl
RefinedRust: A Type System for High-Assurance Verification of Rust Programs.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
2023 — —
Automated and foundational verification of low-level programs.
Michael Sammler
2023 J jnl
Conditional Contextual Refinement.
Proc. ACM Program. Lang.
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
2023 J jnl
DimSum: A Decentralized Approach to Multi-language Semantics and Verification.
Proc. ACM Program. Lang.
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
2023 J jnl
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Proc. ACM Program. Lang.
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
2022 J jnl
BFF: foundational and automated verification of bitfield-manipulating programs.
Proc. ACM Program. Lang.
Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg
2022 A* conf
Islaris: verification of machine code against authoritative ISA semantics.
PLDI
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
2022 J jnl
Simuliris: a separation logic framework for verifying concurrent program optimizations.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
2022 J jnl
VIP: verifying real-world C idioms with integer-pointer casts.
Proc. ACM Program. Lang.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
2021 A* conf
RefinedC: automating the foundational verification of C code with refined ownership types.
PLDI
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
2020 J jnl
The high-level benefits of low-level sandboxing.
Proc. ACM Program. Lang.
Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak
2019 A* conf
ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK).
USENIX Security Symposium
Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, Deepak Garg