{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:31:56Z","timestamp":1758709916345,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"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-66902-1_2","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T07:34:20Z","timestamp":1503992060000},"page":"22-43","source":"Crossref","is-referenced-by-count":13,"title":["Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages"],"prefix":"10.1007","author":[{"given":"Crystal Chang","family":"Din","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ka I","family":"Pun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvia Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"issue":"10","key":"2_CR1","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). (583)","journal-title":"Commun. ACM"},{"key":"2_CR2","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle (1976)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification\u2013The KeY Book: From Theory to Practice","author":"B Beckert","year":"2016","unstructured":"Beckert, B., Klebanov, V., Wei\u00df, B.: Dynamic logic for Java. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M. (eds.) Deductive Software Verification\u2013The KeY Book: From Theory to Practice. LNCS, vol. 10001, pp. 49\u2013106. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-319-49812-6"},{"key":"2_CR4","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algebraic Program."},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-48737-9_2","volume-title":"Formal Syntax and Semantics of Java","author":"S Drossopoulou","year":"1999","unstructured":"Drossopoulou, S., Eisenbach, S.: Describing the semantics of Java and proving type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 41\u201382. Springer, Heidelberg (1999)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Wiedijk, F.: A typed C11 semantics for interactive theorem proving. In: Conference on Certified Programs and Proofs, 15\u201327. ACM (2015)","DOI":"10.1145\/2676724.2693571"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"9th International Symposium on Formal Methods for Components and Objects (FMCO 2010)","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), vol. 6957, pp. 142\u2013164. Springer, Berlin (2011). doi:\n10.1007\/978-3-642-25271-6_8"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"19th International Conference on Computer Aided Verification, CAV 2007","author":"JC Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification, CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Berlin (2007). doi:\n10.1007\/978-3-540-73368-3_21"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-17511-4_20"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/3-540-45694-5_31","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"S Brookes","year":"2002","unstructured":"Brookes, S.: Traces, pomsets, fairness and full abstraction for communicating processes. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 466\u2013482. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45694-5_31"},{"issue":"10","key":"2_CR11","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \"design by contract\". IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"2_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.L.: Principles of Program Analysis. Springer, Heidelberg (1999). doi:\n10.1007\/978-3-662-03811-6"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-09099-3_7","volume-title":"Tests and Proofs","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82\u201398. Springer, Cham (2014). doi:\n10.1007\/978-3-319-09099-3_7"},{"issue":"1","key":"2_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-11(1:1)2015","volume":"11","author":"K Nakata","year":"2015","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1), 1\u201332 (2015)","journal-title":"Log. Methods Comput. Sci."},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-71316-6_22","volume-title":"Programming Languages and Systems","author":"FS Boer","year":"2007","unstructured":"Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316\u2013330. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-71316-6_22"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 517\u2013526. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21401-6_35"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24312-2_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Bubel","year":"2015","unstructured":"Bubel, R., Din, C.C., H\u00e4hnle, R., Nakata, K.: A dynamic logic with traces and coinduction. In: Nivelle, H. (ed.) TABLEAUX 2015. LNCS, vol. 9323, pp. 307\u2013322. Springer, Cham (2015). doi:\n10.1007\/978-3-319-24312-2_21"},{"issue":"3","key":"2_CR18","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","volume":"81","author":"CC Din","year":"2012","unstructured":"Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Logic Algebraic Program. 81(3), 227\u2013256 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"3","key":"2_CR19","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Asp. Comput. 27(3), 551\u2013572 (2015)","journal-title":"Formal Asp. Comput."},{"key":"2_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlamp.2017.02.003","volume":"89","author":"R Ameur-Boulifa","year":"2017","unstructured":"Ameur-Boulifa, R., Henrio, L., Kulankhina, O., Madelaine, E., Savu, A.: Behavioural semantics for asynchronous components. J. Logical Algebraic Methods Program. 89, 1\u201340 (2017)","journal-title":"J. Logical Algebraic Methods Program."},{"issue":"1\u20133","key":"2_CR21","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66902-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,14]],"date-time":"2017-11-14T05:49:18Z","timestamp":1510638558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}