Universe Types for KeY

Typ:	BA
Datum:	2025-03-07
Betreuer:	Wolfram Pfeifer Mattias Ulbrich
Aushang:	PDF

Background

Universe Types

Ownership type systems are a technique to enforce a hierarchical topology of the objects in programming. In recent years, this technique got a revival driven by the popularity of Rust.

More sophisticated ownership type systems, such as Universe types, can furthermore be used to ensure encapsulation by restricting certain references to only be used for read access.

KeY

KeY is a is a formal verification tool for Java, using symbolic execution and deductive reasoning in a dynamic logic with sequent calculus rules. KeY can be used for verifying that a Java programs adheres to a formal specifications written in the Java Modeling Language (JML).

Your Task

The goal is to develop a technique and a workflow to exploit ownership types in the KeY system. The idea is to integrate an existing type checker built with the checker framework.

Theoretical part:	Practical part:
- Adapt calculus rules of KeY	- Make the existing ownership checker usable
	- Implement the adapted rules
	- Collect and prepare concrete examples

Your Profile

You should have a background in formal methods (e.g., from relevant KIT lectures).