{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:10Z","timestamp":1740099070187,"version":"3.37.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319898834"},{"type":"electronic","value":"9783319898841"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_14","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"385-414","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Logical Reasoning for Disjoint Permissions"],"prefix":"10.1007","author":[{"given":"Xuan-Bach","family":"Le","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"14_CR1","unstructured":"http:\/\/www.comp.nus.edu.sg\/~lxbach\/tools\/share_infer\/"},{"key":"14_CR2","unstructured":"http:\/\/www.comp.nus.edu.sg\/~lxbach\/publication\/permission_full.pdf"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Cristiano, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"14_CR5","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. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"issue":"6","key":"14_CR6","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/1749608.1749611","volume":"32","author":"JT Boyland","year":"2010","unstructured":"Boyland, J.T.: Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst. 32(6), 22 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"14_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328897.1328453","volume":"43","author":"James Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-319-63046-5_29","volume-title":"Automated Deduction \u2013 CADE 26","author":"J Brotherston","year":"2017","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M.: Biabduction (and related problems) in array separation logic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 472\u2013490. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_29"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2015","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1145\/1594834.1480917","volume":"44","author":"Cristiano Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-10672-9_19","volume-title":"Programming Languages and Systems","author":"C Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., Vafeiadis, V.: Bi-abductive resource invariant synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 259\u2013274. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_19"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-54434-1_10","volume-title":"Programming Languages and Systems","author":"A Chargu\u00e9raud","year":"2017","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Temporary read-only permissions for separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 260\u2013286. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_10"},{"issue":"9","key":"14_CR14","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"14_CR15","unstructured":"Chin, W.N., Le, T.C., Qin, S.: Automated verification of countdownlatch (2017)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P Rocha Pinto da","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"Thomas Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., Pinto, P.D.R., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: ESOP (2017)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R Dockins","year":"2009","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI (2007)","DOI":"10.1145\/1250734.1250764"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Heule, S., Leino, K.R.M., M\u00fcller, P., Summers, A.J.: Fractional permissions without the fractions. In: FTfJP, pp. 1:1\u20131:6 (2011)","DOI":"10.1145\/2076674.2076675"},{"key":"14_CR24","unstructured":"Hobor, A.: Oracle Semantics. Ph.D. thesis, Department of Computer Science, Princeton University, Princeton, October 2008"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-19718-5_15","volume-title":"Programming Languages and Systems","author":"A Hobor","year":"2011","unstructured":"Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276\u2013296. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_15"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: now with tool support! Log. Methods Comput. Sci. 8(2) (2012)","DOI":"10.2168\/LMCS-8(2:2)2012"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: POPL (2017)","DOI":"10.1145\/3009837.3009893"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL (2011)","DOI":"10.1145\/1926385.1926417"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304\u2013311. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_21"},{"issue":"1","key":"14_CR30","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/2775051.2676980","volume":"50","author":"Ralf Jung","year":"2015","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Le, D.-K., Chin, W.-N., Teo, Y.M.: Threads as resource for concurrency verification. In: PEPM (2015)","DOI":"10.1145\/2678015.2682540"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-08867-9_4","volume-title":"Computer Aided Verification","author":"QL Le","year":"2014","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_4"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-35182-2_26","volume-title":"Programming Languages and Systems","author":"XB Le","year":"2012","unstructured":"Le, X.B., Gherghina, C., Hobor, A.: Decision procedures over sophisticated fractional permissions. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 368\u2013385. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_26"},{"key":"14_CR34","unstructured":"Le, X.-B., Hobor, A., Lin, A.W.: Decidability and complexity of tree shares formulas. In: FSTTCS (2016)"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-319-68690-5_14","volume-title":"Formal Methods and Software Engineering","author":"X-B Le","year":"2017","unstructured":"Le, X.-B., Nguyen, T.-T., Chin, W.-N., Hobor, A.: A certified decision procedure for tree shares. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 226\u2013242. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_14"},{"key":"14_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"Programming Languages and Systems","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378\u2013393. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_27"},{"key":"14_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"14_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"A Nanevski","year":"2014","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290\u2013310. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_16"},{"key":"14_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"HH Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251\u2013266. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_18"},{"issue":"1\u20133","key":"14_CR40","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW OHearn","year":"2007","unstructured":"OHearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR41","unstructured":"Parkinson, M.: Local Reasoning for Java. Ph.D. thesis, University of Cambridge (2005)"},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., O\u2019Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL (2007)","DOI":"10.1145\/1190216.1190261"},{"key":"14_CR43","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"issue":"6","key":"14_CR44","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/2813885.2737964","volume":"50","author":"Ilya Sergey","year":"2015","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR45","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis (2008)"},{"key":"14_CR46","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. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"key":"14_CR47","unstructured":"Villard, J.: Heaps and Hops. Ph.D. thesis, Laboratoire Sp\u00e9cification et V\u00e9rification, \u00c9cole Normale Sup\u00e9rieure de Cachan, France, February 2011"},{"key":"14_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-319-63387-9_27","volume-title":"Computer Aided Verification","author":"M Windsor","year":"2017","unstructured":"Windsor, M., Dodds, M., Simner, B., Parkinson, M.J.: Starling: lightweight concurrency verification with views. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 544\u2013569. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_27"},{"key":"14_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385\u2013398. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_36"}],"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-319-89884-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:05Z","timestamp":1571157185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}