We report ongoing work on the analysis of the protocols that pervade concurrent and distributed software. These protocols are key to ensure that communicating programs interact correctly, without communication errors and deadlocks.

We focus on multiparty session types (MPST), an approach that uses governing multiparty protocols as types to verify the correctness of message-passing programs. Rather than the π-calculus, we target the verification of programs by relying on ACP (the Algebra of Communicating Processes) as specification language; rather than typing, we aim to adopt model checking using the mCRL2 toolset.