@inproceedings{Vafeiadis09,
  title = {Shape-Value Abstraction for Verifying Linearizability},
  author = {Viktor Vafeiadis},
  year = {2009},
  doi = {10.1007/978-3-540-93900-9_27},
  url = {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},
}

@inproceedings{NanevskiVB10,
  title = {Structuring the verification of heap-manipulating programs},
  author = {Aleksandar Nanevski and Viktor Vafeiadis and Josh Berdine},
  year = {2010},
  doi = {10.1145/1706299.1706331},
  url = {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},
}

@inproceedings{CookGMRSSV09,
  title = {Finding heap-bounds for hardware synthesis},
  author = {Byron Cook and Ashutosh Gupta and Stephen Magill and Andrey Rybalchenko and Jirí Simsa and Satnam Singh and Viktor Vafeiadis},
  year = {2009},
  doi = {10.1109/FMCAD.2009.5351120},
  url = {http://dx.doi.org/10.1109/FMCAD.2009.5351120},
  researchr = {https://researchr.org/publication/CookGMRSSV09},
  cites = {0},
  citedby = {0},
  pages = {205-212},
  booktitle = {FMCAD},
}

@inproceedings{Dinsdale-YoungDGPV10,
  title = {Concurrent Abstract Predicates},
  author = {Thomas Dinsdale-Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
  year = {2010},
  doi = {10.1007/978-3-642-14107-2_24},
  url = {http://dx.doi.org/10.1007/978-3-642-14107-2_24},
  researchr = {https://researchr.org/publication/Dinsdale-YoungDGPV10},
  cites = {0},
  citedby = {0},
  pages = {504-528},
  booktitle = {ECOOP},
}

@inproceedings{SewellLWNAHV05,
  title = {Acute: high-level programming language design for distributed computation},
  author = {Peter Sewell and James J. Leifer and Keith Wansbrough and Francesco Zappa Nardelli and Mair Allen-Williams and Pierre Habouzit and Viktor Vafeiadis},
  year = {2005},
  doi = {10.1145/1086365.1086370},
  url = {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},
}

@article{SewellLWNAHV07,
  title = {Acute: High-level programming language design for distributed computation},
  author = {Peter Sewell and James J. Leifer and Keith Wansbrough and Francesco Zappa Nardelli and Mair Allen-Williams and Pierre Habouzit and Viktor Vafeiadis},
  year = {2007},
  doi = {10.1017/S0956796807006442},
  url = {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},
}

@inproceedings{GotsmanCPV09,
  title = {Proving that non-blocking algorithms don t block},
  author = {Alexey Gotsman and Byron Cook and Matthew J. Parkinson and Viktor Vafeiadis},
  year = {2009},
  doi = {10.1145/1480881.1480886},
  url = {http://doi.acm.org/10.1145/1480881.1480886},
  researchr = {https://researchr.org/publication/GotsmanCPV09},
  cites = {0},
  citedby = {0},
  pages = {16-28},
  booktitle = {POPL},
}

@inproceedings{Vafeiadis10,
  title = {RGSep Action Inference},
  author = {Viktor Vafeiadis},
  year = {2010},
  doi = {10.1007/978-3-642-11319-2_25},
  url = {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},
}

@inproceedings{VafeiadisP07,
  title = {A Marriage of Rely/Guarantee and Separation Logic},
  author = {Viktor Vafeiadis and Matthew J. Parkinson},
  year = {2007},
  doi = {10.1007/978-3-540-74407-8_18},
  url = {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},
}

@inproceedings{CalcagnoDV09,
  title = {Bi-abductive Resource Invariant Synthesis},
  author = {Cristiano Calcagno and Dino Distefano and Viktor Vafeiadis},
  year = {2009},
  doi = {10.1007/978-3-642-10672-9_19},
  url = {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},
}

@inproceedings{VafeiadisHHS06,
  title = {Proving correctness of highly-concurrent linearisable objects},
  author = {Viktor Vafeiadis and Maurice Herlihy and Tony Hoare and Marc Shapiro},
  year = {2006},
  doi = {10.1145/1122971.1122992},
  url = {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},
}

@inproceedings{SevcikVNJS11,
  title = {Relaxed-memory concurrency and verified compilation},
  author = {Jaroslav Sevcík and Viktor Vafeiadis and Francesco Zappa Nardelli and Suresh Jagannathan and Peter Sewell},
  year = {2011},
  doi = {10.1145/1926385.1926393},
  url = {http://doi.acm.org/10.1145/1926385.1926393},
  researchr = {https://researchr.org/publication/SevcikVNJS11},
  cites = {0},
  citedby = {0},
  pages = {43-54},
  booktitle = {POPL},
}

@inproceedings{DoddsFPV09,
  title = {Deny-Guarantee Reasoning},
  author = {Mike Dodds and Xinyu Feng and Matthew J. Parkinson and Viktor Vafeiadis},
  year = {2009},
  doi = {10.1007/978-3-642-00590-9_26},
  url = {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},
}

@inproceedings{CalcagnoPV07,
  title = {Modular Safety Checking for Fine-Grained Concurrency},
  author = {Cristiano Calcagno and Matthew J. Parkinson and Viktor Vafeiadis},
  year = {2007},
  doi = {10.1007/978-3-540-74061-2_15},
  url = {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},
}

@inproceedings{Vafeiadis10-0,
  title = {Automatically Proving Linearizability},
  author = {Viktor Vafeiadis},
  year = {2010},
  doi = {10.1007/978-3-642-14295-6_40},
  url = {http://dx.doi.org/10.1007/978-3-642-14295-6_40},
  researchr = {https://researchr.org/publication/Vafeiadis10-0},
  cites = {0},
  citedby = {0},
  pages = {450-464},
  booktitle = {cav},
}

@inproceedings{HurDV11,
  title = {Separation Logic in the Presence of Garbage Collection},
  author = {Chung-Kil Hur and Derek Dreyer and Viktor Vafeiadis},
  year = {2011},
  doi = {10.1109/LICS.2011.46},
  url = {http://dx.doi.org/10.1109/LICS.2011.46},
  tags = {logic},
  researchr = {https://researchr.org/publication/HurDV11},
  cites = {0},
  citedby = {0},
  pages = {247-256},
  booktitle = {lics},
}