Behavioural Separation with Parallel Usages
Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.
Tue 13 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:50 - 18:50 | |||
16:50 30mTalk | IntelliJML: A JML plugin for IntelliJ IDEA FTfJP P: Steven Monteiro University of Twente, P: Erikas Sokolovas University of Twente, The Netherlands, P: Ellen Wittingen University of Twente, Tom van Dijk University of Twente, Marieke Huisman University of Twente File Attached | ||
17:20 30mTalk | Ensuring correct cryptographic algorithm and provider usage at compile time FTfJP P: Weitian Xing University of Waterloo, Yuanhui Cheng University of Waterloo, Werner Dietl University of Waterloo Media Attached | ||
17:50 30mTalk | Behavioural Separation with Parallel Usages FTfJP Iaroslav Golovanov Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, P: Mathias Steen Jakobsen Department of Computer Science, Aalborg University, Denmark, Mikkel Klinke Kettunen Department of Computer Science, Aalborg University, Denmark | ||
18:20 30mTalk | Combining Formal and Machine Learning Techniques for the Generation of JML Specifications FTfJP DOI File Attached | ||
18:50 30mTalk | JML and OpenJML for Java 16 FTfJP File Attached |