A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods (Work in Progress)

Abstract

We present a novel technique for the verification of invariants in the setting of a Java-like language including static fields and methods. The technique is a generalisation of the existing Visibility Technique of Mueller et al., which employs universe types. In order to cater for mutable static fields, we extend this topology to multiple trees (a forest), where each tree is rooted in a class. This allows classes to naturally own object instances as their static fields.We describe how to extend the Visibility Technique to this topology, incorporating extra flexibility for the treatment of static methods. We encounter a potential source of callbacks not present in the original technique, and show how to overcome this using an effects system. To allow flexible and modular verification, we refine our topology with a hierarchy of `levels