Michael Sammler

According to our database, Michael Sammler authored at least 22 papers between 2019 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation.

Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler

Proc. ACM Program. Lang., 2026

A Recipe for Modular Verification of Generic Tree Traversals.

Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

HITrees: Higher-Order Interaction Trees.

Amir Mohammad Fadaei Ayyam, Michael Sammler

CoRR, October, 2025

Program Logics à la Carte.

Max Vistrup, Michael Sammler, Ralf Jung

Proc. ACM Program. Lang., 2025

Destabilizing Iris.

Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer

Proc. ACM Program. Lang., 2025

Formal Foundations for Translational Separation Logic Verifiers.

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

Proc. ACM Program. Lang., 2025

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

Proc. ACM Program. Lang., 2025

2024

Formal Foundations for Translational Separation Logic Verifiers - Artifact.

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

Dataset, October, 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

RefinedRust: A Type System for High-Assurance Verification of Rust Programs.

Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer

Proc. ACM Program. Lang., 2024

Formal Foundations for Translational Separation Logic Verifiers (extended version).

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

CoRR, 2024

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., October, 2023

Conditional Contextual Refinement.

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer

Proc. ACM Program. Lang., January, 2023

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

Proc. ACM Program. Lang., January, 2023

Automated and foundational verification of low-level programs.

Michael Sammler

PhD thesis, 2023

2022

BFF: foundational and automated verification of bitfield-manipulating programs.

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg

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

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

Proc. ACM Program. Lang., 2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

RefinedC: automating the foundational verification of C code with refined ownership types.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

The high-level benefits of low-level sandboxing.

Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak

Proc. ACM Program. Lang., 2020

2019

ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK).

Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, Deepak Garg

Proceedings of the 28th USENIX Security Symposium, 2019