@inproceedings{jacobs2005safe,
author = {Jacobs, Bart and Leino, Rustan and Piessens, Frank and Schulte, Wolfram},
title = {Safe Concurrency for Aggregate Objects with Invariants},
booktitle = {SEFM},
year = {2005},
month = {January},
abstract = {Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a flexible methodology for object-oriented programs that protects object structures against inconsistency due to race conditions. It is based on a recent methodology for single-threaded programs where developers define aggregate object structures using an ownership system and declare invariants over them. The methodology is supported by a set of language elements and by both a sound modular static verification method and run-time checking support. The paper reports on preliminary experience with a prototype implementation.},
publisher = {IEEE Computer Society},
url = {http://approjects.co.za/?big=en-us/research/publication/safe-concurrency-for-aggregate-objects-with-invariants/},
pages = {137-147},
isbn = {0-7695-2435-4},
edition = {SEFM},
}