Michael Sammler
where else to find them
linkedin:michael-sammler
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2022–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
- OOPSLA2 editions2022–2023
all 5 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Simon Spies8 talks
- Derek Dreyer35 talks
- Lennard Gäher7 talks
- Peter Müller28 talks
- Jeehoon Kang14 talks
- Amin Timany16 talks
| title | conference | date |
|---|---|---|
| A Recipe for Modular Verification of Generic Tree Traversals | CPP 2026 | 2026-01-12 |
Presents a concrete verification recipe that models traversal state with a zipper with shadow and characterizes step types as action and silent steps, yielding… | ||
| Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…) | POPL 2026 | 2026-01-11 |
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation… | ||
| Destabilizing Iris | PLDI 2025 | 2025-06-16 |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…) | PLDI 2025 | 2025-06-16 |
Claims a machine‑checked end‑to‑end proof that an interrupt‑free, fixed‑priority, non‑preemptive scheduler meets response‑time bounds by connecting program… | ||
| A Semantic Approach to Robust Property Preservation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so… | ||
| Program logics à la carte | POPL 2025 | 2025-01-19 |
Combines reusable program-logic fragments for language effects (shared state, concurrency, nondeterminism) so logics can be composed rather than rebuilt. Uses… | ||
| Formal Foundations for Translational Separation Logic Verifiers | POPL 2025 | 2025-01-19 |
Provides a formal, mechanized framework that proves soundness of translational separation-logic verifiers by defining a core IVL with both operational and… | ||
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs | PLDI 2024 | 2024-06-24 |
RefinedRust presents a refinement type system that verifies both unsafe Rust and safe Rust by translating MIR into a Coq-embedded Rust model and checking… | ||
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq | PLDI 2024 | 2024-06-24 |
Quiver claims automated inference of full separation logic specs for C code while verifying soundness in Coq using Iris, implemented as a prototype atop… | ||
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C | OOPSLA 2023 | 2023-10-23 |
Melocoton claims the first formal semantics of the OCaml FFI and the first multi‑language program logic that reasons about OCaml and C interactions… | ||
| Conditional Contextual Refinement | POPL 2023 | 2023-01-15 |
A new refinement notion, Conditional Contextual Refinement (CCR), combines separation-logic pre/post conditions with transitive contextual refinement by… | ||
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification | POPL 2023 | 2023-01-15 |
DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a… | ||
| BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs | OOPSLA 2022 | 2022-12-05 |
A foundational, automated verifier encodes common bitfield patterns as structured bit vectors and implements partial, semantics-preserving operations (masking… | ||
| VIP: Verifying Real-World C Idioms with Integer-Pointer Casts | POPL 2022 | 2022-01-16 |
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| nothing matches | ||