{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:29Z","timestamp":1773996329698,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119569","type":"print"},{"value":"9783642119576","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_32","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:55:38Z","timestamp":1267991738000},"page":"610-629","source":"Crossref","is-referenced-by-count":17,"title":["Explicit Stabilisation for Modular Rely-Guarantee Reasoning"],"prefix":"10.1007","author":[{"given":"John","family":"Wickerson","sequence":"first","affiliation":[]},{"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. In: POPL (1990)","DOI":"10.1145\/96709.96712"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-93900-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Amjad","year":"2009","unstructured":"Amjad, H., Bornat, R.: Towards automatic stability analysis for rely-guarantee proofs. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 14\u201328. Springer, Heidelberg (2009)"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 233\u2013248. Springer, Heidelberg (2007)"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-87873-5_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J.W. Coleman","year":"2008","unstructured":"Coleman, J.W.: Expression decomposition in a Rely\/Guarantee context. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 146\u2013160. Springer, Heidelberg (2008)"},{"key":"32_CR6","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Inc., Englewood Cliffs (1976)"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M. Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-Guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 363\u2013377. Springer, Heidelberg (2009)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL (2009)","DOI":"10.1145\/1480881.1480922"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X. Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3) (2005)","DOI":"10.1016\/j.tcs.2004.12.006"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10) (1969)","DOI":"10.1145\/363235.363259"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"32_CR14","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, University of Oxford (1981)"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL (2004)","DOI":"10.1145\/964001.964024"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"L. Prensa Nieto","year":"2003","unstructured":"Prensa Nieto, L.: The Rely-Guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 348\u2013362. Springer, Heidelberg (2003)"},{"key":"32_CR18","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"32_CR19","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of Rely\/Guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Dodds, M., Parkinson, M.: Explicit Stabilisation for Modular Rely-Guarantee Reasoning. Technical report, University of Cambridge (2010)","DOI":"10.1007\/978-3-642-11957-6_32"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Skidanov, A., Reps, T., Sagiv, M.: Automatic assume\/guarantee reasoning for heap-manipulating programs: Ongoing work. In: AIOOL (2005)","DOI":"10.1016\/j.entcs.2005.01.028"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:32:26Z","timestamp":1558272746000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}