Proving correctness of highly-concurrent linearisable objects. - Viktor Vafeiadis; Maurice Herlihy; Tony Hoare; Marc Shapiro 001 (PPoPP, 2006)

A Marriage of Rely/Guarantee and Separation Logic. - Viktor Vafeiadis; Matthew J. Parkinson (CONCUR, 2007)

Modular Safety Checking for Fine-Grained Concurrency. - Cristiano Calcagno; Matthew J. Parkinson; Viktor Vafeiadis (SAS, 2007)

Acute: High-level programming language design for distributed computation. - Peter Sewell; James J. Leifer; Keith Wansbrough; Francesco Zappa Nardelli; Mair Allen-Williams; Pierre Habouzit; Viktor Vafeiadis (J. Funct. Program., 2007)

Modular fine-grained concurrency verification. - Viktor Vafeiadis (2008)

Bi-abductive Resource Invariant Synthesis. - Cristiano Calcagno; Dino Distefano; Viktor Vafeiadis (APLAS, 2009)

Deny-Guarantee Reasoning. - Mike Dodds; Xinyu Feng 001; Matthew J. Parkinson; Viktor Vafeiadis (ESOP, 2009)

Finding heap-bounds for hardware synthesis. - Byron Cook; Ashutosh Gupta 001; Stephen Magill; Andrey Rybalchenko; Jirí Simsa; Satnam Singh; Viktor Vafeiadis (FMCAD, 2009)

Proving that non-blocking algorithms don't block. - Alexey Gotsman; Byron Cook; Matthew J. Parkinson; Viktor Vafeiadis (POPL, 2009)

Shape-Value Abstraction for Verifying Linearizability. - Viktor Vafeiadis (VMCAI, 2009)

Automatically Proving Linearizability. - Viktor Vafeiadis (CAV, 2010)

Concurrent Abstract Predicates. - Thomas Dinsdale-Young; Mike Dodds; Philippa Gardner; Matthew J. Parkinson; Viktor Vafeiadis (ECOOP, 2010)

Structuring the verification of heap-manipulating programs. - Aleksandar Nanevski; Viktor Vafeiadis; Josh Berdine (POPL, 2010)

RGSep Action Inference. - Viktor Vafeiadis (VMCAI, 2010)

Separation Logic in the Presence of Garbage Collection. - Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (LICS, 2011)

Relaxed-memory concurrency and verified compilation. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (POPL, 2011)

Verifying Fence Elimination Optimisations. - Viktor Vafeiadis; Francesco Zappa Nardelli (SAS, 2011)

Concurrent Separation Logic and Operational Semantics. - Viktor Vafeiadis (MFPS, 2011)

The marriage of bisimulations and Kripke logical relations. - Chung-Kil Hur; Derek Dreyer; Georg Neis; Viktor Vafeiadis (POPL, 2012)

Aspect-Oriented Linearizability Proofs. - Thomas A. Henzinger; Ali Sezgin; Viktor Vafeiadis (CONCUR, 2013)

Adjustable References. - Viktor Vafeiadis (ITP, 2013)

Relaxed separation logic: a program logic for C11 concurrency. - Viktor Vafeiadis; Chinmay Narayan (OOPSLA, 2013)

The power of parameterization in coinductive proof. - Chung-Kil Hur; Georg Neis; Derek Dreyer; Viktor Vafeiadis (POPL, 2013)

A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism. - Mustafa Zengin; Viktor Vafeiadis (TASE, 2013)

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (J. ACM, 2013)

GPS: navigating weak memory with ghosts, protocols, and separation. - Aaron Turon; Viktor Vafeiadis; Derek Dreyer (OOPSLA, 2014)

Automating the Choice of Consistency Levels in Replicated Systems. - Cheng Li 001; João Leitão 001; Allen Clement; Nuno M. Preguiça; Rodrigo Rodrigues 001; Viktor Vafeiadis (USENIX ATC, 2014)

Rely/Guarantee Reasoning for Asynchronous Programs. - Ivan Gavran; Filip Niksic; Aditya Kanade 001; Rupak Majumdar; Viktor Vafeiadis (CONCUR, 2015)

Proving Lock-Freedom Easily and Automatically. - Xiao Jia 001; Wei Li; Viktor Vafeiadis (CPP, 2015)

Formal Reasoning about the C11 Weak Memory Model. - Viktor Vafeiadis (CPP, 2015)

Asynchronous Liquid Separation Types. - Johannes Kloos; Rupak Majumdar; Viktor Vafeiadis (ECOOP, 2015)

Owicki-Gries Reasoning for Weak Memory Models. - Ori Lahav 001; Viktor Vafeiadis (ICALP (2), 2015)

Pilsner: a compositionally verified compiler for a higher-order imperative language. - Georg Neis; Chung-Kil Hur; Jan-Oliver Kaiser; Craig McLaughlin; Derek Dreyer; Viktor Vafeiadis (ICFP, 2015)

A formal C memory model supporting integer-pointer casts. - Jeehoon Kang; Chung-Kil Hur; William Mansky; Dmitri Garbuzov; Steve Zdancewic; Viktor Vafeiadis (PLDI, 2015)

Verifying read-copy-update in a logic for weak memory. - Joseph Tassarotti; Derek Dreyer; Viktor Vafeiadis (PLDI, 2015)

Separation logic for weak memory models. - Viktor Vafeiadis (PLMW@POPL, 2015)

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. - Viktor Vafeiadis; Thibaut Balabonski; Soham Chakraborty 001; Robin Morisset; Francesco Zappa Nardelli (POPL, 2015)

Modular Verification of Concurrency-Aware Linearizability. - Nir Hemed; Noam Rinetzky; Viktor Vafeiadis (DISC, 2015)

Aspect-oriented linearizability proofs. - Soham Chakraborty 001; Thomas A. Henzinger; Ali Sezgin; Viktor Vafeiadis (Log. Methods Comput. Sci., 2015)

Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). - Parosh Aziz Abdulla; Fabio Gadducci; Barbara König 001; Viktor Vafeiadis (Dagstuhl Reports, 2015)

Mtac: A monad for typed tactic programming in Coq. - Beta Ziliani; Derek Dreyer; Neelakantan R. Krishnaswami; Aleksandar Nanevski; Viktor Vafeiadis (J. Funct. Program., 2015)

Validating optimizations of concurrent C/C++ programs. - Soham Chakraborty 001; Viktor Vafeiadis (CGO, 2016)

Explaining Relaxed Memory Models with Program Transformations. - Ori Lahav 001; Viktor Vafeiadis (FM, 2016)

Reasoning about Fences and Relaxed Atomics. - Mengda He; Viktor Vafeiadis; Shengchao Qin; João F. Ferreira 001 (PDP, 2016)

Lightweight verification of separate compilation. - Jeehoon Kang; Yoonseung Kim; Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (POPL, 2016)

Taming release-acquire consistency. - Ori Lahav 001; Nick Giannarakis; Viktor Vafeiadis (POPL, 2016)

A Program Logic for C11 Memory Fences. - Marko Doko; Viktor Vafeiadis (VMCAI, 2016)

Geo-Replication: Fast If Possible, Consistent If Necessary. - Valter Balegas; Cheng Li 001; Mahsa Najafzadeh; Daniel Porto 002; Allen Clement; Sérgio Duarte; Carla Ferreira 001; Johannes Gehrke; João Leitão 001; Nuno M. Preguiça; Rodrigo Rodrigues 001; Marc Shapiro 001; et al. (IEEE Data Eng. Bull., 2016)

Program Verification Under Weak Memory Consistency Using Separation Logic. - Viktor Vafeiadis (CAV (1), 2017)

Formalizing the concurrency semantics of an LLVM fragment. - Soham Chakraborty 001; Viktor Vafeiadis (CGO, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Promising Compilation to ARMv8 POP. - Anton Podkopaev; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Tackling Real-Life Relaxed Concurrency with FSL++. - Marko Doko; Viktor Vafeiadis (ESOP, 2017)

Repairing sequential consistency in C/C++11. - Ori Lahav 001; Viktor Vafeiadis; Jeehoon Kang; Chung-Kil Hur; Derek Dreyer (PLDI, 2017)

A promising semantics for relaxed-memory concurrency. - Jeehoon Kang; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis; Derek Dreyer (POPL, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2017)

On Parallel Snapshot Isolation and Release/Acquire Consistency. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (ESOP, 2018)

A Separation Logic for a Promising Semantics. - Kasper Svendsen; Jean Pichon-Pharabod; Marko Doko; Ori Lahav 001; Viktor Vafeiadis (ESOP, 2018)

GPS+: Reasoning About Fences and Relaxed Atomics. - Mengda He; Viktor Vafeiadis; Shengchao Qin; João F. Ferreira 001 (Int. J. Parallel Program., 2018)

Effective stateless model checking for C/C++ concurrency. - Michalis Kokologiannakis; Ori Lahav 001; Konstantinos Sagonas; Viktor Vafeiadis (Proc. ACM Program. Lang., 2018)

Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. - Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2018)

Model checking for weakly consistent libraries. - Michalis Kokologiannakis; Azalea Raad; Viktor Vafeiadis (PLDI, 2019)

On the Semantics of Snapshot Isolation. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (VMCAI, 2019)

Grounding thin-air reads with event structures. - Soham Chakraborty 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Effective lock handling in stateless model checking. - Michalis Kokologiannakis; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Bridging the gap between programming languages and hardware weak memory models. - Anton Podkopaev; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. - Azalea Raad; Marko Doko; Lovro Rozic; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. - Azalea Raad; John Wickerson; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

HMC: Model Checking for Hardware Memory Models. - Michalis Kokologiannakis; Viktor Vafeiadis (ASPLOS, 2020)

Reconciling Event Structures with Modern Multiprocessors. - Evgenii Moiseenko; Anton Podkopaev; Ori Lahav 001; Orestis Melkonian; Viktor Vafeiadis (ECOOP, 2020)

Promising 2.0: global optimizations in relaxed memory concurrency. - Sung-Hwan Lee 001; Minki Cho; Anton Podkopaev; Soham Chakraborty 001; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis (PLDI, 2020)

The Decidability of Verification under Promising 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Viktor Vafeiadis (CoRR, 2020)

Reconciling Event Structures with Modern Multiprocessors (Artifact). - Evgenii Moiseenko; Anton Podkopaev; Ori Lahav 001; Orestis Melkonian; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2020)

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2020)

Persistency semantics of the Intel-x86 architecture. - Azalea Raad; John Wickerson; Gil Neiger; Viktor Vafeiadis (Proc. ACM Program. Lang., 2020)

VSync: push-button verification and optimization for synchronization primitives on weak memory models. - Jonas Oberhauser; Rafael Lourenco de Lima Chehab; Diogo Behrens; Ming Fu; Antonio Paolillo; Lilith Oberhauser; Koustubha Bhat; Yuzhong Wen; Haibo Chen 001; Jaeho Kim; Viktor Vafeiadis (ASPLOS, 2021)

The Challenges of Weak Persistency (Invited Talk). - Viktor Vafeiadis (CALCO, 2021)

GenMC: A Model Checker for Weak Memory Models. - Michalis Kokologiannakis; Viktor Vafeiadis (CAV (1), 2021)

The Decidability of Verification under PS 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; S. Krishna 004; Viktor Vafeiadis (ESOP, 2021)

Dynamic Partial Order Reductions for Spinloops. - Michalis Kokologiannakis; Xiaowei Ren; Viktor Vafeiadis (FMCAD, 2021)

BAM: Efficient Model Checking for Barriers. - Michalis Kokologiannakis; Viktor Vafeiadis (NETYS, 2021)

Verifying and Optimizing the HMCS Lock for Arm Servers. - Jonas Oberhauser; Lilith Oberhauser; Antonio Paolillo; Diogo Behrens; Ming Fu; Viktor Vafeiadis (NETYS, 2021)

VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report). - Jonas Oberhauser; Rafael Lourenco de Lima Chehab; Diogo Behrens; Ming Fu; Antonio Paolillo; Lilith Oberhauser; Koustubha Bhat; Yuzhong Wen; Haibo Chen 001; Jaeho Kim; Viktor Vafeiadis (CoRR, 2021)

PerSeVerE: persistency semantics for verification under ext4. - Michalis Kokologiannakis; Ilya Kaysin; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2021)

Making weak memory models fair. - Ori Lahav 001; Egor Namakonov; Jonas Oberhauser; Anton Podkopaev; Viktor Vafeiadis (Proc. ACM Program. Lang., 2021)

SMT-Based Verification of Persistency Invariants of Px86 Programs. - Iason Marmanis; Viktor Vafeiadis (VSTTE, 2022)

Truly stateless, optimal dynamic partial order reduction. - Michalis Kokologiannakis; Iason Marmanis; Vladimir Gladstein; Viktor Vafeiadis (Proc. ACM Program. Lang., 2022)

Model checking for a multi-execution memory model. - Evgenii Moiseenko; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2022)

Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. - Azalea Raad; Luc Maranget; Viktor Vafeiadis (Proc. ACM Program. Lang., 2022)

AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM. - Martin Beck; Koustubha Bhat; Lazar Stricevic; Geng Chen; Diogo Behrens; Ming Fu; Viktor Vafeiadis; Haibo Chen 001; Hermann Härtig (ASPLOS (2), 2023)

Unblocking Dynamic Partial Order Reduction. - Michalis Kokologiannakis; Iason Marmanis; Viktor Vafeiadis (CAV (1), 2023)

Optimal Bounded Partial Order Reduction. - Iason Marmanis; Viktor Vafeiadis (FMCAD, 2023)

BWoS: Formally Verified Block-based Work Stealing for Parallel Processing. - Jiawei Wang; Bohdan Trach; Ming Fu; Diogo Behrens; Jonathan Schwender; Yutao Liu; Jitang Lei; Viktor Vafeiadis; Hermann Härtig; Haibo Chen 001 (OSDI, 2023)

Reconciling Preemption Bounding with DPOR. - Iason Marmanis; Michalis Kokologiannakis; Viktor Vafeiadis (TACAS (1), 2023)

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). - Ori Lahav 001; Azalea Raad; Joseph Tassarotti; Viktor Vafeiadis; Anton Podkopaev (Dagstuhl Reports, 2023)

The Path to Durable Linearizability. - Emanuele D'Osualdo; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2023)

Kater: Automating Weak Memory Model Metatheory and Consistency Checking. - Michalis Kokologiannakis; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2023)

Extending GenMC's Usability and Performance (Replication Package). - Michalis Kokologiannakis; Rupak Majumdar; Viktor Vafeiadis (Zenodo, 2023)

Automating Memory Model Metatheory with Intersections. - Aristotelis Koutsouridis; Michalis Kokologiannakis; Viktor Vafeiadis (CONCUR, 2024)

Specifying and Verifying Persistent Libraries. - Léo Stefanesco; Azalea Raad; Viktor Vafeiadis (ESOP (2), 2024)

Challenges in Empirically Testing Memory Persistency Models. - Vasileios Klimis; Alastair F. Donaldson; Viktor Vafeiadis; John Wickerson; Azalea Raad (NIER@ICSE, 2024)

Enhancing GenMC's Usability and Performance. - Michalis Kokologiannakis; Rupak Majumdar; Viktor Vafeiadis (TACAS (2), 2024)

Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour. - Vasileios Klimis; Alastair F. Donaldson; Viktor Vafeiadis; John Wickerson; Azalea Raad (CoRR, 2024)

Extending the C/C++ Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (CoRR, 2024)

SPORE: Combining Symmetry and Partial Order Reduction. - Michalis Kokologiannakis; Iason Marmanis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2024)

Extending the C/C++ Memory Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (Proc. ACM Program. Lang., 2024)

RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency. - Pavel Golovin; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2025)

Model Checking C/C++ with Mixed-Size Accesses. - Iason Marmanis; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2025)