Previous article

Next article

Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods

A. J. Summers, Imperial College London
S. Drossopoulou, Imperial College London
P. Müller, ETH, Zürich



PDF Icon
PDF Version


We present three novel techniques for the Verification of invariants in the setting of Java-like languages including static fields and methods. Our techniques structure the heap through universe types, and extend the Visibility Technique of Müller et al. In order to cater for mutable static fields, we extend the classical universe types heap topology with multiple trees, where each tree is rooted in a class. Thus classes may naturally own objects as static fields.

We present a basic version of our approach, which allows trees to be visited at the top and then navigated "downwards", and which avoids dangerous call-backs through effects which track static method calls. As well as the usual kinds of proof obligations de ning that certain invariants must hold at a given state, we employ a second kind of obligation to show that certain other invariants are preserved between two states (i.e., if they hold in the former state then they will still hold in the latter). This allows us to deal with invariants whose expected truth-value cannot always be determined statically in a modular way.

We then present two extensions of our basic technique, aimed at improving usability. Firstly, we introduce a new universe annotation to allow safe callbacks between trees, whereby trees may be visited not at the top, but at the point where a previous visit "had left off". Secondly, we refine our heap topology with a notion of 'levels', which stratify the heap and provide modularity with regard to library classes and the required effects annotations.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors


A. J. Summer is a Research Associate in the Department of Computing at Imperial College London, and is working on the Mobius project. He can be reached by email at alexander. See also his webpage at˜ajs300m


Sophia Drossopoulou is Professor in Programming Languages in the Department of Computing at Imperial College London. She can be reached by email at See also her webpage at˜scd


Peter Müller is Professor in Programming Methodology at ETH Zürich. He can be reached by email at See also his webpage at

A. J. Summers, S. Drossopoulou, P. Müller: "Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods", in Journal of Object Technology,vol. 8, no. 4, Special Issue: Workhop FTfJP and IWACO at ECOOP 08, June 2009, pp. 85-125


Previous article

Next article