loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
Safe Concurrency for Aggregate Objects with Invariants
Koblenz, Germany
September 07-September 09
ISBN: 0-7695-2435-4
ASCII Text
x 
 
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, "Safe Concurrency for Aggregate Objects with Invariants," Software Engineering and Formal Methods, IEEE International Conference on, pp. 137-147, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/SEFM.2005.39,
author = {Bart Jacobs and K. Rustan M. Leino and Frank Piessens and Wolfram Schulte},
title = {Safe Concurrency for Aggregate Objects with Invariants},
journal ={Software Engineering and Formal Methods, IEEE International Conference on},
volume = {0},
year = {2005},
isbn = {0-7695-2435-4},
pages = {137-147},
doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.39},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Software Engineering and Formal Methods, IEEE International Conference on
TI - Safe Concurrency for Aggregate Objects with Invariants
SN - 0-7695-2435-4
SP137
EP147
A1 - Bart Jacobs,
A1 - K. Rustan M. Leino,
A1 - Frank Piessens,
A1 - Wolfram Schulte,
PY - 2005
KW - null
VL - 0
JA - Software Engineering and Formal Methods, IEEE International Conference on
ER -
 
Bart Jacobs, Katholieke Universiteit Leuven Celestijnenlaan, Belgium
K. Rustan M. Leino, Microsoft Research, Redmond, WA., USA
Frank Piessens, Katholieke Universiteit Leuven Celestijnenlaan, Belgium
Wolfram Schulte, Microsoft Research, Redmond, WA., USA
Developing safe multithreaded software systems is diffi- cult 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.
Citation:
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, "Safe Concurrency for Aggregate Objects with Invariants," sefm, pp.137-147, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.