BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Czech Republic
1 × Denmark
1 × Estonia
1 × India
1 × Japan
1 × Slovenia
2 × Canada
2 × Italy
2 × Spain
2 × United Kingdom
9 × USA
Collaborated with:
O.Lahav D.Dreyer A.Raad C.Hur Michalis Kokologiannakis F.Z.Nardelli M.J.Parkinson M.Doko J.Kang S.Chakraborty G.Neis Anton Podkopaev J.Wickerson A.Nanevski C.Narayan M.Dodds J.Kaiser P.Sewell J.Kloos R.Majumdar J.Tassarotti A.Turon J.Berdine C.Calcagno N.Giannarakis X.Feng A.Gotsman B.Cook M.Herlihy C.A.R.Hoare M.Shapiro Konstantinos Sagonas Gil Neiger T.Balabonski R.Morisset B.Ziliani N.R.Krishnaswami J.Sevcík S.Jagannathan T.Dinsdale-Young P.Gardner K.Svendsen J.Pichon-Pharabod Hoang-Hai Dang Yoonseung Kim Lovro Rozic C.McLaughlin W.Mansky D.Garbuzov S.Zdancewic J.J.Leifer K.Wansbrough M.Allen-Williams P.Habouzit
Talks about:
memori (14) model (12) weak (10) concurr (9) consist (8) logic (8) separ (7) program (6) verifi (6) semant (6)

Person: Viktor Vafeiadis

DBLP DBLP: Vafeiadis:Viktor

Contributed to:

ECOOP 20152015
ICALP (2) 20152015
ICFP 20152015
PLDI 20152015
POPL 20152015
OOPSLA 20142014
ICFP 20132013
OOPSLA 20132013
POPL 20132013
POPL 20122012
LICS 20112011
POPL 20112011
SAS 20112011
CAV 20102010
ECOOP 20102010
POPL 20102010
VMCAI 20102010
ESOP 20092009
POPL 20092009
VMCAI 20092009
SAS 20072007
PPoPP 20062006
ICFP 20052005
ESOP 20172017
ESOP 20182018
CAV (1) 20172017
ECOOP 20172017
OOPSLA 20182018
OOPSLA 20192019
POPL 20162016
PLDI 20172017
POPL 20172017
POPL 20182018
PLDI 20192019
POPL 20192019
POPL 20202020
ASPLOS 20202020

Wrote 44 papers:

ECOOP-2015-KloosMV
Asynchronous Liquid Separation Types (JK, RM, VV), pp. 396–420.
ICALP-v2-2015-LahavV #memory management #modelling #reasoning
Owicki-Gries Reasoning for Weak Memory Models (OL, VV), pp. 311–323.
ICFP-2015-NeisHKMDV #compilation #higher-order #imperative #named
Pilsner: a compositionally verified compiler for a higher-order imperative language (GN, CKH, JOK, CM, DD, VV), pp. 166–178.
PLDI-2015-KangHMGZV #c #memory management
A formal C memory model supporting integer-pointer casts (JK, CKH, WM, DG, SZ, VV), pp. 326–335.
PLDI-2015-TassarottiDV #logic #memory management #verification
Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.
POPL-2015-VafeiadisBCMN #compilation #memory management #optimisation #what
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it (VV, TB, SC, RM, FZN), pp. 209–220.
OOPSLA-2014-TuronVD #memory management #named #navigation #protocol
GPS: navigating weak memory with ghosts, protocols, and separation (AT, VV, DD), pp. 691–707.
ICFP-2013-ZilianiDKNV #coq #monad #named #programming
Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.
OOPSLA-2013-VafeiadisN #concurrent #logic
Relaxed separation logic: a program logic for C11 concurrency (VV, CN), pp. 867–884.
POPL-2013-HurNDV #induction #power of #proving
The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
POPL-2012-HurDNV #bisimulation #logic
The marriage of bisimulations and Kripke logical relations (CKH, DD, GN, VV), pp. 59–72.
LICS-2011-HurDV #garbage collection #logic
Separation Logic in the Presence of Garbage Collection (CKH, DD, VV), pp. 247–256.
POPL-2011-SevcikVNJS #compilation #concurrent
Relaxed-memory concurrency and verified compilation (JS, VV, FZN, SJ, PS), pp. 43–54.
SAS-2011-VafeiadisN #optimisation #verification
Verifying Fence Elimination Optimisations (VV, FZN), pp. 146–162.
CAV-2010-Vafeiadis #automation #proving
Automatically Proving Linearizability (VV), pp. 450–464.
ECOOP-2010-Dinsdale-YoungDGPV #concurrent
Concurrent Abstract Predicates (TDY, MD, PG, MJP, VV), pp. 504–528.
POPL-2010-NanevskiVB #source code #verification
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
VMCAI-2010-Vafeiadis
RGSep Action Inference (VV), pp. 345–361.
ESOP-2009-DoddsFPV #reasoning
Deny-Guarantee Reasoning (MD, XF, MJP, VV), pp. 363–377.
POPL-2009-GotsmanCPV #algorithm #proving
Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
VMCAI-2009-Vafeiadis #abstraction #verification
Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.
SAS-2007-CalcagnoPV #composition #concurrent #fine-grained #safety
Modular Safety Checking for Fine-Grained Concurrency (CC, MJP, VV), pp. 233–248.
PPoPP-2006-VafeiadisHHS #correctness #proving
Proving correctness of highly-concurrent linearisable objects (VV, MH, CARH, MS), pp. 129–136.
ICFP-2005-SewellLWNAHV #design #distributed #named #programming language
Acute: high-level programming language design for distributed computation (PS, JJL, KW, FZN, MAW, PH, VV), pp. 15–26.
ESOP-2017-DokoV #concurrent
Tackling Real-Life Relaxed Concurrency with FSL++ (MD, VV), pp. 448–475.
ESOP-2018-RaadLV #consistency #on the #parallel
On Parallel Snapshot Isolation and Release/Acquire Consistency (AR, OL, VV), pp. 940–967.
ESOP-2018-SvendsenPDLV #logic #semantics
A Separation Logic for a Promising Semantics (KS, JPP, MD, OL, VV), pp. 357–384.
CAV-2017-Vafeiadis #consistency #logic #memory management #using #verification
Program Verification Under Weak Memory Consistency Using Separation Logic (VV), pp. 30–46.
ECOOP-2017-KaiserDDLV #consistency #logic #memory management #reasoning
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (JOK, HHD, DD, OL, VV), p. 29.
ECOOP-2017-PodkopaevLV #compilation
Promising Compilation to ARMv8 POP (AP, OL, VV), p. 28.
OOPSLA-2018-RaadV #memory management #persistent #semantics
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model (AR, VV), p. 27.
OOPSLA-2019-Kokologiannakis #effectiveness #model checking
Effective lock handling in stateless model checking (MK, AR, VV), p. 26.
OOPSLA-2019-RaadWV #formal method #modelling #semantics #transaction
Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models (AR, JW, VV), p. 27.
POPL-2016-KangKHDV #compilation #lightweight #verification
Lightweight verification of separate compilation (JK, YK, CKH, DD, VV), pp. 178–190.
POPL-2016-LahavGV #consistency
Taming release-acquire consistency (OL, NG, VV), pp. 649–662.
PLDI-2017-LahavVKHD #consistency
Repairing sequential consistency in C/C++11 (OL, VV, JK, CKH, DD), pp. 618–632.
POPL-2017-KangHLVD #concurrent #semantics
A promising semantics for relaxed-memory concurrency (JK, CKH, OL, VV, DD), pp. 175–189.
POPL-2018-Kokologiannakis #c #c++ #concurrent #effectiveness #model checking
Effective stateless model checking for C/C++ concurrency (MK, OL, KS, VV), p. 32.
PLDI-2019-Kokologiannakis #consistency #library #model checking
Model checking for weakly consistent libraries (MK, AR, VV), pp. 96–110.
POPL-2019-ChakrabortyV
Grounding thin-air reads with event structures (SC, VV), p. 28.
POPL-2019-PodkopaevLV #hardware #memory management #modelling #programming language
Bridging the gap between programming languages and hardware weak memory models (AP, OL, VV), p. 31.
POPL-2019-RaadDRLV #concurrent #consistency #correctness #declarative #library #memory management #modelling #on the #specification #verification
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models (AR, MD, LR, OL, VV), p. 31.
POPL-2020-RaadWNV #architecture #semantics
Persistency semantics of the Intel-x86 architecture (AR, JW, GN, VV), p. 31.
ASPLOS-2020-Kokologiannakis #hardware #memory management #model checking #modelling #named
HMC: Model Checking for Hardware Memory Models (MK, VV), pp. 1157–1171.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.