VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory

Robert Rubbens; Petra V. van den Bos; Marieke Huisman

doi:10.1007/978-3-031-76554-4_12

VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory

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

^*Corresponding author for this work

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

Abstract

In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.

Original language	English
Title of host publication	Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings
Editors	Nikolai Kosmatov, Laura Kovács
Publisher	Springer
Pages	217-236
Number of pages	20
ISBN (Print)	9783031765537
DOIs	https://doi.org/10.1007/978-3-031-76554-4_12
Publication status	Published - 13 Nov 2024
Event	19th International Conference on integrated Formal Methods, iFM 2024 - Manchester, United Kingdom Duration: 13 Nov 2024 → 15 Nov 2024 Conference number: 19

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	15234 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Conference on integrated Formal Methods, iFM 2024
Abbreviated title	IFM 2024
Country/Territory	United Kingdom
City	Manchester
Period	13/11/24 → 15/11/24

Keywords

2025 OA procedure
Concurrent programs
Deductive verification
Choreographies

Access to Document

10.1007/978-3-031-76554-4_12

Cite this

Rubbens, R., van den Bos, P. V., & Huisman, M. (2024). VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. In N. Kosmatov, & L. Kovács (Eds.), Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings (pp. 217-236). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15234 LNCS). Springer. https://doi.org/10.1007/978-3-031-76554-4_12

Rubbens, Robert ; van den Bos, Petra V. ; Huisman, Marieke. / VeyMont : Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings. editor / Nikolai Kosmatov ; Laura Kovács. Springer, 2024. pp. 217-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ff6c20b49a3c4b909fa77fb8e41b5c91,

title = "VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory",

abstract = "In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.",

keywords = "2025 OA procedure, Concurrent programs, Deductive verification, Choreographies",

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

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.; 19th International Conference on integrated Formal Methods, iFM 2024, IFM 2024 ; Conference date: 13-11-2024 Through 15-11-2024",

year = "2024",

month = nov,

day = "13",

doi = "10.1007/978-3-031-76554-4_12",

language = "English",

isbn = "9783031765537",

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

publisher = "Springer",

pages = "217--236",

editor = "Nikolai Kosmatov and Laura Kov{\'a}cs",

booktitle = "Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings",

address = "Germany",

}

Rubbens, R, van den Bos, PV & Huisman, M 2024, VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. in N Kosmatov & L Kovács (eds), Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 15234 LNCS, Springer, pp. 217-236, 19th International Conference on integrated Formal Methods, iFM 2024, Manchester, United Kingdom, 13/11/24. https://doi.org/10.1007/978-3-031-76554-4_12

VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. / Rubbens, Robert; van den Bos, Petra V.; Huisman, Marieke.
Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings. ed. / Nikolai Kosmatov; Laura Kovács. Springer, 2024. p. 217-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15234 LNCS).

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

TY - GEN

T1 - VeyMont

T2 - 19th International Conference on integrated Formal Methods, iFM 2024

AU - Rubbens, Robert

AU - van den Bos, Petra V.

AU - Huisman, Marieke

N1 - Conference code: 19

PY - 2024/11/13

Y1 - 2024/11/13

N2 - In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.

AB - In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.

KW - 2025 OA procedure

KW - Concurrent programs

KW - Deductive verification

KW - Choreographies

UR - http://www.scopus.com/inward/record.url?scp=85210104651&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-76554-4_12

DO - 10.1007/978-3-031-76554-4_12

M3 - Conference contribution

AN - SCOPUS:85210104651

SN - 9783031765537

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

SP - 217

EP - 236

BT - Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings

A2 - Kosmatov, Nikolai

A2 - Kovács, Laura

PB - Springer

Y2 - 13 November 2024 through 15 November 2024

ER -

Rubbens R, van den Bos PV , Huisman M. VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. In Kosmatov N, Kovács L, editors, Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings. Springer. 2024. p. 217-236. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-76554-4_12