Verified Parameterized Choreographies Technical Report

TL;DR

Verified Parameterized Choreographies addresses verification of parameterized multi-party interactions by providing a formal PVL-based formalism that fuses object-oriented programming with choreographies. The approach defines a comprehensive set of choreographic and endpoint projection rules (Cp*, Ep*) enabling confinement-aware translation from high-level choreographies to per-endpoint code, including handling of endpoint families and channel invariants $R_I$. The method relies on concepts such as channel invariants, injectivity checks, and a confined memory model to ensure deadlock-freedom and correct projection under parameterization. This work enables automated verification and extraction of verified concurrent components from choreographies, with practical tooling through the VeyMont artifact, and supports debugging with choreography-only annotations to isolate non-verifying code.

Abstract

This technical report contains the full set of definitions and projection rules of the paper ``Verified Parameterized Choreographies'' by Rubbens et al. It also supplements the artefact.

Figures (4)

• Figure 1: PVL syntax. Left: OOP fragment, right: choreographic fragment.
• Figure 2: Definition of sort to approximate inequality between instances of $\alpha$
• Figure 3: All choreographic projection rules
• Figure 4: All endpoint projection rules