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: "Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings" editor: - name: "Neil D. Jones" link: "http://www.diku.dk/hjemmesider/ansatte/neil/" - name: "Markus Müller-Olm" link: "https://researchr.org/alias/markus-m%C3%BCller-olm" volume: "5403" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-93899-6" 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: "Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010" editor: - name: "Manuel V. Hermenegildo" link: "https://researchr.org/alias/manuel-v.-hermenegildo" - name: "Jens Palsberg" link: "https://researchr.org/alias/jens-palsberg" publisher: "ACM" isbn: "978-1-60558-479-9" 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: "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" 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 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings" editor: - name: "Theo D Hondt" link: "https://researchr.org/alias/theo-d-hondt" volume: "6183" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-14106-5" 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: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005" editor: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "1-59593-064-7" 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: "Journal of Functional Programming" 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: "Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009" editor: - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "978-1-60558-379-2" 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: "Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings" editor: - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" - name: "Manuel V. Hermenegildo" link: "https://researchr.org/alias/manuel-v.-hermenegildo" volume: "5944" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-11318-5" 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 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings" editor: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Vasco Thudichum Vasconcelos" link: "https://researchr.org/alias/vasco-thudichum-vasconcelos" volume: "4703" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-74406-1" 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: "Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings" editor: - name: "Zhenjiang Hu" link: "http://research.nii.ac.jp/~hu/" volume: "5904" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-10671-2" 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: "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: - name: "Josep Torrellas" link: "https://researchr.org/alias/josep-torrellas" - name: "Siddhartha Chatterjee" link: "https://researchr.org/alias/siddhartha-chatterjee" publisher: "ACM" isbn: "1-59593-189-9" 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: "Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011" editor: - name: "Thomas Ball" link: "https://researchr.org/alias/thomas-ball" - name: "Mooly Sagiv" link: "https://researchr.org/alias/mooly-sagiv" publisher: "ACM" isbn: "978-1-4503-0490-0" 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: "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: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" volume: "5502" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-00589-3" 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: "Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings" editor: - name: "Hanne Riis Nielson" link: "https://researchr.org/alias/hanne-riis-nielson" - name: "Gilberto Filé" link: "https://researchr.org/alias/gilberto-fil%C3%A9" volume: "4634" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-74060-5" 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: "Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings" editor: - name: "Tayssir Touili" link: "https://researchr.org/alias/tayssir-touili" - name: "Byron Cook" link: "https://researchr.org/alias/byron-cook" - name: "Paul Jackson" link: "https://researchr.org/alias/paul-jackson" volume: "6174" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-14294-9" 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: "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" kind: "inproceedings" key: "HurDV11"