Viktor Vafeiadis

120 papers A* 19A 18B 22C 1Misc 1Journal 42Unranked 14

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Verified High-Performance Composable Object Library for Remote Direct Memory Access. Proc. ACM Program. Lang. Guillaume Ambal, George Hodgkins, Mark Madler, Gregory V. Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis
2025	J	`jnl`	A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version). CoRR Guillaume Ambal, George Hodgkins, Mark Madler, Gregory V. Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis
2025	J	`jnl`	Model Checking C/C++ with Mixed-Size Accesses. Proc. ACM Program. Lang. Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis
2025	—	`ed.`	Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I ESOP (1) Viktor Vafeiadis
2025	—	`ed.`	Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part II ESOP (2) Viktor Vafeiadis
2025	J	`jnl`	RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency. Proc. ACM Program. Lang. Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis
2024	B	`conf`	Automating Memory Model Metatheory with Intersections. CONCUR Aristotelis Koutsouridis, Michalis Kokologiannakis, Viktor Vafeiadis
2024	—	`conf`	Challenges in Empirically Testing Memory Persistency Models. NIER@ICSE Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
2024	—	`conf`	Enhancing GenMC's Usability and Performance. TACAS (2) Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
2024	J	`jnl`	Extending the C/C++ Memory Model with Inline Assembly. Proc. ACM Program. Lang. Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
2024	J	`jnl`	Extending the C/C++ Model with Inline Assembly. CoRR Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
2024	J	`jnl`	Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour. CoRR Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
2024	J	`jnl`	SPORE: Combining Symmetry and Partial Order Reduction. Proc. ACM Program. Lang. Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
2024	—	`conf`	Specifying and Verifying Persistent Libraries. ESOP (2) Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
2023	—	`conf`	AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM. ASPLOS (2) Martin Beck, Koustubha Bhat, Lazar Stricevic, Geng Chen, Diogo Behrens, Ming Fu, Viktor Vafeiadis, Haibo Chen, Hermann Härtig
2023	A*	`conf`	BWoS: Formally Verified Block-based Work Stealing for Parallel Processing. OSDI Jiawei Wang, Bohdan Trach, Ming Fu, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig, Haibo Chen
2023	J	`jnl`	Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). Dagstuhl Reports Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev
2023	J	`jnl`	Kater: Automating Weak Memory Model Metatheory and Consistency Checking. Proc. ACM Program. Lang. Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
2023	B	`conf`	Optimal Bounded Partial Order Reduction. FMCAD Iason Marmanis, Viktor Vafeiadis
2023	—	`conf`	Reconciling Preemption Bounding with DPOR. TACAS (1) Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis
2023	J	`jnl`	Specifying and Verifying Persistent Libraries. CoRR Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
2023	J	`jnl`	The Path to Durable Linearizability. Proc. ACM Program. Lang. Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
2023	—	`conf`	Unblocking Dynamic Partial Order Reduction. CAV (1) Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
2022	J	`jnl`	Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. Proc. ACM Program. Lang. Azalea Raad, Luc Maranget, Viktor Vafeiadis
2022	J	`jnl`	Model checking for a multi-execution memory model. Proc. ACM Program. Lang. Evgenii Moiseenko, Michalis Kokologiannakis, Viktor Vafeiadis
2022	—	`conf`	SMT-Based Verification of Persistency Invariants of Px86 Programs. VSTTE Iason Marmanis, Viktor Vafeiadis
2022	J	`jnl`	The Path to Durable Linearizability. CoRR Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
2022	J	`jnl`	Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis
2021	—	`conf`	BAM: Efficient Model Checking for Barriers. NETYS Michalis Kokologiannakis, Viktor Vafeiadis
2021	B	`conf`	Dynamic Partial Order Reductions for Spinloops. FMCAD Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis
2021	—	`conf`	GenMC: A Model Checker for Weak Memory Models. CAV (1) Michalis Kokologiannakis, Viktor Vafeiadis
2021	J	`jnl`	Making weak memory models fair. Proc. ACM Program. Lang. Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
2021	J	`jnl`	PerSeVerE: persistency semantics for verification under ext4. Proc. ACM Program. Lang. Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
2021	B	`conf`	The Challenges of Weak Persistency (Invited Talk). CALCO Viktor Vafeiadis
2021	A	`conf`	The Decidability of Verification under PS 2.0. ESOP Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, Viktor Vafeiadis
2021	J	`jnl`	VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report). CoRR 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
2021	A*	`conf`	VSync: push-button verification and optimization for synchronization primitives on weak memory models. ASPLOS 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
2021	—	`conf`	Verifying and Optimizing the HMCS Lock for Arm Servers. NETYS Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis
2020	A*	`conf`	HMC: Model Checking for Hardware Memory Models. ASPLOS Michalis Kokologiannakis, Viktor Vafeiadis
2020	J	`jnl`	Making Weak Memory Models Fair. CoRR Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
2020	J	`jnl`	Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis
2020	J	`jnl`	Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. Azalea Raad, Ori Lahav, Viktor Vafeiadis
2020	A*	`conf`	Promising 2.0: global optimizations in relaxed memory concurrency. PLDI Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
2020	J	`jnl`	Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Ser. Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2020	A	`conf`	Reconciling Event Structures with Modern Multiprocessors. ECOOP Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2020	J	`jnl`	The Decidability of Verification under Promising 2.0. CoRR Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, Viktor Vafeiadis
2019	J	`jnl`	Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2019	J	`jnl`	Effective lock handling in stateless model checking. Proc. ACM Program. Lang. Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
2019	J	`jnl`	Grounding thin-air reads with event structures. Proc. ACM Program. Lang. Soham Chakraborty, Viktor Vafeiadis
2019	A*	`conf`	Model checking for weakly consistent libraries. PLDI Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
2019	J	`jnl`	On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis
2019	B	`conf`	On the Semantics of Snapshot Isolation. VMCAI Azalea Raad, Ori Lahav, Viktor Vafeiadis
2019	J	`jnl`	Reconciling Event Structures with Modern Multiprocessors. CoRR Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2019	J	`jnl`	Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang. Azalea Raad, John Wickerson, Viktor Vafeiadis
2018	A	`conf`	A Separation Logic for a Promising Semantics. ESOP Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
2018	J	`jnl`	Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. CoRR Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2018	J	`jnl`	Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
2018	J	`jnl`	GPS+: Reasoning About Fences and Relaxed Atomics. Int. J. Parallel Program. Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira
2018	A	`conf`	On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP Azalea Raad, Ori Lahav, Viktor Vafeiadis
2018	J	`jnl`	On the Semantics of Snapshot Isolation. CoRR Azalea Raad, Ori Lahav, Viktor Vafeiadis
2018	J	`jnl`	Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. Azalea Raad, Viktor Vafeiadis
2017	A*	`conf`	A promising semantics for relaxed-memory concurrency. POPL Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
2017	A	`conf`	Formalizing the concurrency semantics of an LLVM fragment. CGO Soham Chakraborty, Viktor Vafeiadis
2017	B	`ed.`	Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 CPP Yves Bertot, Viktor Vafeiadis
2017	—	`conf`	Program Verification Under Weak Memory Consistency Using Separation Logic. CAV (1) Viktor Vafeiadis
2017	A	`conf`	Promising Compilation to ARMv8 POP. ECOOP Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2017	A*	`conf`	Repairing sequential consistency in C/C++11. PLDI Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
2017	J	`jnl`	Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). Dagstuhl Artifacts Ser. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017	A	`conf`	Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017	A	`conf`	Tackling Real-Life Relaxed Concurrency with FSL++. ESOP Marko Doko, Viktor Vafeiadis
2016	B	`conf`	A Program Logic for C11 Memory Fences. VMCAI Marko Doko, Viktor Vafeiadis
2016	B	`conf`	Explaining Relaxed Memory Models with Program Transformations. FM Ori Lahav, Viktor Vafeiadis
2016	J	`jnl`	Geo-Replication: Fast If Possible, Consistent If Necessary. IEEE Data Eng. Bull. 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
2016	A*	`conf`	Lightweight verification of separate compilation. POPL Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2016	C	`conf`	Reasoning about Fences and Relaxed Atomics. PDP Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira
2016	A*	`conf`	Taming release-acquire consistency. POPL Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
2016	A	`conf`	Validating optimizations of concurrent C/C++ programs. CGO Soham Chakraborty, Viktor Vafeiadis
2015	A*	`conf`	A formal C memory model supporting integer-pointer casts. PLDI Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
2015	J	`jnl`	Aspect-oriented linearizability proofs. Log. Methods Comput. Sci. Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
2015	A	`conf`	Asynchronous Liquid Separation Types. ECOOP Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis
2015	A*	`conf`	Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. POPL Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli
2015	B	`conf`	Formal Reasoning about the C11 Weak Memory Model. CPP Viktor Vafeiadis
2015	A	`conf`	Modular Verification of Concurrency-Aware Linearizability. DISC Nir Hemed, Noam Rinetzky, Viktor Vafeiadis
2015	J	`jnl`	Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2015	—	`conf`	Owicki-Gries Reasoning for Weak Memory Models. ICALP (2) Ori Lahav, Viktor Vafeiadis
2015	A	`conf`	Pilsner: a compositionally verified compiler for a higher-order imperative language. ICFP Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
2015	B	`conf`	Proving Lock-Freedom Easily and Automatically. CPP Xiao Jia, Wei Li, Viktor Vafeiadis
2015	B	`conf`	Rely/Guarantee Reasoning for Asynchronous Programs. CONCUR Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis
2015	—	`conf`	Separation logic for weak memory models. PLMW@POPL Viktor Vafeiadis
2015	J	`jnl`	Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). Dagstuhl Reports Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis
2015	A*	`conf`	Verifying read-copy-update in a logic for weak memory. PLDI Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
2014	—	`conf`	Automating the Choice of Consistency Levels in Replicated Systems. USENIX ATC Cheng Li, João Leitão, Allen Clement, Nuno M. Preguiça, Rodrigo Rodrigues, Viktor Vafeiadis
2014	A	`conf`	GPS: navigating weak memory with ghosts, protocols, and separation. OOPSLA Aaron Turon, Viktor Vafeiadis, Derek Dreyer
2013	Misc	`conf`	A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism. TASE Mustafa Zengin, Viktor Vafeiadis
2013	B	`conf`	Adjustable References. ITP Viktor Vafeiadis
2013	B	`conf`	Aspect-Oriented Linearizability Proofs. CONCUR Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
2013	J	`jnl`	CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
2013	A	`conf`	Mtac: a monad for typed tactic programming in Coq. ICFP Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2013	A	`conf`	Relaxed separation logic: a program logic for C11 concurrency. OOPSLA Viktor Vafeiadis, Chinmay Narayan
2013	A*	`conf`	The power of parameterization in coinductive proof. POPL Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
2012	A*	`conf`	The marriage of bisimulations and Kripke logical relations. POPL Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
2011	B	`conf`	Concurrent Separation Logic and Operational Semantics. MFPS Viktor Vafeiadis
2011	A*	`conf`	Relaxed-memory concurrency and verified compilation. POPL Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
2011	A*	`conf`	Separation Logic in the Presence of Garbage Collection. LICS Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2011	B	`conf`	Verifying Fence Elimination Optimisations. SAS Viktor Vafeiadis, Francesco Zappa Nardelli
2010	A*	`conf`	Automatically Proving Linearizability. CAV Viktor Vafeiadis
2010	A	`conf`	Concurrent Abstract Predicates. ECOOP Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
2010	B	`conf`	RGSep Action Inference. VMCAI Viktor Vafeiadis
2010	A*	`conf`	Structuring the verification of heap-manipulating programs. POPL Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
2009	B	`conf`	Bi-abductive Resource Invariant Synthesis. APLAS Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis
2009	A	`conf`	Deny-Guarantee Reasoning. ESOP Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis
2009	B	`conf`	Finding heap-bounds for hardware synthesis. FMCAD Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
2009	A*	`conf`	Proving that non-blocking algorithms don't block. POPL Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
2009	B	`conf`	Shape-Value Abstraction for Verifying Linearizability. VMCAI Viktor Vafeiadis
2008	—	`—`	Modular fine-grained concurrency verification. Viktor Vafeiadis
2007	B	`conf`	A Marriage of Rely/Guarantee and Separation Logic. CONCUR Viktor Vafeiadis, Matthew J. Parkinson
2007	J	`jnl`	Acute: High-level programming language design for distributed computation. J. Funct. Program. Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis
2007	B	`conf`	Modular Safety Checking for Fine-Grained Concurrency. SAS Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis
2006	B	`conf`	Proving correctness of highly-concurrent linearisable objects. PPoPP Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro
2005	A	`conf`	Acute: high-level programming language design for distributed computation. ICFP Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis