Philippa Gardner
where else to find them
what they talk about
all 8 in the filters
where they keep going back
- POPL3 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2025
all 10 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Xiaojia Rao3 talks
- Conrad Watt12 talks
- Jean Pichon-Pharabod12 talks
- Aina Linn Georges12 talks
- Bryan Parno22 talks
- Maxime Legoupil5 talks
| title | conference | date |
|---|---|---|
| Compositional Symbolic Execution for the Next 700 Memory Models | OOPSLA 2025 | 2025-10-16 |
Presents a mechanized formal foundation for memory-model‑parametric compositional symbolic execution, claiming soundness for both separation logic and… | ||
| Verification of WebAssembly Features | RPLS 2025 | 2025-06-17 |
A mechanized WebAssembly semantics exists in Isabelle mechanization and parallel mechanizations target Rock/MetaRoc, with proven preservation and progress for… | ||
| A Hybrid Approach to Semi-automated Rust Verification | PLDI 2025 | 2025-06-16 |
A prototype hybrid verifier links Gillian-Rust (symbolic-execution + separation logic) with Creusot so safe Rust specs are checked automatically while unsafe… | ||
| Progressful Interpreters for Efficient WebAssembly Mechanisation | POPL 2025 | 2025-01-19 |
Implements a progressful interpreter in Coq that uses dependent types to certify both soundness and progress, and extracts an executable with proofs erasable… | ||
| Bringing the WebAssembly Standard up to Speed with SpecTec | PLDI 2024 | 2024-06-24 |
SpecTec is a DSL and toolchain that serves as a single source of truth for Wasm semantics, generating typeset spec prose, formal definitions, and a meta-level… | ||
| Unified Compositional Symbolic Execution | N40AI 2024 | 2024-01-20 |
Claims a unified engine that combines OX (correctness) and UX (incorrectness) reasoning via an axiomatic interface and parametric consume/produce functions… | ||
| Unified Compositional Formal Methods: Exact Separation Logic and the Gi... | Incorrectness 2024 | 2024-01-17 |
Claims a single exact separation logic (ESL) that is sound for both over‑approximate verification and under‑approximate bug finding, formalizes an… | ||
| Mechanising WebAssembly Well? | WAW 2024 | 2024-01-15 |
Mechanization of WebAssembly focuses on two concrete routes: an extrinsic approach where preservation + progress yields an interpreter for free, and a… | ||
| Welcome To POPL 2024 | POPL 2024 | 2024-01-14 |
Announcements cover health precautions with hand sanitizers around and a request to take care after recent COVID cases, plus exact catering logistics: two… | ||
| Verified Software at Scale | O'Hearn Fest (POPL 2024) | 2024-01-14 |
Mechanized WebAssembly semantics now feed the standard, with a formal DSL that produces parser tests, reference interpreters and automatically generated… | ||
| SIGPLAN Awards, PC Chair's Report, and Business Meeting | POPL 2024 | 2024-01-14 |
Conference report gives concrete numbers and decisions: 319 submissions with 93 accepted, a single flat 86‑member PC, and adoption of full double blind review… | ||
| Concluding Remarks | POPL 2024 | 2024-01-14 |
Conference closes with thanks to Eric Drer for long‑running PC leadership, the AV team for fixing recurring integration hiccups, and the student volunteers who… | ||
| Iris-Wasm: Robust and Modular Verification of WebAssembly Programs | PLDI 2023 | 2023-06-17 |
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds… | ||
| TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr | POPL 2022 | 2022-01-16 |
TaDA Live claims compositional proofs of termination for blocking fine‑grained concurrent programs by extending separation logic with a semantic model of… | ||
| Gillian: a Multi-language Platform for Compositional Symbolic Analysis | SPLASH 2020 REBASE | 2020-11-16 |
Gillian is a multi-language symbolic-analysis platform that implements a core symbolic-execution engine backed by Z3, OCaml concrete and symbolic memory… | ||
| Gillian a Multi language Platform for Compositional (...) | Code Mesh LDN 2020 | 2020-11-05 |
Gillian is a multi-language symbolic-analysis platform that currently supports JavaScript and C and uses a core symbolic execution engine plus a first-order… | ||
| nothing matches | ||