Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

Mario Bravetti; Adrian Francalanza; Iaroslav Golovanov; Hans Hüttel; Mathias S. Jakobsen; Mikkel K. Kettunen; António Ravara

doi:10.1007/978-3-030-64437-6_6

Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias S. Jakobsen, Mikkel K. Kettunen, António Ravara^*

^*Kontaktforfatter

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

5 Citationer (Scopus)

Abstract

We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.

Originalsprog	Engelsk
Titel	Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings
Redaktører	Bruno C. Oliveira
Antal sider	20
Forlag	Springer
Publikationsdato	2020
Sider	105-124
ISBN (Trykt)	978-3-030-64436-9
ISBN (Elektronisk)	978-3-030-64437-6
DOI	https://doi.org/10.1007/978-3-030-64437-6_6
Status	Udgivet - 2020
Begivenhed	18th Asian Symposium on Programming Languages and Systems, APLAS 2020 - Fukuoka, Japan Varighed: 30 nov. 2020 → 2 dec. 2020

Konference

Konference	18th Asian Symposium on Programming Languages and Systems, APLAS 2020
Land/Område	Japan
By	Fukuoka
Periode	30/11/2020 → 02/12/2020

Navn	Lecture Notes in Computer Science
Vol/bind	12470
ISSN	0302-9743

Bibliografisk note

Funding Information:
Work partially supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No. 778233 (BehAPI), the UK EPSRC grant EP/K034413/1 (ABCD), and by NOVA LINCS (UIDB/04516/2020) via FCT.

Publisher Copyright:
© 2020, Springer Nature Switzerland AG.

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

Adgang til dokumentet

10.1007/978-3-030-64437-6_6

https://arxiv.org/pdf/2002.12793.pdf

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

Link to publication in Scopus

Citationsformater

Bravetti, M., Francalanza, A., Golovanov, I., Hüttel, H., Jakobsen, M. S., Kettunen, M. K., & Ravara, A. (2020). Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. I B. C. Oliveira (red.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings (s. 105-124). Springer. https://doi.org/10.1007/978-3-030-64437-6_6

@inproceedings{74e25beed039487c9cd4f331330643b2,

title = "Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language",

abstract = "We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.",

author = "Mario Bravetti and Adrian Francalanza and Iaroslav Golovanov and Hans H{\"u}ttel and Jakobsen, {Mathias S.} and Kettunen, {Mikkel K.} and Ant{\'o}nio Ravara",

note = "Funding Information: Work partially supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No. 778233 (BehAPI), the UK EPSRC grant EP/K034413/1 (ABCD), and by NOVA LINCS (UIDB/04516/2020) via FCT. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 ; Conference date: 30-11-2020 Through 02-12-2020",

year = "2020",

doi = "10.1007/978-3-030-64437-6_6",

language = "English",

isbn = "978-3-030-64436-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "105--124",

editor = "Oliveira, {Bruno C.}",

booktitle = "Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings",

address = "Germany",

}

Bravetti, M, Francalanza, A, Golovanov, I, Hüttel, H, Jakobsen, MS, Kettunen, MK & Ravara, A 2020, Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. i BC Oliveira (red.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Springer, Lecture Notes in Computer Science, bind 12470, s. 105-124, 18th Asian Symposium on Programming Languages and Systems, APLAS 2020, Fukuoka, Japan, 30/11/2020. https://doi.org/10.1007/978-3-030-64437-6_6

Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. / Bravetti, Mario; Francalanza, Adrian; Golovanov, Iaroslav et al.
Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. red. / Bruno C. Oliveira. Springer, 2020. s. 105-124 (Lecture Notes in Computer Science, Bind 12470).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

TY - GEN

T1 - Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

AU - Bravetti, Mario

AU - Francalanza, Adrian

AU - Golovanov, Iaroslav

AU - Hüttel, Hans

AU - Jakobsen, Mathias S.

AU - Kettunen, Mikkel K.

AU - Ravara, António

N1 - Funding Information: Work partially supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No. 778233 (BehAPI), the UK EPSRC grant EP/K034413/1 (ABCD), and by NOVA LINCS (UIDB/04516/2020) via FCT. Publisher Copyright: © 2020, Springer Nature Switzerland AG. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.

PY - 2020

Y1 - 2020

N2 - We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.

AB - We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.

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

U2 - 10.1007/978-3-030-64437-6_6

DO - 10.1007/978-3-030-64437-6_6

M3 - Article in proceeding

AN - SCOPUS:85097642531

SN - 978-3-030-64436-9

T3 - Lecture Notes in Computer Science

SP - 105

EP - 124

BT - Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings

A2 - Oliveira, Bruno C.

PB - Springer

T2 - 18th Asian Symposium on Programming Languages and Systems, APLAS 2020

Y2 - 30 November 2020 through 2 December 2020

ER -

Bravetti M, Francalanza A, Golovanov I, Hüttel H, Jakobsen MS, Kettunen MK et al. Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. I Oliveira BC, red., Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Springer. 2020. s. 105-124. (Lecture Notes in Computer Science, Bind 12470). doi: 10.1007/978-3-030-64437-6_6

Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

Abstract

Konference

Bibliografisk note

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Citationsformater