{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:39Z","timestamp":1779087699899,"version":"3.51.4"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,3,29]],"date-time":"2024-03-29T00:00:00Z","timestamp":1711670400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that we enrich with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models. We also illustrate how a sound program logic and calculus can be defined for this semantics.<\/jats:p>","DOI":"10.1145\/3648439","type":"journal-article","created":{"date-parts":[[2024,2,16]],"date-time":"2024-02-16T12:38:15Z","timestamp":1708087095000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages"],"prefix":"10.1145","volume":"46","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3588-5609","authenticated-orcid":false,"given":"Crystal Chang","family":"Din","sequence":"first","affiliation":[{"name":"University of Bergen, Bergen, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7137-3523","authenticated-orcid":false,"given":"Ludovic","family":"Henrio","sequence":"additional","affiliation":[{"name":"Univ Lyon, EnsL, UCBL, CNRS, Inria, Lyon, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8763-5548","authenticated-orcid":false,"given":"Violet Ka I","family":"Pun","sequence":"additional","affiliation":[{"name":"Western Norway University of Applied Sciences, Bergen, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9948-2748","authenticated-orcid":false,"given":"S. Lizeth Tapia","family":"Tarifa","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,3,29]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"Abrial Jean-Raymond","year":"1996","unstructured":"Jean-Raymond Abrial. 1996. The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_3_3_2","volume-title":"ABS Documentation (1.9.3 ed.)","year":"2021","unstructured":"ABS Development Team 2021. ABS Documentation (1.9.3 ed.). ABS Development Team. Retrieved from https:\/\/abs-models.org\/manual"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/71.242161"},{"key":"e_1_3_3_5_2","series-title":"LNCS","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","author":"Ahrendt Wolfgang","year":"2016","unstructured":"Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, Vol. 10001. Springer, Cham, Switzerland."},{"issue":"12","key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","article-title":"A system for compositional verification of asynchronous objects","volume":"77","author":"Ahrendt Wolfgang","year":"2012","unstructured":"Wolfgang Ahrendt and Maximilian Dylla. 2012. A system for compositional verification of asynchronous objects. Science of Computer Programming 77, 12 (2012), 1289\u20131309.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_3_7_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlamp.2017.02.003","article-title":"Behavioural semantics for asynchronous components","volume":"89","author":"Ameur-Boulifa Rab\u00e9a","year":"2017","unstructured":"Rab\u00e9a Ameur-Boulifa, Ludovic Henrio, Oleksandra Kulankhina, Eric Madelaine, and A. Savu. 2017. Behavioural semantics for asynchronous components. Journal of Logical and Algebraic Methods in Programming 89 (2017), 1\u201340.","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"e_1_3_3_8_2","first-page":"1","article-title":"Permission-based separation logic for multithreaded Java programs","volume":"11","author":"Amighi Afshin","year":"2015","unstructured":"Afshin Amighi, Christian Haack, Marike Huisman, and Cl\u00e9ment Hurlin. 2015. Permission-based separation logic for multithreaded Java programs. LMCS 11, 1 (2015), 1\u201366.","journal-title":"LMCS"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_3_3_10_2","volume-title":"Multithreading, Parallel, and Concurrent Programming (2nd. ed.)","author":"Andrews Gregory","year":"1999","unstructured":"Gregory Andrews. 1999. Multithreading, Parallel, and Concurrent Programming (2nd. ed.). Addison-Wesley, One Jacob Way, Reading, MA 01867-3999."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5"},{"issue":"3","key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1145\/357103.357110","article-title":"A proof system for communicating sequential processes","volume":"2","author":"Apt Krzysztof R.","year":"1980","unstructured":"Krzysztof R. Apt, Nissim Francez, and Willem P. de Roever. 1980. A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems 2, 3 (1980), 359\u2013385.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Proceedings of the Fundamental Approaches to Software Engineering","volume":"1783","author":"Balser Michael","year":"2000","unstructured":"Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, and Andreas Thums. 2000. Formal system development with KIV. In Proceedings of the Fundamental Approaches to Software Engineering, Tom Maibaum (Ed.). Vol. 1783, Springer, Heidelberg, 363\u2013366."},{"key":"e_1_3_3_14_2","first-page":"315","volume-title":"Proceedings of the 24th International Conference on Automated Deduction","volume":"7898","author":"Beckert Bernhard","year":"2013","unstructured":"Bernhard Beckert and Daniel Bruns. 2013. Dynamic logic with trace semantics. In Proceedings of the 24th International Conference on Automated Deduction, Maria Paola Bonacina (Ed.). Vol. 7898. Springer, Heidelberg, 315\u2013329."},{"key":"e_1_3_3_15_2","volume-title":"Principles of the Spin Model Checker","author":"Ben-Ari Mordechai","year":"2008","unstructured":"Mordechai Ben-Ari. 2008. Principles of the Spin Model Checker. Springer, Heidelberg."},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin Heidelberg."},{"issue":"1","key":"e_1_3_3_17_2","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","article-title":"A semantics for concurrent separation logic","volume":"375","author":"Brookes Stephen","year":"2007","unstructured":"Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science 375, 1\u20133 (2007), 227\u2013270.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","article-title":"Full abstraction for a shared-variable parallel language","volume":"127","author":"Brookes Stephen D.","year":"1996","unstructured":"Stephen D. Brookes. 1996. Full abstraction for a shared-variable parallel language. Information and Computation 127, 2 (1996), 145\u2013163.","journal-title":"Information and Computation"},{"key":"e_1_3_3_19_2","first-page":"466","volume-title":"Proceedings of the 13th International Conference on Concurrency Theory (CONCUR\u201902)","volume":"2421","author":"Brookes Stephen D.","year":"2002","unstructured":"Stephen D. Brookes. 2002. Traces, pomsets, fairness and full abstraction for communicating processes. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR\u201902), Lubos Brim, Petr Jancar, Mojm\u00edr Kret\u00ednsk\u00fd, and Anton\u00edn Kucera (Eds.). Vol. 2421. Springer, Berlin Heidelberg, 466\u2013482."},{"key":"e_1_3_3_20_2","first-page":"303","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Wroclaw, Poland","volume":"9323","author":"Bubel Richard","year":"2015","unstructured":"Richard Bubel, Crystal Chang Din, Reiner H\u00e4hnle, and Keiko Nakata. 2015. A dynamic logic with traces and coinduction. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Wroclaw, Poland, Hans De Nivelle (Ed.). Vol. 9323, Springer, Cham, Switzerland, 303\u2013318."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","unstructured":"Richard Bubel Dilian Gurov Reiner Reiner H\u00e4hnle and Marco Scaletta. 2023. Trace-based Deductive Verification. In Proceedings of 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning (EPiC Series in Computing Vol. 94). 73\u201395. 10.29007\/vdfd","DOI":"10.29007\/vdfd"},{"key":"e_1_3_3_22_2","first-page":"308","volume-title":"Proceedings of the Information Processing\u201974","author":"Burstall Rod M.","year":"1974","unstructured":"Rod M. Burstall. 1974. Program proving as hand simulation with a little induction. In Proceedings of the Information Processing\u201974. Elsevier\/North-Holland, Amsterdam, 308\u2013312."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"issue":"4","key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s004460050018","article-title":"Synchronous, asynchronous, and causally ordered communication","volume":"9","author":"Charron-Bost Bernadette","year":"1996","unstructured":"Bernadette Charron-Bost, Friedemann Mattern, and Gerard Tel. 1996. Synchronous, asynchronous, and causally ordered communication. Distributed Computing 9, 4 (1996), 173\u2013191.","journal-title":"Distributed Computing"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2023. A formal theory of choreographic programming. J. Autom. Reason. 67 2 (2023) 21. 10.1007\/S10817-023-09665-3","DOI":"10.1007\/S10817-023-09665-3"},{"key":"e_1_3_3_26_2","first-page":"57","volume-title":"Proceedings of the Les Fondements de la Programmation","author":"Dahl Ole-Johan","year":"1977","unstructured":"Ole-Johan Dahl. 1977. Can program proving be made practical? In Proceedings of the Les Fondements de la Programmation, M. Amirchahy and D. N\u00e9el (Eds.). Institut de Recherche d\u2019Informatique et d\u2019Automatique, Toulouse, France, 57\u2013114."},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/s10817-009-9119-8","article-title":"Proving fairness and implementation correctness of a microkernel scheduler","volume":"42","author":"Daum Matthias","year":"2009","unstructured":"Matthias Daum, Jan D\u00f6rrenb\u00e4cher, and B. Wolff. 2009. Proving fairness and implementation correctness of a microkernel scheduler. Journal of Automated Reasoning 42, 2\u20134 (2009), 349\u2013388.","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"e_1_3_3_28_2","first-page":"76:1\u201376:39","article-title":"A survey of active object languages","volume":"50","author":"Boer Frank de","year":"2017","unstructured":"Frank de Boer, Crystal Chang Din, Kiko Fernandez-Reyes, Reiner H\u00e4hnle, Ludovic Henrio, Einar Broch Johnsen, Ehsan Khamespanah, Justine Rochas, Vlad Serbanescu, Marjan Sirjani, and Albert Mingkun Yang. 2017. A survey of active object languages. ACM Computing Surveys 50, 5 (2017), 76:1\u201376:39.","journal-title":"ACM Computing Surveys"},{"key":"e_1_3_3_29_2","first-page":"316","volume-title":"Proceedings of the 16th European Symposium on Programming, (ESOP\u201907)","volume":"4421","author":"Boer Frank S. de","year":"2007","unstructured":"Frank S. de Boer, Dave Clarke, and Einar Broch Johnsen. 2007. A complete guide to the future. In Proceedings of the 16th European Symposium on Programming, (ESOP\u201907), Rocco De Nicola (Ed.). Vol. 4421, Springer, Berlin, Heidelberg, 316\u2013330. DOI:10.1007\/978-3-540-71316-6_22"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_3_31_2","first-page":"517","volume-title":"Proceedings of the 25th International Conference on Automated Deduction (CADE), Berlin, Germany","volume":"9195","author":"Din Crystal Chang","year":"2015","unstructured":"Crystal Chang Din, Richard Bubel, and Reiner H\u00e4hnle. 2015. KeY-ABS: A deductive verification tool for the concurrent modelling language ABS. In Proceedings of the 25th International Conference on Automated Deduction (CADE), Berlin, Germany, Amy Felty and Aart Middeldorp (Eds.). Vol. 9195, Springer, Cham, 517\u2013526."},{"issue":"3","key":"e_1_3_3_32_2","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","article-title":"Observable behavior of distributed systems: Component reasoning for concurrent objects","volume":"81","author":"Din Crystal Chang","year":"2012","unstructured":"Crystal Chang Din, Johan Dovland, Einar Broch Johnsen, and Olaf Owe. 2012. Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming 81, 3 (2012), 227\u2013256.","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-319-66902-1_2","volume-title":"Proceedings of the 26th International Conference on Automated Reasoning with Tableaux and Related Methods","volume":"10501","author":"Din Crystal Chang","year":"2017","unstructured":"Crystal Chang Din, Reiner H\u00e4hnle, Einar Broch Johnsen, Violet Ka I Pun, and Silvia Lizeth Tapia Tarifa. 2017. Locally abstract, globally concrete semantics of concurrent programming languages. In Proceedings of the 26th International Conference on Automated Reasoning with Tableaux and Related Methods, Cl\u00e1udia Nalon and Renate Schmidt (Eds.). Vol. 10501, Springer, Cham, Switzerland, 22\u201343."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.03.003"},{"issue":"3","key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","article-title":"Compositional reasoning about active objects with shared futures","volume":"27","author":"Din Crystal Chang","year":"2015","unstructured":"Crystal Chang Din and Olaf Owe. 2015. Compositional reasoning about active objects with shared futures. Formal Aspects of Computing 27, 3 (2015), 551\u2013572.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_3_36_2","first-page":"217","volume-title":"Proceedings of the 17th International Conference on Formal Engineering Methods, ICFEM, Paris","volume":"9407","author":"Din Crystal Chang","year":"2015","unstructured":"Crystal Chang Din, Silvia Lizeth Tapia Tarifa, Reiner H\u00e4hnle, and Einar Broch Johnsen. 2015. History-based specification and verification of scalable concurrent and distributed systems. In Proceedings of the 17th International Conference on Formal Engineering Methods, ICFEM, Paris, Michael Butler, Sylvain Cochon, and Fatiha Za\u00efdi (Eds.). Vol. 9407, Springer, Cham, Switzerland, 217\u2013233."},{"key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1109\/SWSTE.2005.24","volume-title":"Proceedings of the IEEE International Conference on Software Science, Technology and Engineering (SwSTE\u201905)","author":"Dovland Johan","year":"2005","unstructured":"Johan Dovland, Einar Broch Johnsen, and Olaf Owe. 2005. Verification of concurrent objects with asynchronous method calls. In Proceedings of the IEEE International Conference on Software Science, Technology and Engineering (SwSTE\u201905). IEEE Computer Society Press, Los Alamitos, CA, 141\u2013150."},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_3_39_2","first-page":"174","volume-title":"Proceedings of the 24th Symp. on Principles of Programming Languages (POPL\u201997)","author":"Godefroid Patrice","year":"1997","unstructured":"Patrice Godefroid. 1997. Model checking for programming languages using Verisoft. In Proceedings of the 24th Symp. on Principles of Programming Languages (POPL\u201997), Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM, New York, NY, 174\u2013186. DOI:10.1145\/263699.263717"},{"key":"e_1_3_3_40_2","first-page":"24","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, Hyderabad, India","volume":"18","author":"Godefroid Patrice","year":"2012","unstructured":"Patrice Godefroid. 2012. Test generation using symbolic execution. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, Hyderabad, India, Deepak D\u2019Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan (Eds.). Vol. 18, Leibniz-Zentrum fuer Informatik, Schloss Dagstuhl, 24\u201333."},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-40615-7_1","volume-title":"Proceedings of the International School on Formal Models for Components and Objects: Post Proceedings","volume":"7866","author":"H\u00e4hnle Reiner","year":"2013","unstructured":"Reiner H\u00e4hnle. 2013. The abstract behavioral specification language: A tutorial introduction. In Proceedings of the International School on Formal Models for Components and Objects: Post Proceedings, Marcello Bonsangue, Frank de Boer, Elena Giachino, and Reiner H\u00e4hnle (Eds.). Vol. 7866, Springer, Cham, Switzerland, 1\u201337."},{"issue":"2","key":"e_1_3_3_42_2","article-title":"Provably fair cooperative scheduling","volume":"8","author":"H\u00e4hnle Reiner","year":"2023","unstructured":"Reiner H\u00e4hnle and Ludovic Henrio. 2023. Provably fair cooperative scheduling. The Art, Science, and Engineering of Programming 8, 2 (2023). https:\/\/programmingjournal.org\/2024\/8\/issue2\/","journal-title":"The Art, Science, and Engineering of Programming"},{"key":"e_1_3_3_43_2","series-title":"Proceedings of the Computing and Software Science: State of the Art and Perspectives","first-page":"345","volume":"10000","author":"H\u00e4hnle Reiner","year":"2019","unstructured":"Reiner H\u00e4hnle and Marieke Huisman. 2019. Deductive verification: From pen-and-paper proofs to industrial tools. In Proceedings of the Computing and Software Science: State of the Art and Perspectives, Bernhard Steffen and Gerhard Woeginger (Eds.). LNCS, Vol. 10000, Springer, Cham, Switzerland, 345\u2013373."},{"key":"e_1_3_3_44_2","first-page":"278","volume-title":"Proceedings of the Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain","volume":"154","author":"Halpern Joseph Y.","year":"1983","unstructured":"Joseph Y. Halpern, Zohar Manna, and Ben C. Moszkowski. 1983. A hardware semantics based on temporal intervals. In Proceedings of the Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, Josep D\u00edaz (Ed.). Vol. 154, Springer, Berlin, Heidelberg, 278\u2013291. DOI:10.1007\/BFb0036915"},{"key":"e_1_3_3_45_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"Harel David","year":"2000","unstructured":"David Harel, Dexter Kozen, and Jerzy Tiuryn. 2000. Dynamic Logic. MIT Press, Boston, MA, USA."},{"key":"e_1_3_3_46_2","unstructured":"Niklas Heidler. 2022. Mechanization of LAGC semantics in isabelle. bachelor thesis. Technical University of Darmstadt Department of Computer Science. arXiv:2202.08017 [cs.PL]. https:\/\/arxiv.org\/abs\/2202.08017"},{"key":"e_1_3_3_47_2","first-page":"108","volume-title":"Proceedings of the 8th Symposium on the Mathematical Foundations of Computer Science","volume":"74","author":"Hennessy Matthew","year":"1979","unstructured":"Matthew Hennessy and Gordon D. Plotkin. 1979. Full abstraction for a simple parallel programming language. In Proceedings of the 8th Symposium on the Mathematical Foundations of Computer Science, Jir\u00ed Becv\u00e1r (Ed.). Vol. 74, Springer, Heidelberg, 108\u2013120."},{"key":"e_1_3_3_48_2","series-title":"Proceedings of the 8th International Symposium on Formal Methods for Components and Objects (FMCO\u201909)","first-page":"1","author":"Henrio Ludovic","year":"2010","unstructured":"Ludovic Henrio, Florian Kamm\u00fcller, and Muhammad Uzair Khan. 2010. A framework for reasoning on component composition. In Proceedings of the 8th International Symposium on Formal Methods for Components and Objects (FMCO\u201909), Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, and Michael Leuschel (Eds.). Lecture Notes in Computer Science, Springer, Heidelberg, 1\u201320. DOI:10.1007\/978-3-642-17071-3_1"},{"key":"e_1_3_3_49_2","series-title":"Proceedings of the Verification, Model Checking, and Abstract Interpretation","first-page":"315","volume":"7737","author":"Heule Stefan","year":"2013","unstructured":"Stefan Heule, K. Rustan M. Leino, Peter M\u00fcller, and AlexanderJ. Summers. 2013. Abstract read permissions: Fractional permissions without the fractions. In Proceedings of the Verification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). LNCS, Vol. 7737, Springer, Berlin Heidelberg, 315\u2013334. DOI:10.1007\/978-3-642-35873-9_20"},{"key":"e_1_3_3_50_2","first-page":"235","volume-title":"Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA","author":"Hewitt Carl","year":"1973","unstructured":"Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. 1973. A universal modular ACTOR formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, Nils J. Nilsson (Ed.). William Kaufmann, San Francisco, CA, USA, 235\u2013245. Retrieved from http:\/\/ijcai.org\/Proceedings\/73\/Papers\/027B.pdf"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"issue":"10","key":"e_1_3_3_52_2","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare C. A. R.","year":"1969","unstructured":"C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Communications of the ACM 12, 10 (1969), 576\u2013580.","journal-title":"Communications of the ACM"},{"key":"e_1_3_3_53_2","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985","unstructured":"C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_3_3_54_2","volume-title":"The SPIN Model Checker","author":"Holzmann Gerard J.","year":"2003","unstructured":"Gerard J. Holzmann. 2003. The SPIN Model Checker. Pearson Education, Boston, MA, USA."},{"key":"e_1_3_3_55_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed.)","author":"Huth Michael","year":"2004","unstructured":"Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed.). Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_3_56_2","first-page":"137","volume-title":"Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905)","author":"Jacobs Bart","year":"2005","unstructured":"Bart Jacobs, Frank Piessens, K. Rustan M. Leino, and Wolfram Schulte. 2005. Safe concurrency for aggregate objects with invariants. In Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905), Bernhard K. Aichernig and Bernhard Beckert (Eds.). IEEE Computer Society, Los Alamitos, CA, 137\u2013147."},{"issue":"1","key":"e_1_3_3_57_2","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.tcs.2004.10.012","article-title":"A fully abstract may testing semantics for concurrent objects","volume":"338","author":"Jeffrey Alan","year":"2005","unstructured":"Alan Jeffrey and Julian Rathke. 2005. A fully abstract may testing semantics for concurrent objects. Theoretical Computer Science 338, 1-3 (2005), 17\u201363.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_58_2","first-page":"423","volume-title":"Proceedings of the 14th European Symposium on Programming (ESOP\u201905)","volume":"3444","author":"Jeffrey Alan","year":"2005","unstructured":"Alan Jeffrey and Julian Rathke. 2005. Java Jr: Fully abstract trace semantics for a core Java language. In Proceedings of the 14th European Symposium on Programming (ESOP\u201905), Shmuel Sagiv (Ed.). Vol. 3444, Springer, Berlin Heidelberg, 423\u2013438."},{"key":"e_1_3_3_59_2","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Proceedings of the 9th International Symposium on Formal Methods for Components and Objects (FMCO\u201910)","volume":"6957","author":"Johnsen Einar Broch","year":"2011","unstructured":"Einar Broch Johnsen, Reiner H\u00e4hnle, Jan Sch\u00e4fer, Rudolf Schlatte, and Martin Steffen. 2011. ABS: A core language for abstract behavioral specification. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects (FMCO\u201910), Bernhard K. Aichernig, Frank de Boer, and Marcello M. Bonsangue (Eds.). Vol. 6957, Springer, Heidelberg, 142\u2013164."},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.07.001"},{"key":"e_1_3_3_61_2","volume-title":"Development Methods for Computer Programmes Including a Notion of Interference","author":"Jones Cliff B.","year":"1981","unstructured":"Cliff B. Jones. 1981. Development Methods for Computer Programmes Including a Notion of Interference. Ph.D. Dissertation. Oxford University, UK."},{"key":"e_1_3_3_62_2","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-030-29026-9_22","volume-title":"Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX\u201919)","volume":"11714","author":"Kamburjan Eduard","year":"2019","unstructured":"Eduard Kamburjan. 2019. Behavioral program logic. In Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX\u201919), Serenella Cerrito and Andrei Popescu (Eds.). Vol. 11714, Springer, Cham, Switzerland, 391\u2013408. DOI:10.1007\/978-3-030-29026-9_22"},{"key":"e_1_3_3_63_2","volume-title":"Modular Verification of a Modular Specification: Behavioral Types as Program Logics","author":"Kamburjan Eduard","year":"2020","unstructured":"Eduard Kamburjan. 2020. Modular Verification of a Modular Specification: Behavioral Types as Program Logics. Ph.D. Dissertation. Darmstadt University of Technology, Germany. Retrieved from http:\/\/tuprints.ulb.tu-darmstadt.de\/11664\/"},{"key":"e_1_3_3_64_2","series-title":"Proceedings of the Deductive Software Verification: Future Perspectives","first-page":"85","volume":"12345","author":"Kamburjan Eduard","year":"2020","unstructured":"Eduard Kamburjan, Crystal Chang Din, Reiner H\u00e4hnle, and Einar Broch Johnsen. 2020. Behavioral contracts for cooperative scheduling. In Proceedings of the Deductive Software Verification: Future Perspectives, Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, and Mattias Ulbrich (Eds.). LNCS, Vol. 12345, Springer, Cham, 85\u2013121."},{"issue":"7","key":"e_1_3_3_65_2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King James C.","year":"1976","unstructured":"James C. King. 1976. Symbolic execution and program testing. Communications of the ACM 19, 7 (1976), 385\u2013394.","journal-title":"Communications of the ACM"},{"key":"e_1_3_3_66_2","series-title":"Proceedings of the Foundations of Security Analysis and Design V","first-page":"195","volume":"5705","author":"Leino K. Rustan M.","year":"2009","unstructured":"K. Rustan M. Leino, Peter M\u00fcller, and Jan Smans. 2009. Verification of concurrent programs with chalice. In Proceedings of the Foundations of Security Analysis and Design V, Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri (Eds.). LNCS, Vol. 5705, Springer, Berlin Heidelberg, 195\u2013222. DOI:10.1007\/978-3-642-03829-7_7"},{"issue":"10","key":"e_1_3_3_67_2","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","article-title":"Applying \u201cDesign by Contract\u201d","volume":"25","author":"Meyer Bertrand","year":"1992","unstructured":"Bertrand Meyer. 1992. Applying \u201cDesign by Contract\u201d. IEEE Computer 25, 10 (1992), 40\u201351.","journal-title":"IEEE Computer"},{"key":"e_1_3_3_68_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice-Hall, Inc., USA."},{"issue":"4","key":"e_1_3_3_69_2","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","article-title":"Proofs of networks of processes","volume":"7","author":"Misra Jayadev","year":"1981","unstructured":"Jayadev Misra and K. Mani Chandy. 1981. Proofs of networks of processes. IEEE Transactions on Software Engineering 7, 4 (1981), 417\u2013426.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_3_70_2","volume-title":"Foundations for Programming Languages","author":"Mitchell John C.","year":"1996","unstructured":"John C. Mitchell. 1996. Foundations for Programming Languages. MIT Press, Boston, MA, USA."},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.012"},{"key":"e_1_3_3_73_2","series-title":"Proceedings of the Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY","first-page":"177","volume":"12345","author":"Mostowski Wojciech","year":"2020","unstructured":"Wojciech Mostowski. 2020. From explicit to implicit dynamic frames in concurrent reasoning for Java. In Proceedings of the Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, and Mattias Ulbrich (Eds.). LNCS, Vol. 12345, Springer, Cham, 177\u2013203. DOI:10.1007\/978-3-030-64354-6_7"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:1)2015"},{"key":"e_1_3_3_75_2","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer, Berlin Heidelberg."},{"issue":"1","key":"e_1_3_3_76_2","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"O\u2019Hearn Peter W.","year":"2007","unstructured":"Peter W. O\u2019Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science 375, 1-3 (2007), 271\u2013307.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_77_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs I","volume":"6","author":"Owicki Susan S.","year":"1976","unstructured":"Susan S. Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Informatica 6 (1976), 319\u2013340.","journal-title":"Acta Informatica"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.1137\/0214066"},{"key":"e_1_3_3_79_2","first-page":"17","article-title":"A structural approach to operational semantics","volume":"60","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin. 2004. A structural approach to operational semantics. Journal of Logical and Algebraic Methods in Programming 60\u201361 (2004), 17\u2013139.","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"e_1_3_3_80_2","volume-title":"The Pi-Calculus: A Theory of Mobile Processes","author":"Sangiorgi Davide","year":"2001","unstructured":"Davide Sangiorgi and David Walker. 2001. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2652"},{"issue":"3","key":"e_1_3_3_82_2","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logics","volume":"32","author":"Sistla A. Prasad","year":"1985","unstructured":"A. Prasad Sistla and Edmund M. Clarke. 1985. The complexity of propositional linear temporal logics. Journal of the ACM 32, 3 (1985), 733\u2013749.","journal-title":"Journal of the ACM"},{"issue":"4","key":"e_1_3_3_83_2","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1145\/1780.1805","article-title":"Axiomatic semantics of communicating sequential processes","volume":"6","author":"Soundararajan Neelam","year":"1984","unstructured":"Neelam Soundararajan. 1984. Axiomatic semantics of communicating sequential processes. ACM Transactions on Programming Languages and Systems 6, 4 (1984), 647\u2013662.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_3_84_2","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-030-38808-9_8","volume-title":"Proceedings of the 2nd International Workshop on Dynamic Logic: New Trends and Applications","volume":"12005","author":"Steinh\u00f6fel Dominic","year":"2020","unstructured":"Dominic Steinh\u00f6fel and Reiner H\u00e4hnle. 2020. The trace modality. In Proceedings of the 2nd International Workshop on Dynamic Logic: New Trends and Applications, Alexandru Baltag and Luis S. Barbosa (Eds.). Vol. 12005, Springer, Cham, 124\u2013140."},{"key":"e_1_3_3_85_2","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-031-08166-8_23","volume-title":"Proceedings of the Logic of Software. A Tasting Menu of Formal Methods.","author":"Tarifa Silvia Lizeth Tapia","year":"2022","unstructured":"Silvia Lizeth Tapia Tarifa. 2022. Locally abstract globally concrete semantics of time and resource aware active objects. In Proceedings of the Logic of Software. A Tasting Menu of Formal Methods.Springer, Cham, 481\u2013499. DOI:10.1007\/978-3-031-08166-8_23"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.11.002"},{"key":"e_1_3_3_87_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111750"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_3_89_2","volume-title":"Proceedings of the 16th Workshop on Formal Techniques for Java-like Programs (FTfJP\u201914)","author":"Zaharieva-Stojanovski Marina","year":"2014","unstructured":"Marina Zaharieva-Stojanovski, Marieke Huisman, and Stefan Blom. 2014. Verifying functional behaviour of concurrent programs. In Proceedings of the 16th Workshop on Formal Techniques for Java-like Programs (FTfJP\u201914). ACM, New York, NY, USA, Article 4, 6 pages. DOI:10.1145\/2635631.2635849"},{"key":"e_1_3_3_90_2","volume-title":"Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship","author":"Zwiers Job","year":"1989","unstructured":"Job Zwiers. 1989. Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship. Springer, Heidelberg."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648439","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3648439","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:19Z","timestamp":1750287019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,29]]},"references-count":89,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3648439"],"URL":"https:\/\/doi.org\/10.1145\/3648439","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,29]]},"assertion":[{"value":"2022-02-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-12-26","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}