Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last

Sung Shik Jongmans

doi:10.1007/978-3-031-71177-0_11

Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last

Sung Shik Jongmans^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Formal Methods - 26th International Symposium, FM 2024, Proceedings
Editors	Andre Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	158-166
Number of pages	9
ISBN (Print)	9783031711763
DOIs	https://doi.org/10.1007/978-3-031-71177-0_11
Publication status	Published - 2025
Event	26th International Symposium on Formal Methods - Milan, Italy Duration: 9 Sept 2024 → 13 Sept 2024 Conference number: 26 https://www.fm24.polimi.it/

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14934 LNCS
ISSN	0302-9743

Conference

Conference	26th International Symposium on Formal Methods
Abbreviated title	FM 2024
Country/Territory	Italy
City	Milan
Period	9/09/24 → 13/09/24
Internet address	https://www.fm24.polimi.it/

Access to Document

10.1007/978-3-031-71177-0_11Licence: CC BY

Cite this

Jongmans, Sung Shik. / Discourje : Run-Time Verification of Communication Protocols in Clojure — Live at Last. Formal Methods - 26th International Symposium, FM 2024, Proceedings. editor / Andre Platzer ; Kristin Yvonne Rozier ; Matteo Pradella ; Matteo Rossi. Springer Science and Business Media Deutschland GmbH, 2025. pp. 158-166 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14934 LNCS).

@inproceedings{5efedb4a74d04182b00b34681d9cd267,

title = "Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last",

abstract = "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.",

author = "Jongmans, \{Sung Shik\}",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 26th International Symposium on Formal Methods, FM 2024 ; Conference date: 09-09-2024 Through 13-09-2024",

year = "2025",

doi = "10.1007/978-3-031-71177-0\_11",

language = "English",

isbn = "9783031711763",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "158--166",

editor = "Andre Platzer and Rozier, \{Kristin Yvonne\} and Matteo Pradella and Matteo Rossi",

booktitle = "Formal Methods - 26th International Symposium, FM 2024, Proceedings",

address = "Germany",

url = "https://www.fm24.polimi.it/",

}

Jongmans, SS 2025, Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last. in A Platzer, KY Rozier, M Pradella & M Rossi (eds), Formal Methods - 26th International Symposium, FM 2024, Proceedings. Springer Science and Business Media Deutschland GmbH, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14934 LNCS, pp. 158-166, 26th International Symposium on Formal Methods, Milan, Italy, 9/09/24. https://doi.org/10.1007/978-3-031-71177-0_11

Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last. / Jongmans, Sung Shik.
Formal Methods - 26th International Symposium, FM 2024, Proceedings. ed. / Andre Platzer; Kristin Yvonne Rozier; Matteo Pradella; Matteo Rossi. Springer Science and Business Media Deutschland GmbH, 2025. p. 158-166 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14934 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Discourje

T2 - 26th International Symposium on Formal Methods

AU - Jongmans, Sung Shik

N1 - Conference code: 26

PY - 2025

Y1 - 2025

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-71177-0_11

DO - 10.1007/978-3-031-71177-0_11

M3 - Conference Article in proceeding

AN - SCOPUS:85205091305

SN - 9783031711763

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 158

EP - 166

BT - Formal Methods - 26th International Symposium, FM 2024, Proceedings

A2 - Platzer, Andre

A2 - Rozier, Kristin Yvonne

A2 - Pradella, Matteo

A2 - Rossi, Matteo

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 9 September 2024 through 13 September 2024

ER -

Jongmans SS. Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last. In Platzer A, Rozier KY, Pradella M, Rossi M, editors, Formal Methods - 26th International Symposium, FM 2024, Proceedings. Springer Science and Business Media Deutschland GmbH. 2025. p. 158-166. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14934 LNCS). doi: 10.1007/978-3-031-71177-0_11