@InProceedings{10.1007/978-3-031-95589-1_3,
author="Rubbens, Robert
and van den Bos, Petra
and Huisman, Marieke",
editor="Di Giusto, Cinzia
and Ravara, Ant{\'o}nio",
title="Verified Parameterized Choreographies",
booktitle="Coordination Models and Languages",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="50--69",
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 .",
isbn="978-3-031-95589-1"
}

{"_id":"z2HsMEmqCrrrYrmJa","bibbaseid":"rubbens-vandenbos-huisman-verifiedparameterizedchoreographies-2025","author_short":["Rubbens, R.","van den Bos, P.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Rubbens"],"firstnames":["Robert"],"suffixes":[]},{"propositions":["van","den"],"lastnames":["Bos"],"firstnames":["Petra"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Di","Giusto"],"firstnames":["Cinzia"],"suffixes":[]},{"propositions":[],"lastnames":["Ravara"],"firstnames":["António"],"suffixes":[]}],"title":"Verified Parameterized Choreographies","booktitle":"Coordination Models and Languages","year":"2025","publisher":"Springer Nature Switzerland","address":"Cham","pages":"50–69","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 .","isbn":"978-3-031-95589-1","bibtex":"@InProceedings{10.1007/978-3-031-95589-1_3,\nauthor=\"Rubbens, Robert\nand van den Bos, Petra\nand Huisman, Marieke\",\neditor=\"Di Giusto, Cinzia\nand Ravara, Ant{\\'o}nio\",\ntitle=\"Verified Parameterized Choreographies\",\nbooktitle=\"Coordination Models and Languages\",\nyear=\"2025\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"50--69\",\nabstract=\"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 .\",\nisbn=\"978-3-031-95589-1\"\n}\n\n","author_short":["Rubbens, R.","van den Bos, P.","Huisman, M."],"editor_short":["Di Giusto, C.","Ravara, A."],"key":"10.1007/978-3-031-95589-1_3","id":"10.1007/978-3-031-95589-1_3","bibbaseid":"rubbens-vandenbos-huisman-verifiedparameterizedchoreographies-2025","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["verified","parameterized","choreographies","rubbens","van den bos","huisman"],"title":"Verified Parameterized Choreographies","year":2025}