@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 = {Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings}, editor = {Neil D. Jones and Markus Müller-Olm}, volume = {5403}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-93899-6}, } @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 = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010}, editor = {Manuel V. Hermenegildo and Jens Palsberg}, publisher = {ACM}, isbn = {978-1-60558-479-9}, } @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 = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA}, publisher = {IEEE}, isbn = {978-1-4244-4966-8}, } @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 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings}, editor = {Theo D Hondt}, volume = {6183}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-14106-5}, } @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 = {Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005}, editor = {Olivier Danvy and Benjamin C. Pierce}, publisher = {ACM}, isbn = {1-59593-064-7}, } @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 = {Journal of Functional Programming}, 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 = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009}, editor = {Zhong Shao and Benjamin C. Pierce}, publisher = {ACM}, isbn = {978-1-60558-379-2}, } @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 = {Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings}, editor = {Gilles Barthe and Manuel V. Hermenegildo}, volume = {5944}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-11318-5}, } @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 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings}, editor = {Luís Caires and Vasco Thudichum Vasconcelos}, volume = {4703}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-74406-1}, } @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 = {Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings}, editor = {Zhenjiang Hu}, volume = {5904}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-10671-2}, } @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 = {Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006, New York, New York, USA, March 29-31, 2006}, editor = {Josep Torrellas and Siddhartha Chatterjee}, publisher = {ACM}, isbn = {1-59593-189-9}, } @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 = {Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011}, editor = {Thomas Ball and Mooly Sagiv}, publisher = {ACM}, isbn = {978-1-4503-0490-0}, } @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 = {Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings}, editor = {Giuseppe Castagna}, volume = {5502}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-00589-3}, } @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 = {Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings}, editor = {Hanne Riis Nielson and Gilberto Filé}, volume = {4634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-74060-5}, } @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 = {Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings}, editor = {Tayssir Touili and Byron Cook and Paul Jackson}, volume = {6174}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-14294-9}, } @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 = {Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada}, publisher = {IEEE Computer Society}, isbn = {978-0-7695-4412-0}, }