Lennard Gäher
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
all 5 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Michael Sammler16 talks
- Derek Dreyer35 talks
- Simon Spies8 talks
- Peter Müller28 talks
- Jeehoon Kang14 talks
- Ralf Jung18 talks
| title | conference | date |
|---|---|---|
| Building Blocks for Step-Indexed Program Logics | CPP 2026 | 2026-01-12 |
Claims a single modular physical-step modality lets program-logic designers recover every prior multiple-later elimination technique without redoing… | ||
| 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… | ||
| 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… | ||
| Stuttering for Free | OOPSLA 2023 | 2023-10-23 |
Presents FreeSim, a new stuttering-simulation technique mechanized in Coq that replaces the usual “synchronous progress” requirement with asynchronous… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | ICFP 2022 | 2022-09-11 |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| 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 | ||