Multiparty Session Typing in Java, Deductively

Jelle Bouma; Stijn de Gouw; Sung Shik Jongmans

doi:10.1007/978-3-031-30820-8_3

Multiparty Session Typing in Java, Deductively

Jelle Bouma, Stijn de Gouw, Sung Shik Jongmans^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
Editors	Sriram Sankaranarayanan, Natasha Sharygina
Place of Publication	Cham
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	19-27
Number of pages	9
ISBN (Print)	9783031308192
DOIs	https://doi.org/10.1007/978-3-031-30820-8_3
Publication status	Published - Apr 2023
Event	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023 - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 https://etaps.org/2023/cfp/

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13994 LNCS
ISSN	0302-9743

Conference

Conference	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023
Country/Territory	France
City	Paris
Period	22/04/23 → 27/04/23
Internet address	https://etaps.org/2023/cfp/

Access to Document

10.1007/978-3-031-30820-8_3Licence: CC BY

Cite this

Bouma, J., de Gouw, S., & Jongmans, S. S. (2023). Multiparty Session Typing in Java, Deductively. In S. Sankaranarayanan, & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings (pp. 19-27). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-30820-8_3

Bouma, Jelle ; de Gouw, Stijn ; Jongmans, Sung Shik. / Multiparty Session Typing in Java, Deductively. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. editor / Sriram Sankaranarayanan ; Natasha Sharygina. Cham : Springer Science and Business Media Deutschland GmbH, 2023. pp. 19-27 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13994 LNCS).

@inproceedings{e75b41c4878f43db9a8fcb4d737405f0,

title = "Multiparty Session Typing in Java, Deductively",

abstract = "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.",

author = "Jelle Bouma and {de Gouw}, Stijn and Jongmans, {Sung Shik}",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s).; 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023 ; Conference date: 22-04-2023 Through 27-04-2023",

year = "2023",

month = apr,

doi = "10.1007/978-3-031-30820-8_3",

language = "English",

isbn = "9783031308192",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "19--27",

editor = "Sriram Sankaranarayanan and Natasha Sharygina",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings",

address = "Germany",

url = "https://etaps.org/2023/cfp/",

}

Bouma, J, de Gouw, S & Jongmans, SS 2023, Multiparty Session Typing in Java, Deductively. in S Sankaranarayanan & N Sharygina (eds), Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Springer Science and Business Media Deutschland GmbH, Cham, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13994 LNCS, pp. 19-27, 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, 22/04/23. https://doi.org/10.1007/978-3-031-30820-8_3

Multiparty Session Typing in Java, Deductively. / Bouma, Jelle; de Gouw, Stijn; Jongmans, Sung Shik.
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. ed. / Sriram Sankaranarayanan; Natasha Sharygina. Cham: Springer Science and Business Media Deutschland GmbH, 2023. p. 19-27 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13994 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Multiparty Session Typing in Java, Deductively

AU - Bouma, Jelle

AU - de Gouw, Stijn

AU - Jongmans, Sung Shik

PY - 2023/4

Y1 - 2023/4

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85161411660&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-30820-8_3

DO - 10.1007/978-3-031-30820-8_3

M3 - Conference Article in proceeding

AN - SCOPUS:85161411660

SN - 9783031308192

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 19

EP - 27

BT - Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings

A2 - Sankaranarayanan, Sriram

A2 - Sharygina, Natasha

PB - Springer Science and Business Media Deutschland GmbH

CY - Cham

T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023

Y2 - 22 April 2023 through 27 April 2023

ER -

Bouma J, de Gouw S, Jongmans SS. Multiparty Session Typing in Java, Deductively. In Sankaranarayanan S, Sharygina N, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Cham: Springer Science and Business Media Deutschland GmbH. 2023. p. 19-27. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13994 LNCS). doi: 10.1007/978-3-031-30820-8_3

Multiparty Session Typing in Java, Deductively

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this