Suggestions for papers (feel free to choose others, but please confirm with the assistant) ========================================================================================== Concurrency =========== (Allocated to Tobias Hartmann) http://www.eecs.qmul.ac.uk/~ohearn/papers/concur04.pdf Modular Verification of a Non-blocking Stack M Parkinson, R Bornat and P O'Hearn, POPL 2007 (Allocated to Uri Juhasz) Bornat et al - Permission Accounting in Separation Logic, POPL 2005 (Allocated to Simon Hudon) A Fresh Look at Separation Algebras and Share Accounting, by Hobor Aquinas and Robert Dockins and Andrew W. Appel, APLAS 2009 Deny-Guarantee Reasoning, by Mike Dodds, Xinyu Feng, Matthew J. Parkinson and Viktor Vafeiadis. In ESOP 2009. Resource analysis ================= http://personal.cis.strath.ac.uk/~raa/amortised-sep-logic.pdf Shape analysis ============== (Allocated to Milos Novacek) A local shape analysis based on separation logic D Distefano, P O'Hearn and H Yang. In TACAS 2006. (Allocated to Valentin Wuestholz) Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn and Hongseok Yang. Footprint Analysis: A Shape Analysis that Discovers Preconditions (SAS 2007) (Allocated to Simone Frau) Inferring invariants in Separation Logic for imperative list-processing algorithms. S Magill, A Nanevsky, E Clarke and P Lee, SPACE 2006 Tools ===== (Allocated to Alejandro Garcia) Symbolic Execution with Separation Logic. J Berdine, C Calcagno and PW O'Hearn. Proceedings of APLAS'05. (Allocated to Mischael Schill) jStar - http://www.jstarverifier.org/ VeriFast - http://people.cs.kuleuven.be/~bart.jacobs/verifast/ HolFoot - http://www.cl.cam.ac.uk/~tt291/publications/Tuer09.pdf (Allocated to Maria Christakis) Smallfoot: Modular Automatic Assertion Checking with Separation Logic J Berdine, C Calcagno and PW O'Hearn. In 4th FMCO, LNCS 4111, 2006 (Allocated to Malte Schwerhoff) Parkinson et al - The Relationship Between Separation Logic and Implicit Dynamic Frames Proofs of algorithms and systems ================================ Schorr-Waite Algorithm - www.eecs.qmul.ac.uk/~hyang/paper/SchorrWaite.ps Concurrent C minor - http://www.cs.princeton.edu/~appel/cminor/ Compcert - http://compcert.inria.fr/publi.html OO reasoning ============ http://www.itu.dk/~birkedal/papers/veroop-conf.pdf Enhancing Modular OO Verification with Separation Logic W-N Chin, C David H-H Nguyen and S Qin, POPL'08