@book{19716e99eed94630a54b0c2e36023eb9,
title = "Verifying Class Invariants in Concurrent Programs",
abstract = "Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in terms of a visible state semantics, i.e., invariants only have to hold whenever a method begins or ends execution, and they may be broken inside a method body. However, in a concurrent setting, this restriction is no longer usable, because due to thread interleavings, any program state is potentially a visible state. In this paper we present a new approach for reasoning about class invariants in multithreaded programs. We allow a thread to explicitly break an invariant at specific program locations, while ensuring that no other thread can observe the broken invariant. We develop our technique in a permission-based separation logic environment. However, we deviate from separation logic's standard rules and allow a class invariant to express properties over shared memory locations (the invariant footprint), independently of the permissions on these locations. In this way, a thread may break or reestablish an invariant without holding permissions to all locations in its footprint. To enable modular verification, we adopt the restrictions of Muller's ownership-based type system.",
keywords = "METIS-304003, IR-89408, Class Invariants, FMT-OO: VERIFICATION OF OBJECT-BASED SYSTEMS, Separation Logic, Permissions, EWI-24423, Verification",
author = "M. Zaharieva and Marieke Huisman",
year = "2014",
month = jan,
day = "17",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-14-01",
address = "Netherlands",
}