{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:44:53Z","timestamp":1778215493549,"version":"3.51.4"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030993351","type":"print"},{"value":"9783030993368","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if\/while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre\/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_19","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"520-547","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["A Predicate Transformer for Choreographies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4394-8745","authenticated-orcid":false,"given":"Sung-Shik","family":"Jongmans","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petra","family":"van den Bos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Olderog, E.: Fifty years of hoare\u2019s logic. Formal Aspects Comput. 31(6), 751\u2013807 (2019)","DOI":"10.1007\/s00165-019-00501-3"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Baeten, J.C.M., Bravetti, M.: A ground-complete axiomatisation of finite-state processes in a generic process algebra. Mathematical Structures in Computer Science 18(6), 1057\u20131089 (2008)","DOI":"10.1017\/S0960129508007111"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL. pp. 191\u2013202. ACM (2012)","DOI":"10.1145\/2103656.2103680"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: Verification of parallel and concurrent software. In: IFM. Lecture Notes in Computer Science, vol. 10510, pp. 102\u2013110. Springer (2017)","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a06269, pp. 162\u2013176. Springer (2010)","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1-3), 227\u2013270 (2007)","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Carbone, M., Cruz-Filipe, L., Montesi, F., Murawska, A.: Multiparty classical choreographies. In: LOPSTR. Lecture Notes in Computer Science, vol. 11408, pp. 59\u201376. Springer (2018)","DOI":"10.1007\/978-3-030-13838-7_4"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: ESOP. Lecture Notes in Computer Science, vol.\u00a04421, pp. 2\u201317. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_2"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012)","DOI":"10.1145\/2220365.2220367"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL. pp. 263\u2013274. ACM (2013)","DOI":"10.1145\/2429069.2429101"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a08704, pp. 47\u201362. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. Distributed Comput. 31(1), 51\u201367 (2018)","DOI":"10.1007\/s00446-017-0295-1"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science 26(2), 238\u2013302 (2016)","DOI":"10.1017\/S0960129514000188"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: FoSSaCS. Lecture Notes in Computer Science, vol. 10203, pp. 424\u2013440 (2017)","DOI":"10.1007\/978-3-662-54458-7_25"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: Choreographies in practice. In: FORTE. Lecture Notes in Computer Science, vol.\u00a09688, pp. 114\u2013123. Springer (2016)","DOI":"10.1007\/978-3-319-39570-8_8"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. In: FACS. Lecture Notes in Computer Science, vol. 10231, pp. 17\u201335 (2016)","DOI":"10.1007\/978-3-319-57666-4_3"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: Encoding asynchrony in choreographies. In: SAC. pp. 1175\u20131177. ACM (2017)","DOI":"10.1145\/3019612.3019901"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: FORTE. Lecture Notes in Computer Science, vol. 10321, pp. 92\u2013107. Springer (2017)","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38\u201366 (2020)","DOI":"10.1016\/j.tcs.2019.07.005"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Communications in choreographies, revisited. In: SAC. pp. 1248\u20131255. ACM (2018)","DOI":"10.1145\/3167132.3167267"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: ICTAC. Lecture Notes in Computer Science, vol. 12819, pp. 115\u2013133. Springer (2021)","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"19_CR22","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a turing-complete choreographic language in coq. In: ITP. LIPIcs, vol.\u00a0193, pp. 15:1\u201315:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou, P., Yoshida, N.: Dynamic multirole session types. In: POPL. pp. 435\u2013446. ACM (2011)","DOI":"10.1145\/1926385.1926435"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou, P., Yoshida, N.: Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: ICALP (2). Lecture Notes in Computer Science, vol.\u00a07966, pp. 174\u2013186. Springer (2013)","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Logical Methods in Computer Science 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:6)2012"},{"key":"19_CR26","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor. Comput. Sci. 328(1-2), 19\u201337 (2004)","DOI":"10.1016\/j.tcs.2004.07.004"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Giallorenzo, S., Montesi, F., Gabbrielli, M.: Applied choreographies. In: FORTE. Lecture Notes in Computer Science, vol. 10854, pp. 21\u201340. Springer (2018)","DOI":"10.1007\/978-3-319-92612-4_2"},{"key":"19_CR29","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: The choreographic and multitier cases (pearl). In: ECOOP. LIPIcs, vol.\u00a0194, pp. 22:1\u201322:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","DOI":"10.1145\/233551.233556"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Slaats, T., L\u00f3pez, H.A., Debois, S., Carbone, M.: Declarative choreographies and liveness. In: FORTE. Lecture Notes in Computer Science, vol. 11535, pp. 129\u2013147. Springer (2019)","DOI":"10.1007\/978-3-030-21759-4_8"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL), 6:1\u20136:30 (2020)","DOI":"10.1145\/3371074"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Parallel programming: An axiomatic approach. Comput. Lang. 1(2), 151\u2013160 (1976)","DOI":"10.1016\/0096-0551(75)90014-4"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. Lecture Notes in Computer Science, vol.\u00a01381, pp. 122\u2013138. Springer (1998)","DOI":"10.1007\/BFb0053567"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. pp. 273\u2013284. ACM (2008)","DOI":"10.1145\/1328897.1328472"},{"key":"19_CR36","unstructured":"Hurlin, C.: Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. (Sp\u00e9cification et v\u00e9rification de programmes orient\u00e9s objets en logique de s\u00e9paration). Ph.D. thesis, University of Nice Sophia Antipolis, France (2009)"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributive networks. In: FOCS. pp. 150\u2013158. IEEE Computer Society (1981)","DOI":"10.1109\/SFCS.1981.41"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60\u201387 (1990)","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Jongmans, S.S., van\u00a0den Bos, P.: A Predicate Transformer for Choreographies (Full Version). Tech. Rep. OUNL-CS-2022-01, Open University of the Netherlands (2022)","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Jongmans, S.S., van\u00a0den Bos, P.: A Predicate Transformer for Choreographies (Technical Report). Tech. Rep. OUNL-CS-2022-02, Open University of the Netherlands (2022)","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"19_CR41","doi-asserted-by":"crossref","unstructured":"L\u00f3pez, H.A., Marques, E.R.B., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., Yoshida, N.: Protocol-based verification of message-passing parallel programs. In: OOPSLA. pp. 280\u2013298. ACM (2015)","DOI":"10.1145\/2814270.2814302"},{"key":"19_CR42","doi-asserted-by":"crossref","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a08052, pp. 425\u2013439. Springer (2013)","DOI":"10.1007\/978-3-642-40184-8_30"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: CC. pp. 128\u2013138. ACM (2018)","DOI":"10.1145\/3178372.3179495"},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3), 271\u2013307 (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"19_CR45","doi-asserted-by":"crossref","unstructured":"Peleg, D.: Time-optimal leader election in general networks. J. Parallel Distributed Comput. 8(1), 96\u201399 (1990)","DOI":"10.1016\/0743-7315(90)90074-Y"},{"key":"19_CR46","doi-asserted-by":"crossref","unstructured":"Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies - safe runtime updates of distributed applications. In: COORDINATION. Lecture Notes in Computer Science, vol.\u00a09037, pp. 67\u201382. Springer (2015)","DOI":"10.1007\/978-3-319-19282-6_5"},{"key":"19_CR47","unstructured":"Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci. 13(2) (2017)"},{"key":"19_CR48","doi-asserted-by":"crossref","unstructured":"Preda, M.D., Giallorenzo, S., Lanese, I., Mauro, J., Gabbrielli, M.: AIOCJ: A choreographic framework for safe adaptive distributed applications. In: SLE. Lecture Notes in Computer Science, vol.\u00a08706, pp. 161\u2013170. Springer (2014)","DOI":"10.1007\/978-3-319-11245-9_9"},{"key":"19_CR49","doi-asserted-by":"crossref","unstructured":"Rensink, A., Wehrheim, H.: Process algebra with action dependencies. Acta Informatica 38(3), 155\u2013234 (2001)","DOI":"10.1007\/s002360100070"},{"key":"19_CR50","unstructured":"Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)"},{"key":"19_CR51","doi-asserted-by":"crossref","unstructured":"Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90, 61\u201383 (2017)","DOI":"10.1016\/j.jlamp.2016.11.005"},{"key":"19_CR52","doi-asserted-by":"crossref","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148:1\u2013148:30 (2020)","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99336-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:09:36Z","timestamp":1731647376000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_19"}},"subtitle":["Computing Preconditions in Choreographic Programming"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}