Ori Lahav
where else to find them
linkedin:ori-lahav
what they talk about
all 5 in the filters
where they keep going back
- OOPSLA3 editions2020–2024
- POPL2 editions2021–2023
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2025
all 7 in the filters
on a stage with
all 21 in the filters
who talks about the same things
- Viktor Vafeiadis23 talks
- Azalea Raad27 talks
- Roy Margalit3 talks
- Michalis Kokologiannakis12 talks
- Jeehoon Kang14 talks
- Andreas Pavlogiannis18 talks
| title | conference | date |
|---|---|---|
| Dynamic Robustness Verification against Weak Memory | PLDI 2025 | 2025-06-16 |
Algorithm verifies robustness against C11/C++20 weak memory using location clocks and runs as the RSAN/Arson tool that reports full backtraces for violations… | ||
| 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… | ||
| 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… | ||
| A case against semantic dependencies | The Future of Weak Memory 2024 | 2024-01-15 |
Argues that the proposed three-step C/C++ fix—derive a global semantic dependency from all candidate executions then apply RC11 consistency—fails on concrete… | ||
| A Denotational Approach to Release/Acquire Concurrency | GALOP 2024 | 2024-01-14 |
Presents a directionally adequate denotational semantics for Release/Acquire memory using Brookes-style trace semantics adapted to a view-based machine; traces… | ||
| Putting Weak Memory in Order via a Promising Intermediate Representation | PLDI 2023 | 2023-06-17 |
Claims an in-order source semantics for C/C++ that preserves all common compiler optimizations for non-atomics by compiling to an out-of-order IR with… | ||
| An Operational Approach to Library Abstraction under Relaxed Memory Concurrency | POPL 2023 | 2023-01-15 |
Claims a library-abstraction theorem for RC11-style weak memory by giving an operational semantics exposing knowledge propagation that records propagation… | ||
| Kater: Automating Weak Memory Model Metatheory and Consistency Checking | POPL 2023 | 2023-01-15 |
Kater reduces meta theoretic questions about axiomatic weak memory models to language inclusion between CAT expressions, proving decidability for a wide class… | ||
| An Algebraic Theory for Shared-State Concurrency | APLAS 2022 | 2022-12-05 |
Presents a concrete monadic denotational model for a higher‑order language with shared‑state interleaving concurrency, proving a representation theorem that… | ||
| Making Weak Memory Models Fair | OOPSLA 2021 | 2021-10-17 |
Proposes a uniform memory fairness condition for declarative weak memory models (requires porf-acyclicity) and proves it is equivalent to natural operational… | ||
| Taming x86-TSO Persistency | POPL 2021 | 2021-01-17 |
Proposes a new synchronous PTSO model that eagerly persists writes and proves it reaches the same non‑volatile states as the asynchronous POPL’20 model — a… | ||
| Verifying Observational Robustness Against a C11-style Memory Model | POPL 2021 | 2021-01-17 |
Proves robustness against the C11-style model is decidable (PSPACE-complete) by a concrete reduction to SC reachability, implements that instrumentation in the… | ||
| 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… | ||
| The Reversim Story | Reversim Summit 2019 | 2019-06-16 |
How, when and where did the podcast and the conference came to be. Stories behind the scenes and the unwritten (unspoken) history of technical content in… | ||
| nothing matches | ||