{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:40Z","timestamp":1763467900849,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>\n            Reasoning about multithreaded object-oriented programs is difficult, due to the nonlocal nature of object aliasing and data races. We propose a programming regime (or\n            <jats:italic>programming model<\/jats:italic>\n            ) that rules out data races, and enables local reasoning in the presence of object aliasing and concurrency. Our programming model builds on the multithreading and synchronization primitives as they are present in current mainstream programming languages. Java or C# programs developed according to our model can be annotated by means of stylized comments to make the use of the model explicit. We show that such annotated programs can be formally verified to comply with the programming model. If the annotated program verifies, the underlying Java or C# program is guaranteed to be free from data races, and it is sound to reason locally about program behavior. Verification is modular: a program is valid if all methods are valid, and validity of a method does not depend on program elements that are not visible to the method. We have implemented a verifier for programs developed according to our model in a custom build of the Spec# programming system, and we have validated our approach on a case study.\n          <\/jats:p>","DOI":"10.1145\/1452044.1452045","type":"journal-article","created":{"date-parts":[[2008,12,10]],"date-time":"2008-12-10T15:32:31Z","timestamp":1228923151000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A programming model for concurrent object-oriented programs"],"prefix":"10.1145","volume":"31","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[{"name":"Katholieke Universiteit Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Smans","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,12,12]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS), M. Nielsen and U. Engberg, Eds. Lecture Notes in Computer Science","volume":"2303","author":"\u00c1brah\u00e1m-Mumm E.","unstructured":"\u00c1brah\u00e1m-Mumm , E. , de Boer , F. S. , de Roever , W.-P. , and Steffen , M . 2002. Verification for Java's reentrant multithreading concept . In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS), M. Nielsen and U. Engberg, Eds. Lecture Notes in Computer Science , vol. 2303 . Springer, 5--20. \u00c1brah\u00e1m-Mumm, E., de Boer, F. S., de Roever, W.-P., and Steffen, M. 2002. Verification for Java's reentrant multithreading concept. In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS), M. Nielsen and U. Engberg, Eds. Lecture Notes in Computer Science, vol. 2303. Springer, 5--20."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582440"},{"key":"e_1_2_1_6_1","unstructured":"Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. Res. Rep. 159 Compaq Systems Research Center.  Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. Res. Rep. 159 Compaq Systems Research Center."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964023"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.006"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512558"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a4"},{"key":"e_1_2_1_12_1","unstructured":"Gosling J. Joy B. Steele G. and Bracha G. 2005. The Java Language Specification (3rd Edition). Prentice Hall.   Gosling J. Joy B. Steele G. and Bracha G. 2005. The Java Language Specification (3rd Edition). Prentice Hall."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.39"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Jacobs B. Leino K. R. M. Piessens F. and Schulte W. 2005b. Safe concurrency for aggregate objects with invariants: Soundness proof. Tech. rep. MSR-TR-2005-85 Microsoft Research.  Jacobs B. Leino K. R. M. Piessens F. and Schulte W. 2005b. Safe concurrency for aggregate objects with invariants: Soundness proof. Tech. rep. MSR-TR-2005-85 Microsoft Research.","DOI":"10.1109\/SEFM.2005.39"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_23"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964022"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science","volume":"3086","author":"Welc A.","unstructured":"Welc , A. , Jagannathan , S. , and Hosking , A. L . 2004. Transactional monitors for concurrent objects . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science , vol. 3086 . Springer, 519--542. Welc, A., Jagannathan, S., and Hosking, A. L. 2004. Transactional monitors for concurrent objects. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science, vol. 3086. Springer, 519--542."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452045","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1452044.1452045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:06Z","timestamp":1750253406000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1145\/1452044.1452045"],"URL":"https:\/\/doi.org\/10.1145\/1452044.1452045","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2008,12]]},"assertion":[{"value":"2007-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}