Viktor Vafeiadis

ORCID

Publication Activity (10 Years)

Years Active: 2005-2024
Publications (10 Years): 82

Top Venues

Proc. ACM Program. Lang.

CoRR

PLDI

POPL

University of Cambridge, UK (PHD)

Education History

University of Cambridge, UK

PHD

Publications

Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
Challenges in Empirically Testing Memory Persistency Models. NIER@ICSE (2024)
Aristotelis Koutsouridis, Michalis Kokologiannakis, Viktor Vafeiadis
Automating Memory Model Metatheory with Intersections. CONCUR (2024)
Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
Enhancing GenMC's Usability and Performance. TACAS (2) (2024)
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
SPORE: Combining Symmetry and Partial Order Reduction. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
Specifying and Verifying Persistent Libraries. ESOP (2) (2024)
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour. CoRR (2024)
Jiawei Wang, Bohdan Trach, Ming Fu, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig, Haibo Chen
BWoS: Formally Verified Block-based Work Stealing for Parallel Processing. OSDI (2023)
Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
Specifying and Verifying Persistent Libraries. CoRR (2023)
Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. Proc. ACM Program. Lang. 7 (POPL) (2023)
Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). Dagstuhl Reports 13 (10) (2023)
Martin Beck, Koustubha Bhat, Lazar Stricevic, Geng Chen, Diogo Behrens, Ming Fu, Viktor Vafeiadis, Haibo Chen, Hermann Härtig
AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM. ASPLOS (2) (2023)
Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis
Reconciling Preemption Bounding with DPOR. TACAS (1) (2023)
Iason Marmanis, Viktor Vafeiadis
Optimal Bounded Partial Order Reduction. FMCAD (2023)
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
Unblocking Dynamic Partial Order Reduction. CAV (1) (2023)
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
The Path to Durable Linearizability. Proc. ACM Program. Lang. 7 (POPL) (2023)
Evgenii Moiseenko, Michalis Kokologiannakis, Viktor Vafeiadis
Model checking for a multi-execution memory model. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Iason Marmanis, Viktor Vafeiadis
SMT-Based Verification of Persistency Invariants of Px86 Programs. VSTTE (2022)
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis
Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6 (POPL) (2022)
Azalea Raad, Luc Maranget, Viktor Vafeiadis
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. Proc. ACM Program. Lang. 6 (POPL) (2022)
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
The Path to Durable Linearizability. CoRR (2022)
Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis
Dynamic Partial Order Reductions for Spinloops. FMCAD (2021)
Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis
Verifying and Optimizing the HMCS Lock for Arm Servers. NETYS (2021)
Michalis Kokologiannakis, Viktor Vafeiadis
GenMC: A Model Checker for Weak Memory Models. CAV (1) (2021)
Viktor Vafeiadis
The Challenges of Weak Persistency (Invited Talk). CALCO (2021)
Michalis Kokologiannakis, Viktor Vafeiadis
BAM: Efficient Model Checking for Barriers. NETYS (2021)
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
Making weak memory models fair. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis
VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report). CoRR (2021)
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
PerSeVerE: persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5 (POPL) (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Viktor Vafeiadis
The Decidability of Verification under PS 2.0. ESOP (2021)
Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis
VSync: push-button verification and optimization for synchronization primitives on weak memory models. ASPLOS (2021)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors. ECOOP (2020)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Ser. 6 (2) (2020)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Michalis Kokologiannakis, Viktor Vafeiadis
HMC: Model Checking for Hardware Memory Models. ASPLOS (2020)
Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis
Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. 4 (POPL) (2020)
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
Making Weak Memory Models Fair. CoRR (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Viktor Vafeiadis
The Decidability of Verification under Promising 2.0. CoRR (2020)
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
Promising 2.0: global optimizations in relaxed memory concurrency. PLDI (2020)
Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3 (POPL) (2019)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors. CoRR (2019)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On the Semantics of Snapshot Isolation. VMCAI (2019)
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
Effective lock handling in stateless model checking. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
Model checking for weakly consistent libraries. PLDI (2019)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3 (POPL) (2019)
Azalea Raad, John Wickerson, Viktor Vafeiadis
Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Soham Chakraborty, Viktor Vafeiadis
Grounding thin-air reads with event structures. Proc. ACM Program. Lang. 3 (POPL) (2019)
Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira
GPS $$+$$ + : Reasoning About Fences and Relaxed Atomics. Int. J. Parallel Program. 46 (6) (2018)
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
A Separation Logic for a Promising Semantics. ESOP (2018)
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2 (POPL) (2018)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. CoRR (2018)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On the Semantics of Snapshot Isolation. CoRR (2018)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP (2018)
Azalea Raad, Viktor Vafeiadis
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Soham Chakraborty, Viktor Vafeiadis
Formalizing the concurrency semantics of an LLVM fragment. CGO (2017)
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
A promising semantics for relaxed-memory concurrency. POPL (2017)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Promising Compilation to ARMv8 POP. ECOOP (2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP (2017)
Viktor Vafeiadis
Program Verification Under Weak Memory Consistency Using Separation Logic. CAV (1) (2017)
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
Repairing sequential consistency in C/C++11. PLDI (2017)
Marko Doko, Viktor Vafeiadis
Tackling Real-Life Relaxed Concurrency with FSL++. ESOP (2017)
Soham Chakraborty, Viktor Vafeiadis
Validating optimizations of concurrent C/C++ programs. CGO (2016)
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
Lightweight verification of separate compilation. POPL (2016)
Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira
Reasoning about Fences and Relaxed Atomics. PDP (2016)
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
Taming release-acquire consistency. POPL (2016)
Marko Doko, Viktor Vafeiadis
A Program Logic for C11 Memory Fences. VMCAI (2016)
Ori Lahav, Viktor Vafeiadis
Explaining Relaxed Memory Models with Program Transformations. FM (2016)
Valter Balegas, Cheng Li, Mahsa Najafzadeh, Daniel Porto, Allen Clement, Sérgio Duarte, Carla Ferreira, Johannes Gehrke, João Leitão, Nuno M. Preguiça, Rodrigo Rodrigues, Marc Shapiro, Viktor Vafeiadis
Geo-Replication: Fast If Possible, Consistent If Necessary. IEEE Data Eng. Bull. 39 (1) (2016)
Viktor Vafeiadis
Separation logic for weak memory models. PLMW@POPL (2015)
Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
Aspect-oriented linearizability proofs. Log. Methods Comput. Sci. 11 (1) (2015)
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
A formal C memory model supporting integer-pointer casts. PLDI (2015)
Nir Hemed, Noam Rinetzky, Viktor Vafeiadis
Modular Verification of Concurrency-Aware Linearizability. DISC (2015)
Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis
Asynchronous Liquid Separation Types. ECOOP (2015)
Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis
Rely/Guarantee Reasoning for Asynchronous Programs. CONCUR (2015)
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015)
Xiao Jia, Wei Li, Viktor Vafeiadis
Proving Lock-Freedom Easily and Automatically. CPP (2015)
Ori Lahav, Viktor Vafeiadis
Owicki-Gries Reasoning for Weak Memory Models. ICALP (2) (2015)
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
Pilsner: a compositionally verified compiler for a higher-order imperative language. ICFP (2015)
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
Verifying read-copy-update in a logic for weak memory. PLDI (2015)
Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). Dagstuhl Reports 5 (11) (2015)
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. POPL (2015)
Viktor Vafeiadis
Formal Reasoning about the C11 Weak Memory Model. CPP (2015)
Aaron Turon, Viktor Vafeiadis, Derek Dreyer
GPS: navigating weak memory with ghosts, protocols, and separation. OOPSLA (2014)
Cheng Li, João Leitão, Allen Clement, Nuno M. Preguiça, Rodrigo Rodrigues, Viktor Vafeiadis
Automating the Choice of Consistency Levels in Replicated Systems. USENIX Annual Technical Conference (2014)
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60 (3) (2013)
Viktor Vafeiadis
Adjustable References. ITP (2013)
Mustafa Zengin, Viktor Vafeiadis
A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism. TASE (2013)
Viktor Vafeiadis, Chinmay Narayan
Relaxed separation logic: a program logic for C11 concurrency. OOPSLA (2013)
Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
Aspect-Oriented Linearizability Proofs. CONCUR (2013)
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
Mtac: a monad for typed tactic programming in Coq. ICFP (2013)
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
The power of parameterization in coinductive proof. POPL (2013)
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
The marriage of bisimulations and Kripke logical relations. POPL (2012)
Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
Separation Logic in the Presence of Garbage Collection. LICS (2011)
Viktor Vafeiadis
Concurrent Separation Logic and Operational Semantics. MFPS (2011)
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
Relaxed-memory concurrency and verified compilation. POPL (2011)
Viktor Vafeiadis, Francesco Zappa Nardelli
Verifying Fence Elimination Optimisations. SAS (2011)
Viktor Vafeiadis
Automatically Proving Linearizability. CAV (2010)
Viktor Vafeiadis
RGSep Action Inference. VMCAI (2010)
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
Structuring the verification of heap-manipulating programs. POPL (2010)
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
Concurrent Abstract Predicates. ECOOP (2010)

Viktor Vafeiadis.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Viktor Vafeiadis