VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. Rubbens, R., Bos, P. v. d., & Huisman, M. In Kosmatov, N. & Kovács, L., editors, Integrated Formal Methods, pages 217–236, Cham, 2024. Springer Nature Switzerland. abstract bibtex 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.
@InProceedings{10.1007/978-3-031-76554-4_12,
author="Rubbens, Robert
and Bos, Petra van den
and Huisman, Marieke",
editor="Kosmatov, Nikolai
and Kov{\'a}cs, Laura",
title="VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory",
booktitle="Integrated Formal Methods",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="217--236",
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.",
isbn="978-3-031-76554-4"
}
Downloads: 0
{"_id":"PPb73MFoNzihHjGTK","bibbaseid":"rubbens-bos-huisman-veymontchoreographybasedgenerationofcorrectconcurrentprogramswithsharedmemory-2024","author_short":["Rubbens, R.","Bos, P. v. d.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Rubbens"],"firstnames":["Robert"],"suffixes":[]},{"propositions":[],"lastnames":["Bos"],"firstnames":["Petra","van","den"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Kosmatov"],"firstnames":["Nikolai"],"suffixes":[]},{"propositions":[],"lastnames":["Kovács"],"firstnames":["Laura"],"suffixes":[]}],"title":"VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory","booktitle":"Integrated Formal Methods","year":"2024","publisher":"Springer Nature Switzerland","address":"Cham","pages":"217–236","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.","isbn":"978-3-031-76554-4","bibtex":"@InProceedings{10.1007/978-3-031-76554-4_12,\nauthor=\"Rubbens, Robert\nand Bos, Petra van den\nand Huisman, Marieke\",\neditor=\"Kosmatov, Nikolai\nand Kov{\\'a}cs, Laura\",\ntitle=\"VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory\",\nbooktitle=\"Integrated Formal Methods\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"217--236\",\nabstract=\"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.\",\nisbn=\"978-3-031-76554-4\"\n}\n\n","author_short":["Rubbens, R.","Bos, P. v. d.","Huisman, M."],"editor_short":["Kosmatov, N.","Kovács, L."],"key":"10.1007/978-3-031-76554-4_12","id":"10.1007/978-3-031-76554-4_12","bibbaseid":"rubbens-bos-huisman-veymontchoreographybasedgenerationofcorrectconcurrentprogramswithsharedmemory-2024","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":["veymont","choreography","based","generation","correct","concurrent","programs","shared","memory","rubbens","bos","huisman"],"title":"VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory","year":2024}