Please use this identifier to cite or link to this item:
Title: A unified framework for verification techniques for object invariants
Authors: Drossopoulou, Sophia
Francalanza, Adrian
Muller, Peter
Summers, Alexander J.
Keywords: Object-oriented methods (Computer science)
Computer software -- Development
Computer software -- Quality control
Issue Date: 2008
Publisher: Springer-Verlag Berlin Heidelberg
Citation: Drossopoulou, S., Francalanza, A., Müller, P., & Summers, A. J. (2008). A unified framework for verification techniques for object invariants. 22nd European Conference on Object-Oriented Programming, Paphos. 412-437.
Abstract: Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object invariants have been proposed. It is difficult to compare these techniques, and to ascertain their soundness, because of their differences in restrictions on programs and invariants, in the use of advanced type systems (e.g., ownership types), in the meaning of invariants, and in proof obligations. We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
A_Unified_Framework_for_Verification_Techniques_fo.pdf367.17 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.