Reasoning about Choreographic Programs

Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, Marco Peressotti [2023].
In CoRR abs/2304.14539.

Abstract

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties. This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2304-14539,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Eva Graversen and
                  Fabrizio Montesi and
                  Marco Peressotti},
  title        = {Reasoning about Choreographic Programs},
  journal      = {CoRR},
  volume       = {abs/2304.14539},
  year         = {2023},
  url          = {https://doi.org/10.48550/arXiv.2304.14539},
  doi          = {10.48550/ARXIV.2304.14539},
  eprinttype    = {arXiv},
  eprint       = {2304.14539},
  timestamp    = {Thu, 04 May 2023 15:47:42 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2304-14539.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Peer-reviewed version

Click to show in publication list