Thibault Dardinier
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski4 editions2023–2026
- OOPSLA3 editions2022–2024
on a stage with
all 14 in the filters
who talks about the same things
- Peter Müller28 talks
- Gaurav Parthasarathy3 talks
- Michael Sammler16 talks
- Simon Spies8 talks
- Marco Eilers4 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| Hyper Separation Logic | PLDI 2026 | 2026-06-15 |
Introduces a logic that supports hyperproperties with arbitrary quantifier alternation over heap programs, proves soundness in Isabelle/HOL, and ships reusable… | ||
| PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs | PLDI 2025 | 2025-06-16 |
PulseCore is a new, mechanized concurrent separation logic implemented inside F★ that claims to support impredicative invariants and higher‑order ghost state… | ||
| 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… | ||
| Hypra: A Deductive Program Verifier for Hyper Hoare Logic | OOPSLA 2024 | 2024-10-20 |
Claims the first automated deductive technique for arbitrary hyperproperties by encoding sets of program states explicitly into an intermediate language and… | ||
| Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…) | PLDI 2024 | 2024-06-24 |
Adds a per-run Isabelle certificate generator to an existing Viper→Boogie translation, proving that whenever the generated Boogie program has no failing… | ||
| Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties | PLDI 2024 | 2024-06-24 |
Logic lifts pre/postconditions to properties of arbitrary sets of states and claims to capture exactly the class of hyperproperties over terminating… | ||
| Verification-Preserving Inlining in Automatic Separation Logic Verifiers | OOPSLA 2023 | 2023-10-23 |
Presents a provable criterion that makes bounded inlining safe for automatic separation-logic verifiers: a semantic condition (formalized in Isabelle/HOL) that… | ||
| CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…) | PLDI 2023 | 2023-06-17 |
Claims a verification method that proves non‑interference for concurrent programs without any timing assumptions by requiring commutativity of updates only on… | ||
| Fractional Resources in Unbounded Separation Logic | OOPSLA 2022 | 2022-12-05 |
Defines a new semantics where assertions may temporarily use unbounded states that allow more-than-one permission during evaluation, then reimpose 0–1… | ||
| nothing matches | ||