# Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)

## TL;DR

This paper introduces a method to simplify the verification of concurrent distributed systems by transforming them into sequential and independent components, enabling more efficient analysis of properties involving concrete data.

## Contribution

It proposes a novel approach to sequentialize well-typed systems guided by global types, facilitating verification of data-dependent properties beyond traditional session types.

## Key findings

- Reduces concurrency to sequential and independent parallel compositions
- Enables efficient verification of data-based termination properties
- Improves analysis of concrete run properties in distributed systems

## Abstract

The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and concurrency in distributed systems. As such, they provide an efficient verification method w.r.t. properties about communication and concurrency, like communication safety or progress. However, they do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables. We sequentialise well-typed systems of processes guided by the structure of their global type to obtain interaction-free abstractions thereof. Without interaction, concurrency in the system is reduced to sequential and completely independent parallel compositions. In such abstractions, the verification of properties such as e.g. data-based termination that are not covered by multiparty session types, but rely on concrete runs or values of variables, becomes significantly more efficient.