Michael Sammler

According to our database, Michael Sammler authored at least 14 papers between 2019 and 2024.

Collaborative distances:

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

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