Viktor Vafeiadis
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL5 editions2021–2026
- OOPSLA3 editions2020–2024
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2024
all 4 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Ori Lahav17 talks
- Azalea Raad27 talks
- Michalis Kokologiannakis12 talks
- Andreas Pavlogiannis18 talks
- Jeehoon Kang14 talks
- Peter Sewell14 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… | ||
| Model Checking C/C++ with Mixed-Size Accesses | POPL 2025 | 2025-01-19 |
Presents an algorithm that lets a DPOR-based model checker handle C/C++ mixed-size accesses by treating whole instructions atomically while allowing revisits… | ||
| RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency | POPL 2025 | 2025-01-19 |
RELINCHE is a model checker that verifies per-object atomicity plus preserved synchronization under weak memory by establishing refinement between an… | ||
| 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… | ||
| SPORE: Combining Symmetry and Partial Order Reduction | PLDI 2024 | 2024-06-24 |
SPORE is a stateless model checker that actually combines symmetry reduction and dynamic partial order reduction to cut interleavings exponentially; it proves… | ||
| BWoS: Formally Verified Block-based Work Stealing for Parallel Processing | OSDI 2023 | 2023-07-10 |
Presents Block-based Work Stealing (BWoS), a queue design that splits per-core queues into fixed-size blocks so owners work inside a block using relaxed… | ||
| 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… | ||
| Principles of Persistent Programming | POPL 2023 | 2023-01-15 |
Defines a formal semantics that composes weak-memory consistency with a separate persistency order, gives both operational and declarative characterizations… | ||
| 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… | ||
| Differential Cost Analysis with Simultaneous Potentials and Anti-potentials | PLDI 2022 | 2022-06-13 |
A prototype automatically synthesizes simultaneous potentials and anti-potentials as polynomial templates, translates the universal polynomial constraints via… | ||
| Finding Typing Compiler Bugs | PLDI 2022 | 2022-06-13 |
Ephesus builds a program generator that emits large (500–1000 line) polymorphic programs and two transformation tests: type erasure mutation removes optional… | ||
| Lasagne: A Static Binary Translator for Weak Memory Model Architectures | PLDI 2022 | 2022-06-13 |
Lasagne is a static x86→ARM translator that lifts x86 binaries to LLVM IR (via Microsoft mactool), applies pattern-based IR refinements to recover pointer… | ||
| Truly Stateless, Optimal Dynamic Partial Order Reduction | POPL 2022 | 2022-01-16 |
Claim: TruSt explores exactly one interleaving per Mazurkiewicz-equivalence class while using linear (paper shows how to get from N^2 to linear) memory instead… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| nothing matches | ||