Please use this identifier to cite or link to this item:
|Title:||A unified framework for verification techniques for object invariants|
Summers, Alexander J.
|Keywords:||Object-oriented methods (Computer science)|
Computer software -- Development
Computer software -- Quality control
|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:
|A_Unified_Framework_for_Verification_Techniques_fo.pdf||367.17 kB||Adobe PDF||View/Open|
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.