PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Mon 24 Jun 2024 13:40 - 14:00 at Finland - Languages & Verification Chair(s): Lindsey Kuper

We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that allows to describe the desired interactions within a concurrent system from a global viewpoint. Employing choreographies provides a clear and comprehensive view of system interactions, enabling the discernment of process flow and detection of potential errors, thus ensuring accurate execution and enhancing system reliability. We equip our language with a probabilistic semantics and then define a formal encoding into the PRISM language and discuss its correctness. Properties of programs written in our choreographic language can be model-checked by the PRISM model-checker via their translation into the PRISM language. Finally, we implement a compiler for our language and demonstrate its practical applicability via examples drawn from the use cases featured in the PRISM website.

This work is currently under submission for publication.

Mon 24 Jun

Displayed time zone: Windhoek change

13:40 - 15:20
Languages & VerificationCP at Finland
Chair(s): Lindsey Kuper University of California, Santa Cruz
13:40
20m
Talk
A Probabilistic Choreography Language for PRISM
CP
Marco Carbone IT University of Copenhagen, Adele Veschetti Technische Universität Darmstadt
Media Attached
14:00
20m
Talk
A Function-as-a-Service Choreographic Programming Language: Examples and Applications
CP
Giuseppe De Palma Department of Computer Science and Engineering - Università di Bologna, Saverio Giallorenzo Alma Mater Studiorum - Università di Bologna / INRIA, Jacopo Mauro University of Southern Denmark, Matteo Trentin Università di Bologna, Gianluigi Zavattaro Department of Computer Science and Engineering - Università di Bologna
Pre-print
14:20
20m
Talk
Exploring Algebraic Placement in Multiparty Languages
CP
George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
Pre-print Media Attached
14:40
20m
Talk
Poroutines: The Essence of Choreographic Programming?
CP
Dan Plyukhin University of Southern Denmark
15:00
20m
Talk
We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
CP
Mako P. Bates University of Vermont, Joseph P. Near University of Vermont
Pre-print Media Attached