Parkinson, Matthew; Bornat, Richard; O’Hearn, Peter Modular verification of a non-blocking stack. (English) Zbl 1295.68092 Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’07, Nice, France, January 17–19, 2007. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-575-4). 297-302 (2007). MSC: 68N30 03B70 68N19 68T15 68W40 PDFBibTeX XMLCite \textit{M. Parkinson} et al., in: Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '07, Nice, France, January 17--19, 2007. New York, NY: Association for Computing Machinery (ACM). 297--302 (2007; Zbl 1295.68092) Full Text: DOI
Bornat, Richard; Calcagno, Cristiano; O’Hearn, Peter; Parkinson, Matthew Permission accounting in separation logic. (English) Zbl 1369.68130 Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’05, Long Beach, CA, USA, January 12–14, 2005. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-830-X). 259-270 (2005). MSC: 68N30 68N19 PDFBibTeX XMLCite \textit{R. Bornat} et al., in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '05, Long Beach, CA, USA, January 12--14, 2005. New York, NY: Association for Computing Machinery (ACM). 259--270 (2005; Zbl 1369.68130) Full Text: DOI