KIT | KIT-Bibliothek | Impressum | Datenschutz

Property Types for Mutable Data Structures in Java

Bachmeier, Joshua


Property Types are a kind of user-defined refinement type about variables and fields in a program. They are verified by discharging as many properties as possible using a scalable type checker. The remaining assertions are forwarded to a less scalable but more powerful deductive verification tool. However, the design and implementation by Lanzinger et al. cannot function in the presence of aliasing and mutability. In this thesis, we find that property checking can be performed safely on mutable data structures provided exclusive mutable access to the referenced object, which we define as property-safety. We study different approaches to aliasing control, including uniqueness, ownership and permissions. Based on this research, we present the Exclusivity Type System, which can be used to check the property-safety of program variables and class fields. Using flow-sensitive type refinement, we develop Mutable Property Types, which can track changes in a variable’s property type over time. Impure methods can be annotated to specify how they change the Property Types of their receiver and arguments. We explain how the original Property Checker’s program translation can be adapted to include correct assertions about the pre- and post-types of each method. ... mehr

Volltext §
DOI: 10.5445/IR/1000150318
Veröffentlicht am 02.09.2022
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Hochschulschrift
Publikationsdatum 01.08.2022
Sprache Englisch
Identifikator KITopen-ID: 1000150318
HGF-Programm 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
Verlag Karlsruher Institut für Technologie (KIT)
Art der Arbeit Abschlussarbeit - Master
Prüfungsdaten 04.08.2022
Referent/Betreuer Beckert, Bernhard
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page