{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T11:16:29Z","timestamp":1783509389670,"version":"3.55.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present\n                    <jats:sc>Sprout<\/jats:sc>\n                    , the first sound and complete implementability checker for symbolic multiparty protocols.\n                    <jats:sc>Sprout<\/jats:sc>\n                    supports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice.\n                    <jats:sc>Sprout<\/jats:sc>\n                    checks implementability via an optimized, sound and complete reduction to the fixpoint logic\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03bc<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    CLP, and uses\n                    <jats:sc>MuVal<\/jats:sc>\n                    as a backend solver for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03bc<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    CLP instances. We evaluate\n                    <jats:sc>Sprout<\/jats:sc>\n                    on an extended benchmark suite of implementable and non-implementable examples, and show that\n                    <jats:sc>Sprout<\/jats:sc>\n                    outperforms its competititors in terms of expressivity and precision, and provides competitive runtime performance.\n                    <jats:sc>Sprout<\/jats:sc>\n                    additionally provides support for verifying custom functional correctness properties beyond implementability.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_16","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:15:06Z","timestamp":1753154106000},"page":"304-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Sprout: A Verifier for\u00a0Symbolic Multiparty Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0173-4498","authenticated-orcid":false,"given":"Elaine","family":"Li","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3638-4096","authenticated-orcid":false,"given":"Felix","family":"Stutz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3197-8736","authenticated-orcid":false,"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"issue":"7","key":"16_CR1","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1109\/TSE.2003.1214326","volume":"29","author":"R Alur","year":"2003","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. IEEE Trans. Software Eng. 29(7), 623\u2013633 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1214326","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24\u201327, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01664, pp. 114\u2013129. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_10","DOI":"10.1007\/3-540-48320-9_10"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Bocchi, L., Demangeon, R., Yoshida, N.: A multiparty multi-session logic. In: Palamidessi, C., Ryan, M.D. (eds.) Trustworthy Global Computing - 7th International Symposium, TGC 2012, Newcastle upon Tyne, UK, September 7\u20138, 2012, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a08191, pp. 97\u2013111. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-41157-1_7","DOI":"10.1007\/978-3-642-41157-1_7"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31\u2013September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06269, pp. 162\u2013176. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Graversen, E., Lugovic, L., Montesi, F., Peressotti, M.: Functional choreographic programming. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27\u201329, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13572, pp. 212\u2013237. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_15","DOI":"10.1007\/978-3-031-17715-6_15"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.tcs.2019.07.005","volume":"802","author":"L Cruz-Filipe","year":"2020","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38\u201366 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.07.005","journal-title":"Theor. Comput. Sci."},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Gazagnaire, T., Genest, B., H\u00e9lou\u00ebt, L., Thiagarajan, P.S., Yang, S.: Causal message sequence charts. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3\u20138, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04703, pp. 166\u2013180. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_12","DOI":"10.1007\/978-3-540-74407-8_12"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Genest, B., Muscholl, A.: Message sequence charts: a survey. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 6\u20139 June 2005, St. Malo, France, pp.\u00a02\u20134. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/ACSD.2005.25","DOI":"10.1109\/ACSD.2005.25"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Genest, B., Muscholl, A., Peled, D.A.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichst\u00e4tt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned]. Lecture Notes in Computer Science, vol.\u00a03098, pp. 537\u2013558. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_15","DOI":"10.1007\/978-3-540-27755-2_15"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1016\/j.jcss.2005.09.007","volume":"72","author":"B Genest","year":"2006","unstructured":"Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level MSCs: model-checking and realizability. J. Comput. Syst. Sci. 72(4), 617\u2013647 (2006). https:\/\/doi.org\/10.1016\/j.jcss.2005.09.007","journal-title":"J. Comput. Syst. Sci."},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Gheri, L., Lanese, I., Sayers, N., Tuosto, E., Yoshida, N.: Design-by-contract for flexible multiparty session protocols. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany. LIPIcs, vol.\u00a0222, pp. 8:1\u20138:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2022.8","DOI":"10.4230\/LIPICS.ECOOP.2022.8"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: the choreographic and multitier cases (pearl). In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11\u201317, 2021, Aarhus, Denmark (Virtual Conference). LIPIcs, vol.\u00a0194, pp. 22:1\u201322:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.22","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022). https:\/\/doi.org\/10.1145\/3498684","DOI":"10.1145\/3498684"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008, pp. 273\u2013284. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Li, E.: Sprout: a verifier for symbolic multiparty protocols (CAV 2025 AE) (2025). https:\/\/doi.org\/10.5281\/zenodo.15313597","DOI":"10.5281\/zenodo.15313597"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Li, E., Stutz, F., Wies, T., Zufferey, D.: Complete multiparty session type projection with automata. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 350\u2013373. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_17","DOI":"10.1007\/978-3-031-37709-9_17"},{"issue":"OOPSLA1","key":"16_CR17","doi-asserted-by":"publisher","first-page":"1434","DOI":"10.1145\/3720493","volume":"9","author":"E Li","year":"2025","unstructured":"Li, E., Stutz, F., Wies, T., Zufferey, D.: Characterizing implementability of global protocols with infinite states and data. Proc. ACM Program. Lang. 9(OOPSLA1), 1434\u20131463 (2025). https:\/\/doi.org\/10.1145\/3720493","journal-title":"Proc. ACM Program. Lang."},{"issue":"1\u20133","key":"16_CR18","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1016\/J.TCS.2003.08.002","volume":"309","author":"M Lohrey","year":"2003","unstructured":"Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1\u20133), 529\u2013554 (2003). https:\/\/doi.org\/10.1016\/J.TCS.2003.08.002","journal-title":"Theor. Comput. Sci."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Mauw, S., Reniers, M.A.: High-level message sequence charts. In: Cavalli, A.R., Sarma, A. (eds.) SDL 1997 Time for Testing, SDL, MSC and Trends - 8th International SDL Forum, Evry, France, 23\u201329 September 1997, Proceedings, pp. 291\u2013306. Elsevier (1997)","DOI":"10.1016\/B978-044482816-3\/50020-4"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Morin, R.: Recognizable sets of message sequence charts. In: Alt, H., Ferreira, A. (eds.) STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes - Juan les Pins, France, March 14\u201316, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02285, pp. 523\u2013534. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45841-7_43","DOI":"10.1007\/3-540-45841-7_43"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Muscholl, A., Peled, D.A.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kutylowski, M., Pacholski, L., Wierzbicki, T. (eds.) Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS 1999, Szklarska Poreba, Poland, September 6\u201310, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01672, pp. 81\u201391. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48340-3_8","DOI":"10.1007\/3-540-48340-3_8"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Roychoudhury, A., Goel, A., Sengupta, B.: Symbolic message sequence charts. ACM Trans. Softw. Eng. Methodol. 21(2), 12:1\u201312:44 (2012). https:\/\/doi.org\/10.1145\/2089116.2089122","DOI":"10.1145\/2089116.2089122"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/J.JLAMP.2016.11.005","volume":"90","author":"B Toninho","year":"2017","unstructured":"Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90, 61\u201383 (2017). https:\/\/doi.org\/10.1016\/J.JLAMP.2016.11.005","journal-title":"J. Log. Algebraic Methods Program."},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang. 7(POPL), 2111\u20132140 (2023). https:\/\/doi.org\/10.1145\/3571265","DOI":"10.1145\/3571265"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Vassor, M., Yoshida, N.: Refinements for multiparty message-passing protocols: specification-agnostic theory and implementation. In: Aldrich, J., Salvaneschi, G. (eds.) 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16\u201320, 2024, Vienna, Austria. LIPIcs, vol.\u00a0313, pp. 41:1\u201341:29. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2024.41","DOI":"10.4230\/LIPICS.ECOOP.2024.41"},{"key":"16_CR26","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3428216","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:32:07Z","timestamp":1783506727000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}