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: Vafeiadis:Viktor
Contributed to:
2015
2015
2015
2015
2015
20142013201320132012
20112011
2011
201020102010
2010
2009200920092007
200620052017201820172017201820192016201720172018201920192020
2020Wrote 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.