Multiparty session typing in Java, deductively (Artifact)

Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to specifications. In the paper "Multiparty Session Typing in Java, Deductively" (TACAS'23), we present BGJ: a new tool to apply the MPST method in combination with Java. The checks performed using our tool are purely static (all errors are reported early at compile-time) and resource-efficient (near-zero cost abstractions at run-time), thereby addressing two issues of existing tools. BGJ is built using VerCors, but our approach is general.

• View at Publisher

See Also
inProceedings Multiparty session typing in Java, deductively J. Bouma (Jelle), C.P.T. de Gouw (Stijn) and S.-S.T.Q. Jongmans (Sung)