Region-based memory management has been shown to be an effective alternative that can co-exist with garbage collectors in memory managed languages especially for Real-Time and Big Data applications. In this paper we propose a novel variant region type system that extends our previous Java region types to Generic Java. The main difficulties are given by the type variables used by Generic Java. Our proposal is based on a modular flow analysis that captures regions lifetime relations via subtyping constraints at the method boundary. Our variant region type system guarantees that well-typed Generic Java programs use lexically-scoped regions and never create dangling references in the store and on the program stack.

Communication-centered programming is one of the most challenging programming paradigms. Development of modern software applications requires expressive mechanisms to specify and verify the communications between different parties. In the last decade, many works have used session types to characterize the various aspects of structured communications. Different from session types, we propose a novel session logic with disjunctions to specify and verify the implementation of communication protocols. Our current logic is based on only twoparty channel sessions, but it is capable of handling delegation naturally through the use of higher-order channels. Due to our use of disjunctions to model both internal and external choices, we rely solely on conditional statements to support such choices, as opposed to specialized switch constructs in prior proposals. Furthermore, since our proposal is based on an extension of separation logic, it also supports heap-manipulating programs and copyless message passing. We demonstrate the expressivity and applicability of our logic on a number of examples.

Constructing software automatically from highlevel models is one of the challenges in software engineering nowadays. There is an urgent need for adequate methods to ensure high quality of models. The Executable Foundational UML (fUML) has been proposed as a computationally complete and compact subset of UML. A fUML model is supposed to be executed and tested in the early stage of the software development process. The complete static and operational semantics of fUML is still in its early stages, and although several proposals to execute and verify fUML models have been issued, this problem is still open. Our project aims to develop a complete virtual machine for fUML models using the K-framework which is a rewrite-based executable semantic framework. Our novel model execution will enable to efficiently test and verify fUML models.

10.1145/1167473.1167498

Region-based memory management offers several important potential advantages over garbage collection, including real-time performance, better data locality, and more efficient use of limited memory. Researchers have advocated the use of regions for functional, imperative, and object-oriented languages. Lexically scoped regions are now a core feature of the Real-Time Specification for Java (RTSJ)[5].Recent research in region-based programming for Java has focused on region checking, which requires manual effort to augment the program with region annotations. In this paper, we propose an automatic region inference system for a core subset of Java. To provide an inference method that is both precise and practical, we support classes and methods that are region-polymorphic, with region-polymorphic recursion for methods. One challenging aspect is to ensure region safety in the presence of features such as class subtyping, method overriding, and downcast operations. Our region inference rules can handle these object-oriented features safely without creating dangling references.