Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Robert Rubbens,
  • Petra van den Bos,
  • Marieke Huisman

摘要

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.