Michael Sammler

Publication Activity (10 Years)

Years Active: 2019-2024
Publications (10 Years): 13

Top Topics

Formal Language

Logic Programming

High Level Information

Top Venues

Proc. ACM Program. Lang.

USENIX Security Symposium

Publications

Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
Formal Foundations for Translational Separation Logic Verifiers (extended version). CoRR (2024)
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
Conditional Contextual Refinement. Proc. ACM Program. Lang. 7 (POPL) (2023)
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6 (POPL) (2022)
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
Islaris: verification of machine code against authoritative ISA semantics. PLDI (2022)
Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg
BFF: foundational and automated verification of bitfield-manipulating programs. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6 (POPL) (2022)
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
RefinedC: automating the foundational verification of C code with refined ownership types. PLDI (2021)
Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak
The high-level benefits of low-level sandboxing. Proc. ACM Program. Lang. 4 (POPL) (2020)
Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, Deepak Garg
ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK). USENIX Security Symposium (2019)