Towards Practical Protocol Verification via Minimal Orchestration in ACP
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.
|Extended Abstract (agere21_VdHeuvelPerez_CameraReady.pdf)||415KiB|
Sun 17 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10
|Session Types in Elixir|
AGEREDOI File Attached
|Towards Practical Protocol Verification via Minimal Orchestration in ACP|