{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:01:15Z","timestamp":1743073275224,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319686899"},{"type":"electronic","value":"9783319686905"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68690-5_14","type":"book-chapter","created":{"date-parts":[[2017,10,9]],"date-time":"2017-10-09T21:14:51Z","timestamp":1507583691000},"page":"226-242","source":"Crossref","is-referenced-by-count":2,"title":["A Certified Decision Procedure for Tree Shares"],"prefix":"10.1007","author":[{"given":"Xuan-Bach","family":"Le","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thanh-Toan","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,10,11]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, New York (2014)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! - a framework for higher-order separation logic in Coq. In: ITP, pp. 315\u2013331 (2012)","DOI":"10.1007\/978-3-642-32347-8_21"},{"key":"14_CR3","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\/1040305.1040327"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Boyland, J.T., M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Constraint semantics for abstract read permissions. In: FTfJP, pp. 2:1\u20132:6 (2014)","DOI":"10.1145\/2635631.2635847"},{"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). doi: 10.1007\/3-540-44898-5_4"},{"key":"14_CR6","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_CR7","unstructured":"Chin, W.N., Le, T.C., Qin, S.: Automated verification of countdownlatch (2017)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In: ICFP, pp. 391\u2013402 (2013)","DOI":"10.1145\/2500365.2500592"},{"key":"14_CR9","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 3 edn. MIT Press (2009)"},{"key":"14_CR10","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). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"T Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: Automatic verification for fine-grained concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420\u2013447. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54434-1_16"},{"key":"14_CR12","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). doi: 10.1007\/978-3-642-14107-2_24"},{"key":"14_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). doi: 10.1007\/978-3-642-10672-9_13"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/978-3-319-27340-2_69","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2015","author":"J Fiedor","year":"2015","unstructured":"Fiedor, J., Letko, Z., Louren\u00e7o, J., Vojnar, T.: Dynamic validation of contracts in concurrent code. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2015. LNCS, vol. 9520, pp. 555\u2013564. Springer, Cham (2015). doi: 10.1007\/978-3-319-27340-2_69"},{"key":"14_CR15","unstructured":"Gherghina, C.A.: Efficiently verifying programs with rich control flows. Ph.D. thesis, National University of Singapore (2012)"},{"key":"14_CR16","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). doi: 10.1007\/978-3-642-19718-5_15"},{"key":"14_CR17","unstructured":"Hobor, A.: Oracle semantics. Ph.D. thesis, Princeton University, Department of Computer Science, Princeton, NJ, October 2008"},{"key":"14_CR18","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. 4960, pp. 353\u2013367. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78739-6_27"},{"issue":"2","key":"14_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(2:2)2012","volume":"8","author":"A Hobor","year":"2012","unstructured":"Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: now with tool support!. Logical Methods Comput. Sci. 8(2), 1\u201336 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: POPL, pp. 473\u2013485 (2017)","DOI":"10.1145\/3093333.3009893"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Huisman, M., Mostowski, W.: A symbolic approach to permission accounting for concurrent reasoning. In: ISPDC, pp. 165\u2013174 (2015)","DOI":"10.1109\/ISPDC.2015.26"},{"key":"14_CR22","doi-asserted-by":"crossref","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, pp. 637\u2013650 (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"K\u0159ena, B., Letko, Z., Vojnar, T., Ur, S.: A platform for search-based testing of concurrent software. In: PADTAD, pp. 48\u201358 (2010)","DOI":"10.1145\/1866210.1866215"},{"key":"14_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":"14_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). doi: 10.1007\/978-3-642-35182-2_26"},{"key":"14_CR26","unstructured":"Le, X.-B., Hobor, A., Lin, A.W.: Decidability and complexity of tree shares formulas. In: FSTTCS (2016)"},{"key":"14_CR27","unstructured":"Le, X.-B., Nguyen, T.-T., Chin, W.-N., Hobor, A.: A certified decision procedure for tree shares (extended) (2017). http:\/\/www.comp.nus.edu.sg\/~lxbach\/certtool\/"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-28891-3_24","volume-title":"NASA Formal Methods","author":"W Meng","year":"2012","unstructured":"Meng, W., He, F., Wang, B.-Y., Liu, Q.: Thread-modular model checking with iterative refinement. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 237\u2013251. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28891-3_24"},{"key":"14_CR29","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). doi: 10.1007\/978-3-662-49122-5_2"},{"key":"14_CR30","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). doi: 10.1007\/978-3-540-69738-1_18"},{"key":"14_CR31","unstructured":"Parkinson, M.: Local reasoning for Java. Ph.D. thesis, University of Cambridge (2005)"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Pippenger, N.: Pure versus impure LISP. In: POPL, pp. 104\u2013109 (1996)","DOI":"10.1145\/237721.237741"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77\u201387 (2015)","DOI":"10.1145\/2737924.2737964"},{"key":"14_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54833-8_9"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390 (2013)","DOI":"10.1145\/2500365.2500600"},{"key":"14_CR36","unstructured":"Villard, J.: Heaps and Hops. Ph.D. thesis, Laboratoire Sp\u00e9cification et V\u00e9rification, \u00c9cole Normale Sup\u00e9rieure de Cachan, France, February 2011"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68690-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T07:26:25Z","timestamp":1570173985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68690-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319686899","9783319686905"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68690-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}