Brijesh Dongol
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
- OOPSLA2 editions2022–2024
all 6 in the filters
on a stage with
all 23 in the filters
who talks about the same things
- Guillaume Ambal3 talks
- Vasileios Klimis4 talks
- Mark Batty5 talks
- Ori Lahav17 talks
- Azalea Raad27 talks
- Simon Cooksey4 talks
| title | conference | date |
|---|---|---|
| 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… | ||
| 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… | ||
| Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM | USENIX ATC 2024 | 2024-07-10 |
Mangosteen converts a linearizable in-memory app to durably linearizable NVM-backed code using six callback hooks, runtime binary instrumentation for… | ||
| 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… | ||
| A Fully Verified Persistency Library | VMCAI 2024 | 2024-01-15 |
Claims a sound, machine-checked correctness path showing that the FliT durability transformation refines an abstract PLib abstract persistency library… | ||
| Proving Memory Access Violations in Isabelle/HOL | FTSCS 2022 | 2022-12-07 |
Verifies memory isolation for SmuV and TrustLite by translating compiled C through BAP and BIL into Isabelle/HOL theories, extending the pipeline to produce… | ||
| Implementing and Verifying Release-Acquire Transactional Memory in C11 | OOPSLA 2022 | 2022-12-05 |
Defines a relaxed transactional-memory spec called TMS2-ra integrated with RC11 (view-based RC11) and a program logic TARO, implements the spec as a C11… | ||
| nothing matches | ||