Verified Parameterized Choreographies

Robert Rubbens; Petra van den Bos; Marieke Huisman

doi:10.1007/978-3-031-95589-1_3

Verified Parameterized Choreographies

Robert Rubbens^*
, Petra van den Bos
, Marieke Huisman

^*Corresponding author for this work

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

50 Downloads (Pure)

Abstract

Choreographies are useful for modelling systems with multiple simultaneously executing and communicating participants, e.g. distributed systems. VeyMont can verify correctness of choreographies and generate verifiably correct code that implements the choreography. Initially, it supported only fixed sets of participants. However, realistic systems are often parameterized: they scale according to some parameter N. This paper extends VeyMont with parameterized choreographies, making VeyMont more usable for realistic case studies. Specifically, we add parameterized primitives such as participant families and parameterized communication. We encode these primitives using a structured parallelism primitive from the underlying verifier VerCors , and by using conditionals in the endpoint projection, partially delaying projection until run time. We illustrate the encoding with a distributed summation choreography, and prove it correct with VerCors .

Original language	English
Title of host publication	Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings
Editors	Cinzia Di Giusto, António Ravara
Publisher	Springer
Pages	50-69
Number of pages	20
ISBN (Print)	9783031955884
DOIs	https://doi.org/10.1007/978-3-031-95589-1_3
Publication status	Published - 18 Jun 2025
Event	COORDINATION 2025: International Conference on Coordination Models and Languages - École National Supérieure des Arts et Métiers (ENSAM), Lille, France Duration: 16 Jun 2025 → 20 Jun 2025 Conference number: 27th https://www.discotec.org/2025/coordination

Publication series

Name	Lecture Notes in Computer Science
Volume	15731 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	COORDINATION 2025
Country/Territory	France
City	Lille
Period	16/06/25 → 20/06/25
Internet address	https://www.discotec.org/2025/coordination

Keywords

2025 OA procedure
Deductive verification
Parameterization
Choreographies

Access to Document

10.1007/978-3-031-95589-1_3

978-3-031-95589-1_3Final published version, 1.44 MBLicence: Taverne

Cite this

Rubbens, R., van den Bos, P., & Huisman, M. (2025). Verified Parameterized Choreographies. In C. Di Giusto, & A. Ravara (Eds.), Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings (pp. 50-69). (Lecture Notes in Computer Science; Vol. 15731 LNCS). Springer. https://doi.org/10.1007/978-3-031-95589-1_3

Rubbens, Robert ; van den Bos, Petra ; Huisman, Marieke. / Verified Parameterized Choreographies. Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings. editor / Cinzia Di Giusto ; António Ravara. Springer, 2025. pp. 50-69 (Lecture Notes in Computer Science).

@inproceedings{e3d73de29c664f369e996f69eaed8d1d,

title = "Verified Parameterized Choreographies",

abstract = "Choreographies are useful for modelling systems with multiple simultaneously executing and communicating participants, e.g. distributed systems. VeyMont can verify correctness of choreographies and generate verifiably correct code that implements the choreography. Initially, it supported only fixed sets of participants. However, realistic systems are often parameterized: they scale according to some parameter N. This paper extends VeyMont with parameterized choreographies, making VeyMont more usable for realistic case studies. Specifically, we add parameterized primitives such as participant families and parameterized communication. We encode these primitives using a structured parallelism primitive from the underlying verifier VerCors , and by using conditionals in the endpoint projection, partially delaying projection until run time. We illustrate the encoding with a distributed summation choreography, and prove it correct with VerCors .",

keywords = "2025 OA procedure, Deductive verification, Parameterization, Choreographies",

author = "Robert Rubbens and \{van den Bos\}, Petra and Marieke Huisman",

note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2025.; COORDINATION 2025 : International Conference on Coordination Models and Languages ; Conference date: 16-06-2025 Through 20-06-2025",

year = "2025",

month = jun,

day = "18",

doi = "10.1007/978-3-031-95589-1\_3",

language = "English",

isbn = "9783031955884",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "50--69",

editor = "\{Di Giusto\}, Cinzia and Ant{\'o}nio Ravara",

booktitle = "Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings",

address = "Germany",

url = "https://www.discotec.org/2025/coordination",

}

Rubbens, R , van den Bos, P & Huisman, M 2025, Verified Parameterized Choreographies. in C Di Giusto & A Ravara (eds), Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings. Lecture Notes in Computer Science, vol. 15731 LNCS, Springer, pp. 50-69, COORDINATION 2025, Lille, France, 16/06/25. https://doi.org/10.1007/978-3-031-95589-1_3

Verified Parameterized Choreographies. / Rubbens, Robert ; van den Bos, Petra ; Huisman, Marieke.
Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings. ed. / Cinzia Di Giusto; António Ravara. Springer, 2025. p. 50-69 (Lecture Notes in Computer Science; Vol. 15731 LNCS).

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

TY - GEN

T1 - Verified Parameterized Choreographies

AU - Rubbens, Robert

AU - van den Bos, Petra

AU - Huisman, Marieke

N1 - Conference code: 27th

PY - 2025/6/18

Y1 - 2025/6/18

N2 - Choreographies are useful for modelling systems with multiple simultaneously executing and communicating participants, e.g. distributed systems. VeyMont can verify correctness of choreographies and generate verifiably correct code that implements the choreography. Initially, it supported only fixed sets of participants. However, realistic systems are often parameterized: they scale according to some parameter N. This paper extends VeyMont with parameterized choreographies, making VeyMont more usable for realistic case studies. Specifically, we add parameterized primitives such as participant families and parameterized communication. We encode these primitives using a structured parallelism primitive from the underlying verifier VerCors , and by using conditionals in the endpoint projection, partially delaying projection until run time. We illustrate the encoding with a distributed summation choreography, and prove it correct with VerCors .

AB - Choreographies are useful for modelling systems with multiple simultaneously executing and communicating participants, e.g. distributed systems. VeyMont can verify correctness of choreographies and generate verifiably correct code that implements the choreography. Initially, it supported only fixed sets of participants. However, realistic systems are often parameterized: they scale according to some parameter N. This paper extends VeyMont with parameterized choreographies, making VeyMont more usable for realistic case studies. Specifically, we add parameterized primitives such as participant families and parameterized communication. We encode these primitives using a structured parallelism primitive from the underlying verifier VerCors , and by using conditionals in the endpoint projection, partially delaying projection until run time. We illustrate the encoding with a distributed summation choreography, and prove it correct with VerCors .

KW - 2025 OA procedure

KW - Deductive verification

KW - Parameterization

KW - Choreographies

UR - https://www.scopus.com/pages/publications/105009411230

U2 - 10.1007/978-3-031-95589-1_3

DO - 10.1007/978-3-031-95589-1_3

M3 - Conference contribution

AN - SCOPUS:105009411230

SN - 9783031955884

T3 - Lecture Notes in Computer Science

SP - 50

EP - 69

BT - Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings

A2 - Di Giusto, Cinzia

A2 - Ravara, António

PB - Springer

T2 - COORDINATION 2025

Y2 - 16 June 2025 through 20 June 2025

ER -

Rubbens R , van den Bos P , Huisman M. Verified Parameterized Choreographies. In Di Giusto C, Ravara A, editors, Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings. Springer. 2025. p. 50-69. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-95589-1_3

Verified Parameterized Choreographies

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification

Cite this