{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T15:53:19Z","timestamp":1778860399333,"version":"3.51.4"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a <jats:italic>projection operator<\/jats:italic>: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is PSPACE-complete. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_17","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"350-373","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Complete Multiparty Session Type Projection with\u00a0Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0173-4498","authenticated-orcid":false,"given":"Elaine","family":"Li","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3638-4096","authenticated-orcid":false,"given":"Felix","family":"Stutz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3197-8736","authenticated-orcid":false,"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"17_CR1","unstructured":"Prototype Implementation of Subset Projection for Multiparty Session Types. https:\/\/gitlab.mpi-sws.org\/fstutz\/async-mpst-gen-choice\/"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aiswarya, C., Atig, M.F.: Data communicating processes with unreliable channels. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, 5\u20138 July 2016, pp. 166\u2013175. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934535","DOI":"10.1145\/2933575.2934535"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"1998","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 305\u2013318. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028754"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theor. Comput. Sci. 331(1), 97\u2013114 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2004.09.034","DOI":"10.1016\/j.tcs.2004.09.034"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR\u201998 Concurrency Theory","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055622"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2-3), 95\u2013230 (2016). https:\/\/doi.org\/10.1561\/2500000031","DOI":"10.1561\/2500000031"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-030-50029-0_6","volume-title":"Coordination Models and Languages","author":"F Barbanera","year":"2020","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 86\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_6"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Barwell, A.D., Scalas, A., Yoshida, N., Zhou, F.: Generalised multiparty session types with crash-stop failures. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, 12\u201316 September 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 35:1\u201335:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.35","DOI":"10.4230\/LIPIcs.CONCUR.2022.35"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, 1\u20134 September 2015. LIPIcs, vol. 42, pp. 283\u2013296. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.283","DOI":"10.4230\/LIPIcs.CONCUR.2015.283"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Bollig, B., Finkel, A., Suresh, A.: Bounded reachability problems are decidable in FIFO machines. In: Konnov, I., Kov\u00e1cs, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020, 1\u20134 September 2020, Vienna, Austria (Virtual Conference). LIPIcs, vol. 171, pp. 49:1\u201349:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.49","DOI":"10.4230\/LIPIcs.CONCUR.2020.49"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983). https:\/\/doi.org\/10.1145\/322374.322380","DOI":"10.1145\/322374.322380"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19\u201351 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2018.02.010","DOI":"10.1016\/j.tcs.2018.02.010"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Log. Methods Comput. Sci. 8(1) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:24)2012","DOI":"10.2168\/LMCS-8(1:24)2012"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"C\u00e9c\u00e9, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166\u2013190 (2005). https:\/\/doi.org\/10.1016\/j.ic.2005.05.006","DOI":"10.1016\/j.ic.2005.05.006"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Charalambides, M., Dinges, P., Agha, G.A.: Parameterized, concurrent session types for asynchronous multi-actor interactions. Sci. Comput. Program. 115-116, 100\u2013126 (2016). https:\/\/doi.org\/10.1016\/j.scico.2015.10.006","DOI":"10.1016\/j.scico.2015.10.006"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:12)2017","DOI":"10.23638\/LMCS-13(2:12)2017"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Chen, T., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Chitil, O., King, A., Danvy, O. (eds.) Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, 8\u201310, September 2014. pp. 135\u2013146. ACM (2014). https:\/\/doi.org\/10.1145\/2643135.2643138","DOI":"10.1145\/2643135.2643138"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-18941-3_4","volume-title":"Formal Methods for Multicore Programming","author":"M Coppo","year":"2015","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146\u2013178. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-18941-3_4"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-78142-2_3","volume-title":"Coordination Models and Languages","author":"F Dagnino","year":"2021","unstructured":"Dagnino, F., Giannini, P., Dezani-Ciancaglini, M.: Deconfined global types for asynchronous sessions. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 41\u201360. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78142-2_3"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-28869-2_10","volume-title":"Programming Languages and Systems","author":"P-M Deni\u00e9lou","year":"2012","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194\u2013213. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_10"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-39212-2_18","volume-title":"Automata, Languages, and Programming","author":"P-M Deni\u00e9lou","year":"2013","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 174\u2013186. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_18"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Deni\u00e9lou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Log. Methods Comput. Sci. 8(4) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(4:6)2012","DOI":"10.2168\/LMCS-8(4:6)2012"},{"key":"17_CR23","unstructured":"Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1\u20133), 147\u2013167 (2007). http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi80-1-3-09"},{"key":"17_CR24","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, 7\u201312 January 2008, pp. 273\u2013284. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Keizer, A.C., Basold, H., P\u00e9rez, J.A.: Session coalgebras: a coalgebraic view on regular and context-free session types. ACM Trans. Program. Lang. Syst. 44(3), 18:1\u201318:45 (2022). https:\/\/doi.org\/10.1145\/3527633","DOI":"10.1145\/3527633"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563","DOI":"10.1145\/359545.359563"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-662-54458-7_26","volume-title":"Foundations of Software Science and Computation Structures","author":"J Lange","year":"2017","unstructured":"Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441\u2013457. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_26"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-25540-4_6","volume-title":"Computer Aided Verification","author":"J Lange","year":"2019","unstructured":"Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 97\u2013117. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_6"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Li, E., Stutz, F., Wies, T., Zufferey, D.: Complete multiparty session type projection with automata. CoRR abs\/2305.17079 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.17079","DOI":"10.48550\/arXiv.2305.17079"},{"key":"17_CR30","doi-asserted-by":"publisher","unstructured":"Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1-3), 529\u2013554 (2003). https:\/\/doi.org\/10.1016\/j.tcs.2003.08.002","DOI":"10.1016\/j.tcs.2003.08.002"},{"key":"17_CR31","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Mukund, M., Stutz, F., Zufferey, D.: Generalising projection in asynchronous multiparty session types. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, 24\u201327 August 2021, Virtual Conference. LIPIcs, vol. 203, pp. 35:1\u201335:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.35","DOI":"10.4230\/LIPIcs.CONCUR.2021.35"},{"key":"17_CR32","doi-asserted-by":"publisher","unstructured":"Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. 13(5), 685\u2013719 (2003). https:\/\/doi.org\/10.1017\/S0960129503004043","DOI":"10.1017\/S0960129503004043"},{"key":"17_CR33","doi-asserted-by":"publisher","unstructured":"Peng, W., Purushothaman, S.: Analysis of a class of communicating finite state machines. Acta Informatica 29(6\/7), 499\u2013522 (1992). https:\/\/doi.org\/10.1007\/BF01185558","DOI":"10.1007\/BF01185558"},{"key":"17_CR34","doi-asserted-by":"publisher","unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: M\u00fcller, P. (ed.) 31st European Conference on Object-Oriented Programming, ECOOP 2017, 19\u201323 June 2017, Barcelona, Spain. LIPIcs, vol. 74, pp. 24:1\u201324:31. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.24","DOI":"10.4230\/LIPIcs.ECOOP.2017.24"},{"key":"17_CR35","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Mpstk: the multiparty session types toolkit (2018). https:\/\/doi.org\/10.1145\/3291638","DOI":"10.1145\/3291638"},{"key":"17_CR36","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1\u201330:29 (2019). https:\/\/doi.org\/10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"17_CR37","doi-asserted-by":"publisher","unstructured":"Stutz, F.: Artifact for \u201cComplete Multiparty Session Type Projection with Automata\u201d, April 2023. https:\/\/doi.org\/10.5281\/zenodo.7878493","DOI":"10.5281\/zenodo.7878493"},{"key":"17_CR38","unstructured":"Stutz, F.: Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In: 37th European Conference on Object-Oriented Programming, ECOOP 2023. LIPIcs (2023). https:\/\/arxiv.org\/pdf\/2302.11272.pdf"},{"key":"17_CR39","doi-asserted-by":"publisher","unstructured":"Stutz, F., Zufferey, D.: Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types. In: Ganty, P., Monica, D.D. (eds.) Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, 21\u201323 September 2022. EPTCS, vol. 370, pp. 194\u2013212 (2022). https:\/\/doi.org\/10.4204\/EPTCS.370.13","DOI":"10.4204\/EPTCS.370.13"},{"key":"17_CR40","doi-asserted-by":"publisher","unstructured":"Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 18\u201322 September 2016, pp. 462\u2013475. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951926","DOI":"10.1145\/2951913.2951926"},{"key":"17_CR41","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.jlamp.2016.11.005"},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-78800-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S La Torre","year":"2008","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299\u2013314. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_21"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"Viering, M., Hu, R., Eugster, P., Ziarek, L.: A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3485501","DOI":"10.1145\/3485501"},{"key":"17_CR44","unstructured":"Wehar, M.: On the complexity of intersection non-emptiness problems. Ph.D. thesis, University of Buffalo (2016)"},{"key":"17_CR45","unstructured":"Spring and Hibernate Transaction in Java. https:\/\/www.uml-diagrams.org\/examples\/spring-hibernate-transaction-sequence-diagram-example.html"}],"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-37709-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:03:36Z","timestamp":1689501816000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"261","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":"67","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":"26% - 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","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":"11","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)"}}]}}