---

Download: PDF.

“Object Ownership in Program Verification” by W. Dietl and P. Müller. In Aliasing in Object-Oriented Programming, vol. 7850 of Lecture Notes in Computer Science, (D. Clarke, J. Noble, and T. Wrigstad, eds.), 2013, pp. 289-318.

Abstract

Dealing with aliasing is one of the key challenges for the verification of imperative programs. For instance, aliases make it difficult to determine which abstractions are potentially affected by a heap update and to determine which locks need to be acquired to avoid data races. Object ownership was one of the first approaches that allowed programmers to control aliasing and to restrict the operations that can be applied to a reference. It thus enabled sound, modular, and automatic verification of heap-manipulating programs. In this paper, we present two ownership systems that have been designed specifically to support program verification — Universe Types and Spec#'s Dynamic Ownership — and explain their applications in program verification, illustrated through a series of Spec# examples.

Keywords: Universe Types, dynamic ownership, Spec#

Download: PDF.

BibTeX entry:

@incollection{DietlMueller12,
   author = {W. Dietl and P. M{"u}ller},
   editor = {D. Clarke and J. Noble and T. Wrigstad},
   title = {Object Ownership in Program Verification},
   booktitle = {Aliasing in Object-Oriented Programming},
   series = {Lecture Notes in Computer Science},
}

---

---