The Community for Technology Leaders
RSS Icon
Subscribe
Koblenz, Germany
Sept. 7, 2005 to Sept. 9, 2005
ISBN: 0-7695-2435-4
pp: 137-147
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
ABSTRACT
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.
INDEX TERMS
null
CITATION
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, "Safe Concurrency for Aggregate Objects with Invariants", SEFM, 2005, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) 2005, pp. 137-147, doi:10.1109/SEFM.2005.39
37 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool