@inproceedings(AmighiBDHMZ14,
 author       = {Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and Zaharieva{-}Stojanovski, Marina},
 year         = {2014},
 title        = {{Verification of Concurrent Systems with VerCors}},
 booktitle    = {Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, {SFM} 2014, Bertinoro, Italy, June 16-20, 2014, Advanced Lectures},
 pages        = {172--216},
 doi          = {10.1007/978-3-319-07317-0_5},
)
@inproceedings(AmighiBH14,
 author       = {Afshin Amighi and Stefan Blom and Marieke Huisman},
 year         = {2014},
 title        = {{Resource Protection Using Atomics - Patterns and Verification}},
 editor       = {Jacques Garrigue},
 booktitle    = {Programming Languages and Systems - 12th Asian Symposium, {APLAS} 2014, Singapore, November 17-19, 2014, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8858},
 publisher    = {Springer},
 pages        = {255--274},
 doi          = {10.1007/978-3-319-12736-1_14},
)
@inproceedings(BlomH14,
 author       = {Stefan Blom and Marieke Huisman},
 year         = {2014},
 title        = {{The VerCors Tool for Verification of Concurrent Programs}},
 booktitle    = {FM},
 pages        = {127--131},
 doi          = {10.1007/978-3-319-06410-9_9},
)
@inproceedings(BornatCOP05,
 author       = {Richard Bornat and Cristiano Calcagno and Peter W. O'Hearn and Matthew J. Parkinson},
 year         = {2005},
 title        = {Permission accounting in separation logic},
 editor       = {Jens Palsberg and Mart{\'{\i}}n Abadi},
 booktitle    = {Proceedings of the 32nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2005, Long Beach, California, USA, January 12-14, 2005},
 publisher    = {{ACM}},
 pages        = {259--270},
 doi          = {10.1145/1040305.1040327},
 url          = {http://dl.acm.org/citation.cfm?id=1040305},
)
@inproceedings(Boyland03,
 author       = {John Boyland},
 year         = {2003},
 title        = {Checking Interference with Fractional Permissions},
 editor       = {Radhia Cousot},
 booktitle    = {Static Analysis, 10th International Symposium, {SAS} 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2694},
 publisher    = {Springer},
 pages        = {55--72},
 doi          = {10.1007/3-540-44898-5_4},
)
@(vct-countdownlatch,
 title        = {Verified {CountDownLatch}},
 url          = {https://github.com/utwente-fmt/vercors/blob/master/examples/synchronizers/CountDownLatch.java},
)
@inproceedings(Dinsdale-YoungDGPV10,
 author       = {Dinsdale{-}Young, Thomas and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
 year         = {2010},
 title        = {Concurrent Abstract Predicates},
 editor       = {Theo D'Hondt},
 booktitle    = {{ECOOP} 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings},
 series       = {LNCS},
 volume       = {6183},
 publisher    = {Springer},
 pages        = {504--528},
 doi          = {10.1007/978-3-642-14107-2_24},
)
@inproceedings(Dinsdale-YoungP17,
 author       = {Dinsdale{-}Young, Thomas and Pedro da Rocha Pinto and Kristoffer Just Andersen and Lars Birkedal},
 year         = {2017},
 title        = {{Caper - Automatic Verification for Fine-Grained Concurrency}},
 booktitle    = {ESOP},
 pages        = {420--447},
 doi          = {10.1007/978-3-662-54434-1_16},
)
@inproceedings(DoddsFPV09,
 author       = {Mike Dodds and Xinyu Feng and Matthew J. Parkinson and Viktor Vafeiadis},
 year         = {2009},
 title        = {Deny-Guarantee Reasoning},
 booktitle    = {ESOP},
 pages        = {363--377},
 doi          = {10.1007/978-3-642-00590-9_26},
)
@article(GotsmanBC11,
 author       = {Alexey Gotsman and Josh Berdine and Byron Cook},
 year         = {2011},
 title        = {{Precision and the Conjunction Rule in Concurrent Separation Logic}},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {276},
 pages        = {171--190},
 doi          = {10.1016/j.entcs.2011.09.021},
)
@inproceedings(JacobsSPVPP11,
 author       = {Bart Jacobs and Jan Smans and Pieter Philippaerts and Fr{\'{e}}d{\'{e}}ric Vogels and Willem Penninckx and Frank Piessens},
 year         = {2011},
 title        = {{VeriFast: {A} Powerful, Sound, Predictable, Fast Verifier for {C} and {J}ava}},
 booktitle    = {NFM},
 pages        = {41--55},
 doi          = {10.1007/978-3-642-20398-5_4},
)
@inproceedings(Jones83-ifip,
 author       = {Cliff B. Jones},
 year         = {1983},
 title        = {Specification and Design of (Parallel) Programs},
 booktitle    = {{IFIP} Congress},
 pages        = {321--332},
)
@inproceedings(JungSSSTBD15,
 author       = {Ralf Jung and David Swasey and Filip Sieczkowski and Kasper Svendsen and Aaron Turon and Lars Birkedal and Derek Dreyer},
 year         = {2015},
 title        = {{Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning}},
 booktitle    = {POPL},
 pages        = {637--650},
 doi          = {10.1145/2676726.2676980},
)
@inproceedings(LeinoMS09,
 author       = {K. Rustan M. Leino and Peter M{\"{u}}ller and Jan Smans},
 year         = {2009},
 title        = {Verification of Concurrent Programs with Chalice},
 editor       = {Alessandro Aldini and Gilles Barthe and Roberto Gorrieri},
 booktitle    = {Foundations of Security Analysis and Design V, {FOSAD} 2007/2008/2009 Tutorial Lectures},
 series       = {Lecture Notes in Computer Science},
 volume       = {5705},
 publisher    = {Springer},
 pages        = {195--222},
 doi          = {10.1007/978-3-642-03829-7_7},
)
@(vct-lock,
 title        = {Verified {Lock}},
 url          = {https://github.com/utwente-fmt/vercors/blob/master/examples/synchronizers/ReentrantLock.java},
)
@inproceedings(0001SS16,
 author       = {Peter M{\"{u}}ller and Malte Schwerhoff and Alexander J. Summers},
 year         = {2016},
 title        = {Viper: {A} Verification Infrastructure for Permission-Based Reasoning},
 booktitle    = {VMCAI},
 pages        = {41--62},
 doi          = {10.1007/978-3-662-49122-5_2},
)
@article(OHearn07,
 author       = {Peter W. O'Hearn},
 year         = {2007},
 title        = {{Resources, concurrency, and local reasoning}},
 journal      = {Theor. Comput. Sci.},
 volume       = {375},
 number       = {1-3},
 pages        = {271--307},
 doi          = {10.1016/j.tcs.2006.12.035},
)
@inproceedings(ParkinsonB08,
 author       = {Matthew J. Parkinson and Gavin M. Bierman},
 year         = {2008},
 title        = {Separation logic, abstraction and inheritance},
 editor       = {George C. Necula and Philip Wadler},
 booktitle    = {Proceedings of the 35th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2008, San Francisco, California, USA, January 7-12, 2008},
 publisher    = {{ACM}},
 pages        = {75--86},
 doi          = {10.1145/1328438.1328451},
 url          = {http://dl.acm.org/citation.cfm?id=1328438},
)
@inproceedings(Reynolds02,
 author       = {John C. Reynolds},
 year         = {2002},
 title        = {Separation Logic: {A} Logic for Shared Mutable Data Structures},
 booktitle    = {17th {IEEE} Symposium on Logic in Computer Science {(LICS} 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings},
 publisher    = {{IEEE} Computer Society},
 pages        = {55--74},
 doi          = {10.1109/LICS.2002.1029817},
 url          = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8005},
)
@(vct-semaphore,
 title        = {Verified {Semaphore}},
 url          = {https://github.com/utwente-fmt/vercors/blob/master/examples/synchronizers/Semaphore.java},
)
@inproceedings(SvendsenB14,
 author       = {Kasper Svendsen and Lars Birkedal},
 year         = {2014},
 title        = {Impredicative Concurrent Abstract Predicates},
 editor       = {Zhong Shao},
 booktitle    = {Programming Languages and Systems - 23rd European Symposium on Programming, {ESOP} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8410},
 publisher    = {Springer},
 pages        = {149--168},
 doi          = {10.1007/978-3-642-54833-8_9},
)
@inproceedings(SvendsenBP13,
 author       = {Kasper Svendsen and Lars Birkedal and Matthew J. Parkinson},
 year         = {2013},
 title        = {Modular Reasoning about Separation of Concurrent Data Structures},
 editor       = {Matthias Felleisen and Philippa Gardner},
 booktitle    = {Programming Languages and Systems - 22nd European Symposium on Programming, {ESOP} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7792},
 publisher    = {Springer},
 pages        = {169--188},
 doi          = {10.1007/978-3-642-37036-6_11},
)
@article(Vafeiadis11,
 author       = {Viktor Vafeiadis},
 year         = {2011},
 title        = {Concurrent Separation Logic and Operational Semantics},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {276},
 pages        = {335--351},
 doi          = {10.1016/j.entcs.2011.09.029},
)
@inproceedings(VafeiadisP07,
 author       = {Viktor Vafeiadis and Matthew J. Parkinson},
 year         = {2007},
 title        = {A Marriage of Rely/Guarantee and Separation Logic},
 editor       = {Lu\'{\i}s Caires and Vasco Thudichum Vasconcelos},
 booktitle    = {{CONCUR} 2007 - Concurrency Theory, 18th International Conference, {CONCUR} 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings},
 series       = {LNCS},
 volume       = {4703},
 publisher    = {Springer},
 pages        = {256--271},
 doi          = {10.1007/978-3-540-74407-8_18},
)
@(vct,
 title        = {VerCors Tool Set},
 url          = {http://ctit-vm3.ewi.utwente.nl/vercors-verifier/},
)