Computing Publications

Publications Home » A Unified Framework for Verificat...

A Unified Framework for Verification Techniques for Object Invariants

Sophia Drossopoulou, Adrian Francalanza, Peter

Conference or Workshop Paper
International Workshop on Foundations of Object Oriented Languages (FOOL)
January, 2008

Verification of object-oriented programs relies on object invariants to express consistency criteria of objects. The semantics of object invariants is subtle, mainly because of call-backs, multi-object invariants, and subclassing.

Several verification techniques for object invariants have been proposed. These techniques are complex and differ in restrictions on programs (for instance, which fields can be updated), restrictions on invariants (what an invariant may refer to), use of advanced type

systems (such as ownership types), meaning of invariants (in which execution states are invariants assumed to hold), and proof obligations (when should an invariant be proven). As a result, it is difficult to understand whether/why these techniques are sound, whether/why they are modular, and to compare their expressiveness. This general lack of understanding also hampers the development of new techniques.

In this paper, we develop and formalise a unified framework to describe verification techniques for object invariants. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters under which a verification technique is sound. We also define what it means for a technique to be modular. To illustrate the generality of our framework, we instantiate it with six verification techniques from the literature. We show how our framework facilitates the assessment and comparison of the soundness, modularity, and expressiveness of these techniques.


BibTEX file for the publication built & maintained by Ashok Argent-Katwala.