{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:21:58Z","timestamp":1726410118046},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_12","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"169-182","source":"Crossref","is-referenced-by-count":13,"title":["The Next 700 Separation Logics"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Parkinson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., Deline, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Bell, C.J., Appel, A., Walker, D.: Concurrent separation logic for pipelined parallelization. In: The 17th Annual Static Analysis Symposium (2009)","DOI":"10.1007\/978-3-642-15769-1_10"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for ALGOL-like languages. Logical Methods in Computer Science\u00a02(5) (2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"12_CR7","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.: Local reasoning, separation and aliasing. In: SPACE (2004)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2003)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S. Brookes","year":"2004","unstructured":"Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: PLDI, pp. 66\u201377 (2007)","DOI":"10.1145\/1250734.1250743"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: POPL (2005)","DOI":"10.1145\/1040305.1040328"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Local reasoning about data update. Festschrift Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, 172 (2007)","DOI":"10.1016\/j.entcs.2007.02.006"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Symp. on Logic in Comp. Sci. (LICS 2007), pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"issue":"8","key":"12_CR14","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., Vafeiadis, V.: Concurrent abstract predicates. In: ECOOP (2010)","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"12_CR16","unstructured":"Dinsdale-Young, T., Gardner, P., Wheelhouse, M.: Locality refinement. Technical Report DTR10-8, Imperial College London (2010)"},{"key":"12_CR17","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":"12_CR18","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL (2009)","DOI":"10.1145\/1480881.1480922"},{"key":"12_CR19","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":"12_CR20","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: PLDI, pp. 170\u2013182 (2008)","DOI":"10.1145\/1375581.1375603"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-87873-5_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"X. Feng","year":"2008","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 54\u201369. Springer, Heidelberg (2008)"},{"key":"12_CR22","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":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-89330-1_13","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2008","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java\u2019s Reentrant Locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 171\u2013187. Springer, Heidelberg (2008)"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf.\u00a01, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"key":"12_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2008.04.050","volume":"212","author":"C.A.R. Hoare","year":"2008","unstructured":"Hoare, C.A.R., O\u2019Hearn, P.W.: Separation logic semantics for communicating processes. Electr. Notes Theor. Comput. Sci.\u00a0212, 3\u201325 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR26","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)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, January 2001, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"issue":"4","key":"12_CR28","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":"12_CR29","volume-title":"The C Programming Language","author":"B.W. Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall, Englewood Cliffs (1988)","edition":"2"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: Proceedings of TLDI 2009, pp. 105\u2013116 (2009)","DOI":"10.1145\/1481861.1481874"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Birkedal, L., Aldrich, J.: Verifying event-driven programs using ramified frame properties. In: TLDI, pp. 63\u201376 (2010)","DOI":"10.1145\/1708016.1708025"},{"issue":"8","key":"12_CR32","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"3","key":"12_CR33","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/365230.365257","volume":"9","author":"P.J. Landin","year":"1966","unstructured":"Landin, P.J.: The next 700 programming languages. Commun. ACM\u00a09(3), 157\u2013166 (1966)","journal-title":"Commun. ACM"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: PLDI, pp. 468\u2013479 (2007)","DOI":"10.1145\/1250734.1250788"},{"issue":"3","key":"12_CR35","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J.C. Mitchell","year":"1988","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst.\u00a010(3), 470\u2013502 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-71316-6_14","volume-title":"Programming Languages and Systems","author":"A. Nanevski","year":"2007","unstructured":"Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 189\u2013204. Springer, Heidelberg (2007)"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-11957-6_2","volume-title":"Programming Languages and Systems","author":"D.A. Naumann","year":"2010","unstructured":"Naumann, D.A., Banerjee, A.: Dynamic boundaries: Information hiding by second order framing with first order assertions. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 2\u201322. Springer, Heidelberg (2010)"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 49\u201367. Springer, Heidelberg (2004)"},{"key":"12_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"12_CR40","first-page":"268","volume-title":"Proc. 31th ACM Symp. on Principles of Prog. Lang.","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. 31th ACM Symp. on Principles of Prog. Lang., January 2004, pp. 268\u2013280. ACM Press, New York (2004)"},{"key":"12_CR41","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf.\u00a06, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"12_CR42","unstructured":"Parkinson, M.: Local Reasoning for Java. PhD thesis, University of Cambridge (November 2005)"},{"key":"12_CR43","volume-title":"ACM Symposium on Principles of Programming Languages (POPL 2008)","author":"M. Parkinson","year":"2008","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: ACM Symposium on Principles of Programming Languages (POPL 2008). ACM Press, New York (January 2008)"},{"key":"12_CR44","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"12_CR45","first-page":"399","volume-title":"The secret history of information hiding","author":"D.L. Parnas","year":"2002","unstructured":"Parnas, D.L.: The secret history of information hiding, pp. 399\u2013409. Springer, New York (2002)"},{"key":"12_CR46","doi-asserted-by":"crossref","unstructured":"Pottier, F.: Hiding local state in direct style: A higher-order anti-frame rule. In: LICS, pp. 331\u2013340 (2008)","DOI":"10.1109\/LICS.2008.16"},{"key":"12_CR47","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"key":"12_CR48","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"12_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-04027-6_32","volume-title":"Computer Science Logic","author":"J. Schwinghammer","year":"2009","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 440\u2013454. Springer, Heidelberg (2009)"},{"key":"12_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-642-12032-9_2","volume-title":"FOSSACS 2010","author":"J. Schwinghammer","year":"2010","unstructured":"Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B.: A semantic foundation for hidden state. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 2\u201317. Springer, Heidelberg (2010)"},{"key":"12_CR51","doi-asserted-by":"crossref","unstructured":"Torp-Smith, N., Birkedal, L., Reynolds, J.C.: Local reasoning about a copying garbage collector. ACM Trans. Program. Lang. Syst.\u00a030(4) (2008)","DOI":"10.1145\/1377492.1377499"},{"key":"12_CR52","unstructured":"Vafeiadis, V.: Modular Fine-Grained Concurrency Verification. PhD thesis, University of Cambridge (July 2007)"},{"key":"12_CR53","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":"12_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-10672-9_15","volume-title":"Programming Languages and Systems","author":"J. Villard","year":"2009","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 194\u2013209. Springer, Heidelberg (2009)"},{"key":"12_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-12002-2_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Villard","year":"2010","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Tracking heaps that hop with heap-hop. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 275\u2013279. Springer, Heidelberg (2010)"},{"key":"12_CR56","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Dodds, M., Parkinson, M.J.: Explicit stabilisation for modular rely-guarantee reasoning. In: ESOP, pp. 610\u2013629 (2010)","DOI":"10.1007\/978-3-642-11957-6_32"},{"key":"12_CR57","unstructured":"Yang, H.: An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Proceedings of the 1st Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (January 2001), http:\/\/www.dcs.qmul.ac.uk\/~hyang\/paper\/SchorrWaite.ps"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T15:53:32Z","timestamp":1636041212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}