Exclusivity through Fractional Permissions for Java

Property types are a way to specify program behavior through a type system. They are
refinement types that reason about user-defined properties. When verifying, some prop-
erties can be discharged using a type checker that provides good usability. The remaining
properties can then be checked by a more powerful tool for deductive verification to
eliminate most false positives.
To be able to verify mutable data structures, property types need a system that ensures
that only exclusive references can be mutated. The Kukicha framework for property types
provides a Uniqueness Checker that ensures this property. The type system that it enforces,
however, enforces rather conservative rules, leading to many false positives.
In this thesis, we develop a type system that upholds this invariant while keeping a high
degree of expressiveness. We formalize its type rules on a minimal imperative language and
provide a formal proof that it ensures the exclusivity requirements. We present borroℚ, an
implementation of this type system using the Checker Framework. For this, we adapt the
type rules to Java, balancing adherence to the proven formal specification and usability.