2023-04-20
Multiparty session typing in Java, deductively
Publication
Publication
Presented at the
29th International Conference Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2023 (April 2023), Paris, France
Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to specifications. 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.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-031-30820-8_3 | |
| Lecture Notes in Computer Science | |
| 29th International Conference Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2023 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Bouma, J., de Gouw, S., & Jongmans, S. (2023). Multiparty session typing in Java, deductively. In 29th International Conference Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2023 (pp. 19–27). doi:10.1007/978-3-031-30820-8_3 |
|
