References

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