Viktor Vafeiadis
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
69
Venues
27
Active years
2005–2024
Best venue rank
A*
Where they publish
- A*POPL10 papers
- AESOP6 papers
- AECOOP5 papers
- A*PLDI5 papers
- BCONCUR4 papers
- A*CAV4 papers
- BVMCAI4 papers
- A*ASPLOS3 papers
- BFMCAD3 papers
- AICFP3 papers
- ATACAS2 papers
- ACGO2 papers
- BCPP2 papers
- AOOPSLA2 papers
- BSAS2 papers
- A*ICSE1 paper
- A*OSDI1 paper
- BCALCO1 paper
- BFM1 paper
- CPDP1 paper
- A*ICALP1 paper
- AUSENIX1 paper
- BITP1 paper
- NationalTASE1 paper
- A*LICS1 paper
- BAPLAS1 paper
- BPPoPP1 paper
Papers
69 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2024 | CONCUR | Automating Memory Model Metatheory with Intersections. | Aristotelis Koutsouridis, Michalis Kokologiannakis, Viktor Vafeiadis |
| 2024 | ESOP | Specifying and Verifying Persistent Libraries. | Lo Stefanesco, Azalea Raad, Viktor Vafeiadis |
| 2024 | ICSE | Challenges in Empirically Testing Memory Persistency Models. | Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad |
| 2024 | TACAS | Enhancing GenMC's Usability and Performance. | Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis |
| 2023 | ASPLOS | 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, Hermann Hrtig |
| 2023 | CAV | Unblocking Dynamic Partial Order Reduction. | Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis |
| 2023 | FMCAD | Optimal Bounded Partial Order Reduction. | Iason Marmanis, Viktor Vafeiadis |
| 2023 | OSDI | 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 Hrtig, Haibo Chen |
| 2023 | TACAS | Reconciling Preemption Bounding with DPOR. | Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis |
| 2021 | ASPLOS | 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, Jaeho Kim, Viktor Vafeiadis |
| 2021 | CALCO | The Challenges of Weak Persistency (Invited Talk). | Viktor Vafeiadis |
| 2021 | CAV | GenMC: A Model Checker for Weak Memory Models. | Michalis Kokologiannakis, Viktor Vafeiadis |
| 2021 | ESOP | The Decidability of Verification under PS 2.0. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, Viktor Vafeiadis |
| 2021 | FMCAD | Dynamic Partial Order Reductions for Spinloops. | Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis |
| 2020 | ASPLOS | HMC: Model Checking for Hardware Memory Models. | Michalis Kokologiannakis, Viktor Vafeiadis |
| 2020 | ECOOP | Reconciling Event Structures with Modern Multiprocessors. | Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis |
| 2020 | PLDI | Promising 2.0: global optimizations in relaxed memory concurrency. | Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis |
| 2019 | PLDI | Model checking for weakly consistent libraries. | Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis |
| 2019 | VMCAI | On the Semantics of Snapshot Isolation. | Azalea Raad, Ori Lahav, Viktor Vafeiadis |
| 2018 | ESOP | On Parallel Snapshot Isolation and Release/Acquire Consistency. | Azalea Raad, Ori Lahav, Viktor Vafeiadis |
| 2018 | ESOP | A Separation Logic for a Promising Semantics. | Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis |
| 2017 | CAV | Program Verification Under Weak Memory Consistency Using Separation Logic. | Viktor Vafeiadis |
| 2017 | CGO | Formalizing the concurrency semantics of an LLVM fragment. | Soham Chakraborty, Viktor Vafeiadis |
| 2017 | ECOOP | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. | Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis |
| 2017 | ECOOP | Promising Compilation to ARMv8 POP. | Anton Podkopaev, Ori Lahav, Viktor Vafeiadis |
| 2017 | ESOP | Tackling Real-Life Relaxed Concurrency with FSL++. | Marko Doko, Viktor Vafeiadis |
| 2017 | PLDI | Repairing sequential consistency in C/C++11. | Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer |
| 2017 | POPL | A promising semantics for relaxed-memory concurrency. | Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
| 2016 | CGO | Validating optimizations of concurrent C/C++ programs. | Soham Chakraborty, Viktor Vafeiadis |
| 2016 | FM | Explaining Relaxed Memory Models with Program Transformations. | Ori Lahav, Viktor Vafeiadis |
| 2016 | PDP | Reasoning about Fences and Relaxed Atomics. | Mengda He, Viktor Vafeiadis, Shengchao Qin, Joo F. Ferreira |
| 2016 | POPL | Lightweight verification of separate compilation. | Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
| 2016 | POPL | Taming release-acquire consistency. | Ori Lahav, Nick Giannarakis, Viktor Vafeiadis |
| 2016 | VMCAI | A Program Logic for C11 Memory Fences. | Marko Doko, Viktor Vafeiadis |
| 2015 | CONCUR | Rely/Guarantee Reasoning for Asynchronous Programs. | Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis |
| 2015 | CPP | Proving Lock-Freedom Easily and Automatically. | Xiao Jia, Wei Li, Viktor Vafeiadis |
| 2015 | CPP | Formal Reasoning about the C11 Weak Memory Model. | Viktor Vafeiadis |
| 2015 | ECOOP | Asynchronous Liquid Separation Types. | Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis |
| 2015 | ICALP | Owicki-Gries Reasoning for Weak Memory Models. | Ori Lahav, Viktor Vafeiadis |
| 2015 | ICFP | 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 |
| 2015 | PLDI | A formal C memory model supporting integer-pointer casts. | Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis |
| 2015 | PLDI | Verifying read-copy-update in a logic for weak memory. | Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis |
| 2015 | POPL | Separation logic for weak memory models. | Viktor Vafeiadis |
| 2015 | POPL | Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. | Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli |
| 2014 | OOPSLA | GPS: navigating weak memory with ghosts, protocols, and separation. | Aaron Turon, Viktor Vafeiadis, Derek Dreyer |
| 2014 | USENIX | Automating the Choice of Consistency Levels in Replicated Systems. | Cheng Li, Joo Leito, Allen Clement, Nuno M. Preguia, Rodrigo Rodrigues, Viktor Vafeiadis |
| 2013 | CONCUR | Aspect-Oriented Linearizability Proofs. | Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis |
| 2013 | ICFP | Mtac: a monad for typed tactic programming in Coq. | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | ITP | Adjustable References. | Viktor Vafeiadis |
| 2013 | OOPSLA | Relaxed separation logic: a program logic for C11 concurrency. | Viktor Vafeiadis, Chinmay Narayan |
| 2013 | POPL | The power of parameterization in coinductive proof. | Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis |
| 2013 | TASE | A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism. | Mustafa Zengin, Viktor Vafeiadis |
| 2012 | POPL | The marriage of bisimulations and Kripke logical relations. | Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis |
| 2011 | LICS | Separation Logic in the Presence of Garbage Collection. | Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
| 2011 | POPL | Relaxed-memory concurrency and verified compilation. | Jaroslav Sevck, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell |
| 2011 | SAS | Verifying Fence Elimination Optimisations. | Viktor Vafeiadis, Francesco Zappa Nardelli |
| 2010 | CAV | Automatically Proving Linearizability. | Viktor Vafeiadis |
| 2010 | ECOOP | Concurrent Abstract Predicates. | Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis |
| 2010 | POPL | Structuring the verification of heap-manipulating programs. | Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine |
| 2010 | VMCAI | RGSep Action Inference. | Viktor Vafeiadis |
| 2009 | APLAS | Bi-abductive Resource Invariant Synthesis. | Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis |
| 2009 | ESOP | Deny-Guarantee Reasoning. | Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | FMCAD | Finding heap-bounds for hardware synthesis. | Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jir Simsa, Satnam Singh, Viktor Vafeiadis |
| 2009 | POPL | Proving that non-blocking algorithms don't block. | Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | VMCAI | Shape-Value Abstraction for Verifying Linearizability. | Viktor Vafeiadis |
| 2007 | CONCUR | A Marriage of Rely/Guarantee and Separation Logic. | Viktor Vafeiadis, Matthew J. Parkinson |
| 2007 | SAS | Modular Safety Checking for Fine-Grained Concurrency. | Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis |
| 2006 | PPoPP | Proving correctness of highly-concurrent linearisable objects. | Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro |
| 2005 | ICFP | 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 |