{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:53:10Z","timestamp":1740099190530,"version":"3.37.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_5","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"89-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Complexity Analysis of Tree Share Structure"],"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"}]},{"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158\u2013174. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_14"},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"5_CR3","unstructured":"Appel, A.W., Dockins, R., Hobor, A.: Mechanized semantic library (2009)"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. Theor. Comput. Sci. 11(1), 71\u201377 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR5","unstructured":"Blumensath, A.: Automatic structures. Ph.D. thesis, RWTH Aachen (1999)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/s00224-004-1133-y","volume":"37","author":"A Blumensath","year":"2004","unstructured":"Blumensath, A., Grade, E.: Finite presentations of infinite structures: automata and interpretations. Theory Comput. Syst. 37, 641\u2013674 (2004)","journal-title":"Theory Comput. Syst."},{"key":"5_CR7","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":"5_CR8","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":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Colcombet, T., L\u00f6ding, C.: Transforming structures by set interpretations. Log. Methods Comput. Sci. 3(2) (2007)","DOI":"10.2168\/LMCS-3(2:4)2007"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. In: APAL (1990)","DOI":"10.1016\/0168-0072(90)90080-L"},{"key":"5_CR12","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, version 8.0 (2004)"},{"key":"5_CR13","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":"5_CR14","doi-asserted-by":"crossref","unstructured":"Dohrau, J., Summers, A.J., Urban, C., M\u00fcnger, S., M\u00fcller, P.: Permission inference for array programs. In: CAV (2018)","DOI":"10.1007\/978-3-319-96142-2_7"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-662-54434-1_17","volume-title":"Programming Languages and Systems","author":"M Doko","year":"2017","unstructured":"Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448\u2013475. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_17"},{"key":"5_CR16","unstructured":"Gherghina, C.A.: Efficiently verifying programs with rich control flows. Ph.D. thesis, National University of Singapore (2012)"},{"issue":"5","key":"5_CR17","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0020-0190(90)90051-X","volume":"35","author":"E Gr\u00e4del","year":"1990","unstructured":"Gr\u00e4del, E.: Simple interpretations among complicated theories. Inf. Process. Lett. 35(5), 235\u2013238 (1990)","journal-title":"Inf. Process. Lett."},{"key":"5_CR18","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":"5_CR19","unstructured":"Hobor, A.: Oracle semantics. Ph.D. thesis, Princeton University, Department of Computer Science, Princeton, NJ, October 2008"},{"key":"5_CR20","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":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-06686-8_16","volume-title":"Computer Science - Theory and Applications","author":"S Jain","year":"2014","unstructured":"Jain, S., Khoussainov, B., Stephan, F., Teng, D., Zou, S.: Semiautomatic structures. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.\u00c9., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 204\u2013217. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06686-8_16"},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2743014","volume":"63","author":"A Jez","year":"2016","unstructured":"Jez, A.: Recompression: a simple and powerful technique for word equations. J. ACM 63(1), 4:1\u20134:51 (2016)","journal-title":"J. ACM"},{"key":"5_CR23","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, January 2001"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Le, D.-K., Chin, W.-N., Teo, Y.M.: Threads as resource for concurrency verification. In: PEPM, pp. 73\u201384 (2015)","DOI":"10.1145\/2678015.2682540"},{"key":"5_CR25","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":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-319-89884-1_14","volume-title":"Programming Languages and Systems","author":"X-B Le","year":"2018","unstructured":"Le, X.-B., Hobor, A.: Logical reasoning for disjoint permissions. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 385\u2013414. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_14"},{"key":"5_CR27","unstructured":"Le, X.-B., Hobor, A., Lin, A.W.: Decidability and complexity of tree shares formulas. In: FSTTCS (2016)"},{"key":"5_CR28","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"},{"issue":"2","key":"5_CR29","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G S Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. In: Mat. Sbornik, pp. 147\u2013236 (1977)","journal-title":"Mathematics of the USSR-Sbornik"},{"key":"5_CR30","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1016\/0304-3975(95)00209-X","volume":"160","author":"K Marriott","year":"1996","unstructured":"Marriott, K., Odersky, M.: Negative Boolean constraints. Theor. Comput. Sci. 160, 365\u2013380 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"5_CR31","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR32","unstructured":"Parkinson, M.: Local reasoning for Java. Ph.D. thesis, University of Cambridge (2005)"},{"issue":"1","key":"5_CR33","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1145\/1190215.1190261","volume":"42","author":"Matthew Parkinson","year":"2007","unstructured":"Parkinson, M.J., Bornat, R., O\u2019Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL 2007, pp. 297\u2013302 (2007)","journal-title":"ACM SIGPLAN Notices"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"714","DOI":"10.1007\/3-540-45061-0_56","volume-title":"Automata, Languages and Programming","author":"T Rybina","year":"2003","unstructured":"Rybina, T., Voronkov, A.: Upper bounds for a theory of queues. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 714\u2013724. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_56"},{"key":"5_CR35","unstructured":"Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, M.I.T. (1974)"},{"key":"5_CR36","unstructured":"To, A.W.: Model checking infinite-state systems: generic and specific approaches. Ph.D. thesis, LFCS, School of Informatics, University of Edinburgh (2010)"},{"key":"5_CR37","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":"5_CR38","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: ESOP 2017 (2017)"}],"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-030-02768-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T06:11:15Z","timestamp":1572156675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}