Computing Publications

Publications Home » A Universe-Type-Based Verificatio...

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

Alexander Summers, Sophia Drossopoulou, Peter

Conference or Workshop Paper
Formal techniques for Java-like Programming
July, 2008

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'

PDF of full publication (168 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.