publications:
- title: "Shape-Value Abstraction for Verifying Linearizability"
  author:
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-540-93900-9_27"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-93900-9_27"
  tags:
  - "abstraction"
  researchr: "https://researchr.org/publication/Vafeiadis09"
  cites: 0
  citedby: 0
  pages: "335-348"
  booktitle: "vmcai"
  kind: "inproceedings"
  key: "Vafeiadis09"
- title: "Structuring the verification of heap-manipulating programs"
  author:
  - name: "Aleksandar Nanevski"
    link: "https://researchr.org/alias/aleksandar-nanevski"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  - name: "Josh Berdine"
    link: "https://researchr.org/alias/josh-berdine"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1706299.1706331"
  links:
    doi: "http://doi.acm.org/10.1145/1706299.1706331"
  tags:
  - "program verification"
  researchr: "https://researchr.org/publication/NanevskiVB10"
  cites: 0
  citedby: 0
  pages: "261-274"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "NanevskiVB10"
- title: "Finding heap-bounds for hardware synthesis"
  author:
  - name: "Byron Cook"
    link: "https://researchr.org/alias/byron-cook"
  - name: "Ashutosh Gupta"
    link: "https://researchr.org/alias/ashutosh-gupta"
  - name: "Stephen Magill"
    link: "https://researchr.org/alias/stephen-magill"
  - name: "Andrey Rybalchenko"
    link: "https://researchr.org/alias/andrey-rybalchenko"
  - name: "Jirí Simsa"
    link: "https://researchr.org/alias/jir%C3%A3%C2%AD-simsa"
  - name: "Satnam Singh"
    link: "https://researchr.org/alias/satnam-singh"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2009"
  doi: "http://dx.doi.org/10.1109/FMCAD.2009.5351120"
  links:
    doi: "http://dx.doi.org/10.1109/FMCAD.2009.5351120"
  researchr: "https://researchr.org/publication/CookGMRSSV09"
  cites: 0
  citedby: 0
  pages: "205-212"
  booktitle: "FMCAD"
  kind: "inproceedings"
  key: "CookGMRSSV09"
- title: "Concurrent Abstract Predicates"
  author:
  - name: "Thomas Dinsdale-Young"
    link: "https://researchr.org/alias/thomas-dinsdale-young"
  - name: "Mike Dodds"
    link: "http://www-users.cs.york.ac.uk/~miked/"
  - name: "Philippa Gardner"
    link: "https://researchr.org/alias/philippa-gardner"
  - name: "Matthew J. Parkinson"
    link: "https://researchr.org/alias/matthew-j.-parkinson"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-14107-2_24"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-14107-2_24"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/Dinsdale-YoungDGPV10"
  researchr: "https://researchr.org/publication/Dinsdale-YoungDGPV10"
  cites: 0
  citedby: 0
  pages: "504-528"
  booktitle: "ECOOP"
  kind: "inproceedings"
  key: "Dinsdale-YoungDGPV10"
- title: "Acute: high-level programming language design for distributed computation"
  author:
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  - name: "James J. Leifer"
    link: "https://researchr.org/alias/james-j.-leifer"
  - name: "Keith Wansbrough"
    link: "https://researchr.org/alias/keith-wansbrough"
  - name: "Francesco Zappa Nardelli"
    link: "https://researchr.org/alias/francesco-zappa-nardelli"
  - name: "Mair Allen-Williams"
    link: "https://researchr.org/alias/mair-allen-williams"
  - name: "Pierre Habouzit"
    link: "https://researchr.org/alias/pierre-habouzit"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1086365.1086370"
  links:
    doi: "http://doi.acm.org/10.1145/1086365.1086370"
  tags:
  - "programming languages"
  - "language design"
  - "programming"
  - "design"
  researchr: "https://researchr.org/publication/SewellLWNAHV05"
  cites: 0
  citedby: 0
  pages: "15-26"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "SewellLWNAHV05"
- title: "Acute: High-level programming language design for distributed computation"
  author:
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  - name: "James J. Leifer"
    link: "https://researchr.org/alias/james-j.-leifer"
  - name: "Keith Wansbrough"
    link: "https://researchr.org/alias/keith-wansbrough"
  - name: "Francesco Zappa Nardelli"
    link: "https://researchr.org/alias/francesco-zappa-nardelli"
  - name: "Mair Allen-Williams"
    link: "https://researchr.org/alias/mair-allen-williams"
  - name: "Pierre Habouzit"
    link: "https://researchr.org/alias/pierre-habouzit"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2007"
  doi: "http://dx.doi.org/10.1017/S0956796807006442"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796807006442"
  tags:
  - "programming languages"
  - "language design"
  - "programming"
  - "design"
  researchr: "https://researchr.org/publication/SewellLWNAHV07"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "17"
  number: "4-5"
  pages: "547-612"
  kind: "article"
  key: "SewellLWNAHV07"
- title: "Proving that non-blocking algorithms don t block"
  author:
  - name: "Alexey Gotsman"
    link: "https://researchr.org/alias/alexey-gotsman"
  - name: "Byron Cook"
    link: "https://researchr.org/alias/byron-cook"
  - name: "Matthew J. Parkinson"
    link: "https://researchr.org/alias/matthew-j.-parkinson"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1480881.1480886"
  links:
    doi: "http://doi.acm.org/10.1145/1480881.1480886"
  researchr: "https://researchr.org/publication/GotsmanCPV09"
  cites: 0
  citedby: 0
  pages: "16-28"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "GotsmanCPV09"
- title: "RGSep Action Inference"
  author:
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-11319-2_25"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-11319-2_25"
  researchr: "https://researchr.org/publication/Vafeiadis10"
  cites: 0
  citedby: 0
  pages: "345-361"
  booktitle: "vmcai"
  kind: "inproceedings"
  key: "Vafeiadis10"
- title: "A Marriage of Rely/Guarantee and Separation Logic"
  author:
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  - name: "Matthew J. Parkinson"
    link: "https://researchr.org/alias/matthew-j.-parkinson"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-74407-8_18"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-74407-8_18"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/VafeiadisP07"
  cites: 0
  citedby: 0
  pages: "256-271"
  booktitle: "concur"
  kind: "inproceedings"
  key: "VafeiadisP07"
- title: "Bi-abductive Resource Invariant Synthesis"
  author:
  - name: "Cristiano Calcagno"
    link: "https://researchr.org/alias/cristiano-calcagno"
  - name: "Dino Distefano"
    link: "https://researchr.org/alias/dino-distefano"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-10672-9_19"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-10672-9_19"
  researchr: "https://researchr.org/publication/CalcagnoDV09"
  cites: 0
  citedby: 0
  pages: "259-274"
  booktitle: "aplas"
  kind: "inproceedings"
  key: "CalcagnoDV09"
- title: "Proving correctness of highly-concurrent linearisable objects"
  author:
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  - name: "Maurice Herlihy"
    link: "https://researchr.org/alias/maurice-herlihy"
  - name: "Tony Hoare"
    link: "https://researchr.org/alias/tony-hoare"
  - name: "Marc Shapiro"
    link: "https://researchr.org/alias/marc-shapiro"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1122971.1122992"
  links:
    doi: "http://doi.acm.org/10.1145/1122971.1122992"
  tags:
  - "meta-model"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/VafeiadisHHS06"
  cites: 0
  citedby: 0
  pages: "129-136"
  booktitle: "ppopp"
  kind: "inproceedings"
  key: "VafeiadisHHS06"
- title: "Relaxed-memory concurrency and verified compilation"
  author:
  - name: "Jaroslav Sevcík"
    link: "https://researchr.org/alias/jaroslav-sevc%C3%ADk"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  - name: "Francesco Zappa Nardelli"
    link: "https://researchr.org/alias/francesco-zappa-nardelli"
  - name: "Suresh Jagannathan"
    link: "https://researchr.org/alias/suresh-jagannathan"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/1926385.1926393"
  links:
    doi: "http://doi.acm.org/10.1145/1926385.1926393"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/SevcikVNJS11"
  researchr: "https://researchr.org/publication/SevcikVNJS11"
  cites: 0
  citedby: 0
  pages: "43-54"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "SevcikVNJS11"
- title: "Deny-Guarantee Reasoning"
  author:
  - name: "Mike Dodds"
    link: "http://www-users.cs.york.ac.uk/~miked/"
  - name: "Xinyu Feng"
    link: "https://researchr.org/alias/xinyu-feng"
  - name: "Matthew J. Parkinson"
    link: "https://researchr.org/alias/matthew-j.-parkinson"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-00590-9_26"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-00590-9_26"
  researchr: "https://researchr.org/publication/DoddsFPV09"
  cites: 0
  citedby: 0
  pages: "363-377"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "DoddsFPV09"
- title: "Modular Safety Checking for Fine-Grained Concurrency"
  author:
  - name: "Cristiano Calcagno"
    link: "https://researchr.org/alias/cristiano-calcagno"
  - name: "Matthew J. Parkinson"
    link: "https://researchr.org/alias/matthew-j.-parkinson"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-74061-2_15"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-74061-2_15"
  researchr: "https://researchr.org/publication/CalcagnoPV07"
  cites: 0
  citedby: 0
  pages: "233-248"
  booktitle: "SAS"
  kind: "inproceedings"
  key: "CalcagnoPV07"
- title: "Automatically Proving Linearizability"
  author:
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-14295-6_40"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-14295-6_40"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cav/Vafeiadis10"
  researchr: "https://researchr.org/publication/Vafeiadis10-0"
  cites: 0
  citedby: 0
  pages: "450-464"
  booktitle: "cav"
  kind: "inproceedings"
  key: "Vafeiadis10-0"
- title: "Separation Logic in the Presence of Garbage Collection"
  author:
  - name: "Chung-Kil Hur"
    link: "https://researchr.org/alias/chung-kil-hur"
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Viktor Vafeiadis"
    link: "http://www.mpi-sws.org/~viktor"
  year: "2011"
  doi: "http://dx.doi.org/10.1109/LICS.2011.46"
  links:
    doi: "http://dx.doi.org/10.1109/LICS.2011.46"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/HurDV11"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/HurDV11"
  cites: 0
  citedby: 0
  pages: "247-256"
  booktitle: "lics"
  kind: "inproceedings"
  key: "HurDV11"