Azalea Raad
where else to find them
no profile links on file
what they talk about
all 8 in the filters
where they keep going back
all 7 in the filters
on a stage with
all 40 in the filters
who talks about the same things
- Viktor Vafeiadis23 talks
- Ori Lahav17 talks
- Parosh Aziz Abdulla9 talks
- Jeehoon Kang14 talks
- John Wickerson14 talks
- Peter Sewell14 talks
| title | conference | date |
|---|---|---|
| U-Turn: Enhancing Incorrectness Analysis by Reversing Direction | POPL 2026 | 2026-01-11 |
Combines forward Incorrectness Logic derivations with backward Sufficient Incorrectness Logic by instrumenting backward proof rules with the forward derivation… | ||
| A Verified High-Performance Composable Object Library for Remote Direct Memory Access | POPL 2026 | 2026-01-11 |
LOCO is a verified C++ RDMA object library that implements ring buffers, barriers and a key‑value store atop a single-thread manager for hardware completion… | ||
| Bayesian Separation Logic | POPL 2026 | 2026-01-11 |
Introduces a separation logic that actually models Bayesian updating and scoring, proving an internal Bayes' theorem by invoking the Rokhlin‑Simmons… | ||
| Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…) | TPSA 2025 | 2025-01-19 |
Claims a fully automatic under-approximate method that refutes type soundness in libraries by encoding type assignments as separation-logic assertions and… | ||
| U-turn: Forward-driven backward analysis for incorrectness | TPSA 2025 | 2025-01-19 |
Combines forward IL to produce only true reachable errors with a backward SIL proof that extracts the actual preconditions responsible for those errors… | ||
| Extending the C/C++ Memory Model with Inline Assembly | OOPSLA 2024 | 2024-10-20 |
A formal memory model is built that extends RC11 to handle inline x86 assembly, specifically first C++ model with inline assembly for x86 covering non-temporal… | ||
| Non-Termination Proving at Scale | OOPSLA 2024 | 2024-10-20 |
Claims a sound and complete under-approximate logic called UNTerSL that composes incorrectness/divergence reasoning with separation logic and bi-abduction to… | ||
| Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA(…) | OOPSLA 2024 | 2024-10-20 |
Claims a first formal semantics for RDMA on x86‑TSO: three equivalent models (two operational at different abstraction levels, one declarative), with a… | ||
| Under-approximation for Scalable Bug Detection | CPP 2024 | 2024-01-15 |
Presents a concrete under‑approximate program logic, Incorrectness Separation Logic, and an automated analyzer Pulse‑X that targets memory‑safety bugs (null… | ||
| Welcome | The Future of Weak Memory 2024 | 2024-01-15 |
Program opens by defining weak versus strong memory and lists concrete agenda items: empirical validation of memory persistency models, tooling for checking… | ||
| Introduction | O'Hearn Fest (POPL 2024) | 2024-01-14 |
Brief history and concrete impact: seminal papers on concurrent separation logic (2004) and the original separation logic paper accumulate major influence —… | ||
| Memento: A Framework for Detectable Recoverability in Persistent Memory | PLDI 2023 | 2023-06-17 |
Memento is a programming framework that proves and enforces detectable recoverability for persistent memory by using a timestamp-based recovery strategy plus… | ||
| The Path to Durable Linearizability | POPL 2023 | 2023-01-15 |
Proposes a concrete method that converts an existing linearizability proof into durable correctness by adding small, checkable Delta proof obligations that… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| Finding real bugs in big programs with incorrectness logic | OOPSLA 2022 | 2022-12-05 |
Pulse-X applies ISL (a synthesis of Incorrectness Logic and separation logic) to build an automatic under-approximate analyzer for memory errors, inferring… | ||
| Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of In | POPL 2022 | 2022-01-16 |
Extends x86 semantics to cover non-temporal stores and page memory types, delivering EX86/PEx86 models in both operational and declarative forms and proving… | ||
| Concurrent Incorrectness Separation Logic | POPL 2022 | 2022-01-16 |
Develops CISL as a parametric extension of Incorrectness Separation Logic that models concurrency with histories and lock-aware events, instantiates to race… | ||
| PerSeVerE: Persistency Semantics for Verification under Ext4 | POPL 2021 | 2021-01-17 |
Formal semantics for ext4 are derived from the kernel implementation and stress tests and integrated with C/C++ weak-memory models; a model-checker then… | ||
| Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel- | OOPSLA 2020 | 2020-11-15 |
The paper introduces POG, the first program logic for persistent x86, and an Ix86 instrumented semantics that reduces Px86 by removing the pbuffer via a… | ||
| Persistence Semantics for Weak Memory | OOPSLA 2018 | 2018-11-07 |
Introduces PTSO: an integration of epoch persistency with x86/SPARC TSO that gives both operational and declarative semantics and a machine-checked proof of… | ||
| nothing matches | ||