default search action
Viktor Vafeiadis
Person information
- affiliation: Max Planck Institute for Software Systems
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j26]Paulo Emílio de Vilhena
, Ori Lahav
Extending the C/C++ Memory Model with Inline Assembly. Proc. ACM Program. Lang. 8(OOPSLA2): 1081-1107 (2024) - [j25]Michalis Kokologiannakis
SPORE: Combining Symmetry and Partial Order Reduction. Proc. ACM Program. Lang. 8(PLDI): 1781-1803 (2024) - [c73]Aristotelis Koutsouridis, Michalis Kokologiannakis, Viktor Vafeiadis:
Automating Memory Model Metatheory with Intersections. CONCUR 2024: 33:1-33:16 - [c72]Léo Stefanesco, Azalea Raad, Viktor Vafeiadis:
Specifying and Verifying Persistent Libraries. ESOP (2) 2024: 185-211 - [c71]Vasileios Klimis
Challenges in Empirically Testing Memory Persistency Models. NIER@ICSE 2024: 82-86 - [c70]Michalis Kokologiannakis
Enhancing GenMC's Usability and Performance. TACAS (2) 2024: 66-84 - [i13]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 abs/2405.18575 (2024) - [i12]Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad:
Extending the C/C++ Model with Inline Assembly. CoRR abs/2408.17208 (2024) - 2023
- [j24]Michalis Kokologiannakis
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. Proc. ACM Program. Lang. 7(POPL): 544-572 (2023) - [j23]Emanuele D'Osualdo
The Path to Durable Linearizability. Proc. ACM Program. Lang. 7(POPL): 748-774 (2023) - [c69]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: 61-73 - [c68]Michalis Kokologiannakis
Unblocking Dynamic Partial Order Reduction. CAV (1) 2023: 230-250 - [c67]Iason Marmanis, Viktor Vafeiadis:
Optimal Bounded Partial Order Reduction. FMCAD 2023: 86-91 - [c66]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: 833-850 - [c65]Iason Marmanis
Reconciling Preemption Bounding with DPOR. TACAS (1) 2023: 85-104 - [d1]Michalis Kokologiannakis
Extending GenMC's Usability and Performance (Replication Package). Zenodo, 2023 - [i11]Léo Stefanesco, Azalea Raad, Viktor Vafeiadis:
Specifying and Verifying Persistent Libraries. CoRR abs/2306.01614 (2023) - [i10]Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev:
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). Dagstuhl Reports 13(10): 50-64 (2023) - 2022
- [j22]Evgenii Moiseenko
Model checking for a multi-execution memory model. Proc. ACM Program. Lang. 6(OOPSLA2): 758-785 (2022) - [j21]Michalis Kokologiannakis
Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL): 1-28 (2022) - [j20]Azalea Raad
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [c64]Iason Marmanis
SMT-Based Verification of Persistency Invariants of Px86 Programs. VSTTE 2022: 92-110 - [i9]Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis:
The Path to Durable Linearizability. CoRR abs/2211.07631 (2022) - 2021
- [j19]Ori Lahav
Making weak memory models fair. Proc. ACM Program. Lang. 5(OOPSLA): 1-27 (2021) - [j18]Michalis Kokologiannakis
PerSeVerE: persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) - [c63]Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo
VSync: push-button verification and optimization for synchronization primitives on weak memory models. ASPLOS 2021: 530-545 - [c62]Viktor Vafeiadis
The Challenges of Weak Persistency (Invited Talk). CALCO 2021: 4:1-4:3 - [c61]Michalis Kokologiannakis
GenMC: A Model Checker for Weak Memory Models. CAV (1) 2021: 427-440 - [c60]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, Viktor Vafeiadis
The Decidability of Verification under PS 2.0. ESOP 2021: 1-29 - [c59]Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis
Dynamic Partial Order Reductions for Spinloops. FMCAD 2021: 163-172 - [c58]Michalis Kokologiannakis
BAM: Efficient Model Checking for Barriers. NETYS 2021: 223-239 - [c57]Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis
Verifying and Optimizing the HMCS Lock for Arm Servers. NETYS 2021: 240-260 - [i8]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 abs/2102.06590 (2021) - 2020
- [j17]Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis:
Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Ser. 6(2): 04:1-04:3 (2020) - [j16]Azalea Raad, Ori Lahav
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4(OOPSLA): 151:1-151:28 (2020) - [j15]Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis
Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL): 11:1-11:31 (2020) - [c56]Michalis Kokologiannakis, Viktor Vafeiadis
HMC: Model Checking for Hardware Memory Models. ASPLOS 2020: 1157-1171 - [c55]Evgenii Moiseenko
Reconciling Event Structures with Modern Multiprocessors. ECOOP 2020: 5:1-5:26 - [c54]Sung-Hwan Lee
Promising 2.0: global optimizations in relaxed memory concurrency. PLDI 2020: 362-376 - [i7]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, Viktor Vafeiadis:
The Decidability of Verification under Promising 2.0. CoRR abs/2007.09944 (2020) - [i6]Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis:
Making Weak Memory Models Fair. CoRR abs/2012.01067 (2020)
2010 – 2019
- 2019
- [j14]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): 135:1-135:27 (2019) - [j13]Michalis Kokologiannakis
Effective lock handling in stateless model checking. Proc. ACM Program. Lang. 3(OOPSLA): 173:1-173:26 (2019) - [j12]Azalea Raad, Marko Doko
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3(POPL): 68:1-68:31 (2019) - [j11]Anton Podkopaev, Ori Lahav
Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3(POPL): 69:1-69:31 (2019) - [j10]Soham Chakraborty, Viktor Vafeiadis
Grounding thin-air reads with event structures. Proc. ACM Program. Lang. 3(POPL): 70:1-70:28 (2019) - [c53]Michalis Kokologiannakis
Model checking for weakly consistent libraries. PLDI 2019: 96-110 - [c52]Azalea Raad, Ori Lahav
On the Semantics of Snapshot Isolation. VMCAI 2019: 1-23 - [i5]Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis:
Reconciling Event Structures with Modern Multiprocessors. CoRR abs/1911.06567 (2019) - 2018
- [j9]Mengda He, Viktor Vafeiadis
GPS+: Reasoning About Fences and Relaxed Atomics. Int. J. Parallel Program. 46(6): 1157-1183 (2018) - [j8]Azalea Raad, Viktor Vafeiadis
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. 2(OOPSLA): 137:1-137:27 (2018) - [j7]Michalis Kokologiannakis
Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2(POPL): 17:1-17:32 (2018) - [c51]Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko
A Separation Logic for a Promising Semantics. ESOP 2018: 357-384 - [c50]Azalea Raad, Ori Lahav
On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP 2018: 940-967 - [i4]Azalea Raad, Ori Lahav, Viktor Vafeiadis:
On the Semantics of Snapshot Isolation. CoRR abs/1805.06196 (2018) - [i3]Anton Podkopaev, Ori Lahav, Viktor Vafeiadis:
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. CoRR abs/1807.07892 (2018) - 2017
- [j6]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): 15:1-15:2 (2017) - [c49]Viktor Vafeiadis
Program Verification Under Weak Memory Consistency Using Separation Logic. CAV (1) 2017: 30-46 - [c48]Soham Chakraborty, Viktor Vafeiadis:
Formalizing the concurrency semantics of an LLVM fragment. CGO 2017: 100-110 - [c47]Jan-Oliver Kaiser, Hoang-Hai Dang
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP 2017: 17:1-17:29 - [c46]Anton Podkopaev
Promising Compilation to ARMv8 POP. ECOOP 2017: 22:1-22:28 - [c45]Marko Doko
Tackling Real-Life Relaxed Concurrency with FSL++. ESOP 2017: 448-475 - [c44]Ori Lahav
Repairing sequential consistency in C/C++11. PLDI 2017: 618-632 - [c43]Jeehoon Kang
A promising semantics for relaxed-memory concurrency. POPL 2017: 175-189 - [e1]Yves Bertot, Viktor Vafeiadis:
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. ACM 2017, ISBN 978-1-4503-4705-1 [contents] - 2016
- [j5]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
Geo-Replication: Fast If Possible, Consistent If Necessary. IEEE Data Eng. Bull. 39(1): 81-92 (2016) - [c42]Soham Chakraborty, Viktor Vafeiadis
Validating optimizations of concurrent C/C++ programs. CGO 2016: 216-226 - [c41]Ori Lahav
Explaining Relaxed Memory Models with Program Transformations. FM 2016: 479-495 - [c40]Mengda He, Viktor Vafeiadis
Reasoning about Fences and Relaxed Atomics. PDP 2016: 520-527 - [c39]Jeehoon Kang
Lightweight verification of separate compilation. POPL 2016: 178-190 - [c38]Ori Lahav
Taming release-acquire consistency. POPL 2016: 649-662 - [c37]Marko Doko
A Program Logic for C11 Memory Fences. VMCAI 2016: 413-430 - 2015
- [j4]Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
Aspect-oriented linearizability proofs. Log. Methods Comput. Sci. 11(1) (2015) - [j3]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) - [c36]Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis
Rely/Guarantee Reasoning for Asynchronous Programs. CONCUR 2015: 483-496 - [c35]Viktor Vafeiadis
Formal Reasoning about the C11 Weak Memory Model. CPP 2015: 1-2 - [c34]Xiao Jia, Wei Li, Viktor Vafeiadis
Proving Lock-Freedom Easily and Automatically. CPP 2015: 119-127 - [c33]Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis
Asynchronous Liquid Separation Types. ECOOP 2015: 396-420 - [c32]Ori Lahav
Owicki-Gries Reasoning for Weak Memory Models. ICALP (2) 2015: 311-323 - [c31]Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin
Pilsner: a compositionally verified compiler for a higher-order imperative language. ICFP 2015: 166-178 - [c30]Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
Verifying read-copy-update in a logic for weak memory. PLDI 2015: 110-120 - [c29]Jeehoon Kang
A formal C memory model supporting integer-pointer casts. PLDI 2015: 326-335 - [c28]Viktor Vafeiadis
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. POPL 2015: 209-220 - [c27]Nir Hemed, Noam Rinetzky, Viktor Vafeiadis
Modular Verification of Concurrency-Aware Linearizability. DISC 2015: 371-387 - [i2]Viktor Vafeiadis:
Separation logic for weak memory models. PLMW@POPL 2015: 11:1 - [i1]Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis:
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). Dagstuhl Reports 5(11): 1-28 (2015) - 2014
- [c26]Aaron Turon, Viktor Vafeiadis
GPS: navigating weak memory with ghosts, protocols, and separation. OOPSLA 2014: 691-707 - [c25]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 ATC 2014: 281-292 - 2013
- [j2]Jaroslav Sevcík, Viktor Vafeiadis
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3): 22:1-22:50 (2013) - [c24]Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
Aspect-Oriented Linearizability Proofs. CONCUR 2013: 242-256 - [c23]Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
Mtac: a monad for typed tactic programming in Coq. ICFP 2013: 87-100 - [c22]Viktor Vafeiadis
Adjustable References. ITP 2013: 328-337 - [c21]Viktor Vafeiadis
Relaxed separation logic: a program logic for C11 concurrency. OOPSLA 2013: 867-884 - [c20]Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
The power of parameterization in coinductive proof. POPL 2013: 193-206 - [c19]Mustafa Zengin, Viktor Vafeiadis
A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism. TASE 2013: 105-112 - 2012
- [c18]Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
The marriage of bisimulations and Kripke logical relations. POPL 2012: 59-72 - 2011
- [c17]Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
Separation Logic in the Presence of Garbage Collection. LICS 2011: 247-256 - [c16]Jaroslav Sevcík, Viktor Vafeiadis
Relaxed-memory concurrency and verified compilation. POPL 2011: 43-54 - [c15]Viktor Vafeiadis
Verifying Fence Elimination Optimisations. SAS 2011: 146-162 - [c14]Viktor Vafeiadis
Concurrent Separation Logic and Operational Semantics. MFPS 2011: 335-351 - 2010
- [c13]Viktor Vafeiadis
Automatically Proving Linearizability. CAV 2010: 450-464 - [c12]Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
Concurrent Abstract Predicates. ECOOP 2010: 504-528 - [c11]Aleksandar Nanevski, Viktor Vafeiadis
Structuring the verification of heap-manipulating programs. POPL 2010: 261-274 - [c10]Viktor Vafeiadis
RGSep Action Inference. VMCAI 2010: 345-361
2000 – 2009
- 2009
- [c9]Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis
Bi-abductive Resource Invariant Synthesis. APLAS 2009: 259-274 - [c8]Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis
Deny-Guarantee Reasoning. ESOP 2009: 363-377 - [c7]Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
Finding heap-bounds for hardware synthesis. FMCAD 2009: 205-212 - [c6]Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
Proving that non-blocking algorithms don't block. POPL 2009: 16-28 - [c5]Viktor Vafeiadis
Shape-Value Abstraction for Verifying Linearizability. VMCAI 2009: 335-348 - 2008
- [b1]Viktor Vafeiadis:
Modular fine-grained concurrency verification. University of Cambridge, UK, 2008 - 2007
- [j1]Peter Sewell
Acute: High-level programming language design for distributed computation. J. Funct. Program. 17(4-5): 547-612 (2007) - [c4]Viktor Vafeiadis, Matthew J. Parkinson:
A Marriage of Rely/Guarantee and Separation Logic. CONCUR 2007: 256-271 - [c3]Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis:
Modular Safety Checking for Fine-Grained Concurrency. SAS 2007: 233-248 - 2006
- [c2]Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro
Proving correctness of highly-concurrent linearisable objects. PPoPP 2006: 129-136 - 2005
- [c1]Peter Sewell
Acute: high-level programming language design for distributed computation. ICFP 2005: 15-26
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-02 22:35 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: