{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T09:13:09Z","timestamp":1746522789805,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"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><jats:p>Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (communication deadlock freedom) of implementations relative to specifications. Discourje is an existing run-time verification library for communication protocols in Clojure, based on dynamic MPST. The original version of Discourje can detect only safety violations. In this paper, we present an extension of Discourje to detect also liveness violations.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_11","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"158-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Discourje: Run-Time Verification of\u00a0Communication Protocols in\u00a0Clojure \u2014 Live at\u00a0Last"],"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"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"issue":"2\u20133","key":"11_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: FMCO. LNCS, vol.\u00a04111 (2005)","DOI":"10.1007\/11804192_17"},{"key":"11_CR3","unstructured":"Barwell, A.D., Hou, P., Yoshida, N., Zhou, F.: Designing asynchronous multiparty protocols with crash-stop failures. In: ECOOP. LIPIcs, vol.\u00a0263, pp. 1:1\u20131:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.tcs.2017.02.009","volume":"669","author":"L Bocchi","year":"2017","unstructured":"Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33\u201358 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bonnaire-Sergeant, A., Davies, R., Tobin-Hochstadt, S.: Practical optional types for Clojure. In: ESOP. LNCS, vol.\u00a09632 (2016)","DOI":"10.1007\/978-3-662-49498-1_4"},{"issue":"3","key":"11_CR6","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF01782773","volume":"2","author":"G Bracha","year":"1987","unstructured":"Bracha, G., Toueg, S.: Distributed deadlock detection. Distributed Comput. 2(3), 127\u2013138 (1987)","journal-title":"Distributed Comput."},{"key":"11_CR7","unstructured":"Burl\u00f2, C.B., Francalanza, A., Scalas, A.: On the monitorability of session types, in theory and practice. In: ECOOP. LIPIcs, vol.\u00a0194, pp. 20:1\u201320:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"102847","DOI":"10.1016\/j.scico.2022.102847","volume":"222","author":"CB Burl\u00f2","year":"2022","unstructured":"Burl\u00f2, C.B., Francalanza, A., Scalas, A., Trubiani, C., Tuosto, E.: PSTMonitor: monitor synthesis from probabilistic session types. Sci. Comput. Program. 222, 102847 (2022)","journal-title":"Sci. Comput. Program."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Castro, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in Go: statically-typed endpoint APIs for dynamically-instantiated communication structures. PACMPL 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290342"},{"key":"11_CR10","unstructured":"Cledou, G., Edixhoven, L., Jongmans, S., Proen\u00e7a, J.: API generation for multiparty session types, revisited and revised using Scala 3. In: ECOOP. LIPIcs, vol.\u00a0222 (2022)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Ferreira, F., Jongmans, S.: Oven: Safe and live communication protocols in Scala, using synthetic behavioural type analysis. In: ISSTA, pp. 1511\u20131514. ACM (2023)","DOI":"10.1145\/3597926.3604926"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"100731","DOI":"10.1016\/j.jlamp.2021.100731","volume":"124","author":"H Gommerstadt","year":"2022","unstructured":"Gommerstadt, H., Jia, L., Pfenning, F.: Session-typed concurrent contracts. J. Log. Algebraic Methods Program. 124, 100731 (2022)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Hamers, R., Jongmans, S.: Discourje: runtime verification of communication protocols in Clojure. In: TACAS (1). LNCS, vol. 12078 (2020)","DOI":"10.26226\/morressier.604907f51a80aac83ca25d9e"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/978-3-030-61362-4_28","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"R Hamers","year":"2020","unstructured":"Hamers, R., Jongmans, S.-S.: Safe sessions of channel actions in clojure: a tour of the discourje project. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 489\u2013508. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_28"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"van\u00a0den Heuvel, B., P\u00e9rez, J.A., Dobre, R.A.: Monitoring blackbox implementations of multiparty session protocols. In: RV. Lecture Notes in Computer Science, vol. 14245, pp. 66\u201385. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_4","DOI":"10.1007\/978-3-031-44267-4_4"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Hilbrich, T., de\u00a0Supinski, B.R., Nagel, W.E., Protze, J., Baier, C., M\u00fcller, M.S.: Distributed wait state tracking for runtime MPI deadlock detection. In: SC, pp. 16:1\u201316:12. ACM (2013)","DOI":"10.1145\/2503210.2503237"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL (2008)","DOI":"10.1145\/1328438.1328472"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Horlings, E., Jongmans, S.: Analysis of specifications of multiparty sessions with dcj-lint. In: ESEC\/SIGSOFT FSE, pp. 1590\u20131594. ACM (2021)","DOI":"10.1145\/3468264.3473127"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: FASE. LNCS, vol.\u00a09633 (2016)","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: FASE. LNCS, vol. 10202 (2017)","DOI":"10.1007\/978-3-662-54494-5_7"},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 1\u201336 (2016)","journal-title":"ACM Comput. Surv."},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Imai, K., Neykova, R., Yoshida, N., Yuen, S.: Multiparty session programming with global protocol combinators. In: ECOOP. LIPIcs, vol.\u00a0166 (2020)","DOI":"10.4204\/EPTCS.322.3"},{"key":"11_CR23","unstructured":"Jongmans, S.S.: Discourje: run-time verification of communication protocols in clojure \u2013 Live at last. Technical report (2023). https:\/\/arxiv.org\/abs\/2407.00540"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Jongmans, S.: Discourje: run-time verification of communication protocols in Clojure \u2013 live at last (artifact) (2024). https:\/\/doi.org\/10.5281\/zenodo.12519843","DOI":"10.5281\/zenodo.12519843"},{"issue":"2","key":"11_CR25","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s007780050075","volume":"8","author":"N Krivokapic","year":"1999","unstructured":"Krivokapic, N., Kemper, A., Gudes, E.: Deadlock detection in distributed database systems: a new algorithm and a comparative performance analysis. VLDB J. 8(2), 79\u2013100 (1999)","journal-title":"VLDB J."},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Lagaillardie, N., Neykova, R., Yoshida, N.: Implementing multiparty session types in rust. In: COORDINATION. LNCS, vol. 12134 (2020)","DOI":"10.1007\/978-3-030-50029-0_8"},{"key":"11_CR27","unstructured":"Lagaillardie, N., Neykova, R., Yoshida, N.: Stay safe under panic: affine Rust programming with multiparty session types. In: ECOOP. LIPIcs, vol.\u00a0222 (2022)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Melgratti, H.C., Padovani, L.: Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang. 1(ICFP), 1\u201329 (2017)","DOI":"10.1145\/3110279"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Miu, A., Ferreira, F., Yoshida, N., Zhou, F.: Communication-safe web programming in TypeScript with routed multiparty session types. In: CC (2021)","DOI":"10.1145\/3446804.3446854"},{"issue":"5","key":"11_CR30","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1007\/s00165-017-0420-8","volume":"29","author":"R Neykova","year":"2017","unstructured":"Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Asp. Comput. 29(5), 877\u2013910 (2017)","journal-title":"Formal Asp. Comput."},{"key":"11_CR31","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 (2018)","DOI":"10.1145\/3178372.3179495"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC (2017)","DOI":"10.1145\/3033019.3033031"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Pinzaru, G., Rivera, V.: Towards static verification of Clojure contract-based programs. In: TOOLS. LNCS, vol. 11771 (2019)","DOI":"10.1007\/978-3-030-29852-4_5"},{"key":"11_CR34","unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP. LIPIcs, vol.\u00a074 (2017)"},{"issue":"4","key":"11_CR35","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10619-011-7078-7","volume":"29","author":"S Srinivasan","year":"2011","unstructured":"Srinivasan, S., Rajaram, R.: A decentralized deadlock detection and resolution algorithm for generalized model in distributed systems. Distrib. Parallel Databases 29(4), 261\u2013276 (2011)","journal-title":"Distrib. Parallel Databases"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in Go. In: ASPLOS (2019)","DOI":"10.1145\/3297858.3304069"},{"key":"11_CR37","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), 1\u201330 (2020)","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:12:22Z","timestamp":1726121542000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has 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":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}