{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T09:10:13Z","timestamp":1761988213960,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_26","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"363-377","source":"Crossref","is-referenced-by-count":76,"title":["Deny-Guarantee Reasoning"],"prefix":"10.1007","author":[{"given":"Mike","family":"Dodds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","first-page":"259","volume-title":"POPL 2005","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005, pp. 259\u2013270. ACM Press, New York (2005)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"26_CR3","first-page":"366","volume-title":"LICS 2007","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366\u2013378. IEEE Computer Society, Los Alamitos (2007)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning (extended version and formalization in Isabelle). Technical Report UCAM-CL-TR-736, University of Cambridge (2009), http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-736.html","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"26_CR5","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":"26_CR6","first-page":"254","volume-title":"ICFP 2005","author":"X. Feng","year":"2005","unstructured":"Feng, X., Shao, Z.: Modular verification of concurrent assembly code with dynamic thread creation and termination. In: ICFP 2005, pp. 254\u2013267. ACM Press, New York (2005)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C. Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a java-like language with fork\/join. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"issue":"4","key":"26_CR10","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR11","unstructured":"Jones, C.B.: Annoted bibliography on rely\/guarantee conditions (2007), http:\/\/homepages.cs.ncl.ac.uk\/cliff.jones\/ftp-stuff\/rg-hist.pdf"},{"key":"26_CR12","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)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00590-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T00:23:40Z","timestamp":1558225420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}