Sprout: A Verifier for Symbolic Multiparty Protocols

Benchmark suites; Correctness properties; Fixpoints; Functional correctness; Implementability; Multi-party communication; Multi-party protocols; Sound and complete; Theoretical Computer Science; Computer Science (all)

Abstract :

[en] We present Sprout, the first sound and complete implementability checker for symbolic multiparty protocols. Sprout supports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice. Sprout checks implementability via an optimized, sound and complete reduction to the fixpoint logic μCLP, and uses MuVal as a backend solver for μCLP instances. We evaluate Sprout on an extended benchmark suite of implementable and non-implementable examples, and show that Sprout outperforms its competititors in terms of expressivity and precision, and provides competitive runtime performance. Sprout additionally provides support for verifying custom functional correctness properties beyond implementability.

Disciplines :

Computer science

Author, co-author :

Li, Elaine ; New York University, New York, United States

STUTZ, Felix ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

Wies, Thomas ; New York University, New York, United States

Zufferey, Damien ; NVIDIA, Zürich, Switzerland

External co-authors :

yes

Language :

English

Title :

Sprout: A Verifier for Symbolic Multiparty Protocols

Publication date :

2025

Event name :

37th International Conference on Computer Aided Verification

Event place :

Zagreb, Croatia

Event date :

23-07-2025 => 25-07-2025

Main work title :

Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings

Editor :

Piskac, Ruzica

Publisher :

Springer Science and Business Media Deutschland GmbH

ISBN/EAN :

978-3-03-198681-9

Peer reviewed :

Peer reviewed

Additional URL :

https://link.springer.com/content/pdf/10.1007/978-3-031-98682-6_16

FnR Project :

C22/IS/17238244/AVVA

Funders :

NSF - National Science Foundation
FNR - Fonds National de la Recherche Luxembourg

Available on ORBilu :

since 28 January 2026

Statistics

Number of views

4 (0 by Unilu)

Number of downloads

1 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

WoS citations^™

Bibliography

Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. IEEE Trans. Software Eng. 29(7), 623–633 (2003). https://doi.org/10.1109/TSE.2003.1214326, https://doi.org/10.1109/TSE.2003.1214326
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR ’99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1664, pp. 114–129. Springer (1999). https://doi.org/10.1007/3-540-48320-9_10, https://doi. org/10.1007/3-540-48320-9_10
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-8, 2012, Revised Selected Papers. Lecture Notes in Computer Science, vol. 8191, pp. 97–111. Springer (2012). https://doi.org/10.1007/978-3-642-41157-1_7, https://doi.org/10.1007/978-3-642-41157-1_7
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-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6269, pp. 162–176. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_12, https://doi.org/10.1007/978-3-642-15375-4_12
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-29, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13572, pp. 212–237. Springer (2022). https://doi.org/10.1007/978-3-031-17715-6_15, https://doi.org/10.1007/978-3-031-17715-6_15
Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38–66 (2020). https://doi.org/10.1016/j.tcs.2019.07.005, https://doi.org/10.1016/j.tcs.2019.07.005
Gazagnaire, T., Genest, B., Hélouët, 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-8, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4703, pp. 166–180. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_ 12, https://doi.org/10.1007/978-3-540-74407-8_12
Genest, B., Muscholl, A.: Message sequence charts: A survey. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 6-9 June 2005, St. Malo, France. pp. 2–4. IEEE Computer Society (2005). https://doi.org/10.1109/ACSD.2005.25, https://doi.org/10.1109/ACSD.2005.25
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ätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned]. Lecture Notes in Computer Science, vol. 3098, pp. 537– 558. Springer (2003). https://doi.org/10.1007/978-3-540-27755-2_15, https://doi.org/10.1007/978-3-540-27755-2_15
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infnite-state high-level MSCs: Model-checking and realizability. J. Comput. Syst. Sci. 72(4), 617–647 (2006). https://doi.org/10.1016/j.jcss.2005.09.007, https://doi.org/10.1016/j. jcss.2005.09.007
Gheri, L., Lanese, I., Sayers, N., Tuosto, E., Yoshida, N.: Design-by-contract for fexible 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. 222, pp. 8:1–8:28. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.ECOOP.2022.8, https://doi.org/10.4230/LIPIcs.ECOOP.2022.8
Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisen-burger, P.: Multiparty languages: The choreographic and multitier cases (pearl). In: Møller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Con-ference). LIPIcs, vol. 194, pp. 22:1–22:27. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.ECOOP.2021.22, https://doi.org/10.4230/LIPIcs.ECOOP.2021.22
Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1–27 (2022). https://doi.org/10.1145/3498684, https://doi.org/10.1145/3498684
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-12, 2008. pp. 273–284. ACM (2008). https://doi. org/10.1145/1328438.1328472, https://doi.org/10.1145/1328438.1328472
Li, E.: Sprout: A verifer for symbolic multiparty protocols (CAV’25 AE) (Apr 2025). https://doi.org/10.5281/zenodo.15313597, https://doi.org/10.5281/zenodo.15313597
Li, E., Stutz, F., Wies, T., Zuferey, D.: Complete multiparty session type projection with automata. In: Enea, C., Lal, A. (eds.) Computer Aided Verifcation-35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 350– 373. Springer (2023). https://doi.org/10.1007/978-3-031-37709-9_17, https://doi.org/10.1007/978-3-031-37709-9_17
Li, E., Stutz, F., Wies, T., Zuferey, D.: Characterizing implementability of global protocols with infnite states and data. Proc. ACM Program. Lang. 9(OOPSLA1), 1434–1463 (2025). https://doi.org/10.1145/3720493, https://doi.org/10.1145/3720493
Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1-3), 529–554 (2003). https://doi.org/10.1016/J.TCS. 2003.08.002, https://doi.org/10.1016/j.tcs.2003.08.002
Mauw, S., Reniers, M.A.: High-level message sequence charts. In: Cavalli, A.R., Sarma, A. (eds.) SDL ’97 Time for Testing, SDL, MSC and Trends-8th International SDL Forum, Evry, France, 23-29 September 1997, Proceedings. pp. 291–306. Elsevier (1997)
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-16, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2285, pp. 523–534. Springer (2002). https://doi. org/10.1007/3-540-45841-7_43, https://doi.org/10.1007/3-540-45841-7_43
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’99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1672, pp. 81–91. Springer (1999). https://doi. org/10.1007/3-540-48340-3_8, https://doi.org/10.1007/3-540-48340-3_8
Roychoudhury, A., Goel, A., Sengupta, B.: Symbolic message sequence charts. ACM Trans. Softw. Eng. Methodol. 21(2), 12:1–12:44 (2012). https://doi.org/10.1145/2089116.2089122, https://doi.org/10.1145/2089116.2089122
Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90, 61–83 (2017). https://doi.org/10.1016/J.JLAMP. 2016.11.005, https://doi.org/10.1016/j.jlamp.2016.11.005
Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fxpoint logic solving for temporal verifcation. Proc. ACM Program. Lang. 7(POPL), 2111–2140 (2023). https://doi.org/10.1145/3571265, https://doi.org/10.1145/3571265
Vassor, M., Yoshida, N.: Refnements for multiparty message-passing protocols: Specifcation-agnostic theory and implementation. In: Aldrich, J., Salvaneschi, G. (eds.) 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria. LIPIcs, vol. 313, pp. 41:1–41:29. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPICS.ECOOP.2024.41, https://doi.org/10.4230/LIPIcs.ECOOP.2024.41
Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verifed refnements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148:1– 148:30 (2020). https://doi.org/10.1145/3428216, https://doi.org/10.1145/3428216