{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:05:13Z","timestamp":1725473113427},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_23","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"420-439","source":"Crossref","is-referenced-by-count":22,"title":["A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Smans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)"},{"key":"23_CR2","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI 2002","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002. SIGPLAN Notices, vol.\u00a037, pp. 234\u2013245. ACM Press, New York (2002)"},{"issue":"6","key":"23_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.5381\/jot.2004.3.6.a4","volume":"3","author":"S.N. Freund","year":"2004","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology\u00a03(6), 81\u2013101 (2004)","journal-title":"Journal of Object Technology"},{"key":"23_CR4","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/964001.964022","volume-title":"POPL 2004","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: POPL 2004. SIGPLAN Notices, vol.\u00a039, pp. 245\u2013255. ACM Press, New York (2004)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-45931-6_2","volume-title":"Foundations of Software Science and Computation Structures","author":"E. \u00c1brah\u00e1m-Mumm","year":"2002","unstructured":"\u00c1brah\u00e1m-Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: Verification for Java\u2019s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 5\u201320. Springer, Heidelberg (2002)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/11531142_24","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"E. Rodr\u00edguez","year":"2005","unstructured":"Rodr\u00edguez, E., Dwyer, M., Flanagan, C., Hatcliff, J., Leavens, G.T.: Extending sequential specification techniques for modular specification and verification of multi-threaded programs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 551\u2013576. Springer, Heidelberg (2005)"},{"key":"23_CR7","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/582419.582440","volume-title":"OOPSLA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA 2002. SIGPLAN Notices, vol.\u00a037, pp. 211\u2013230. ACM, New York (2002)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/781131.781169","volume-title":"PLDI 2003","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI 2003, pp. 338\u2013349. ACM, New York (2003)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (to appear, 2006)"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/SEFM.2005.39","volume-title":"Proc. Int. Conf. Software Engineering and Formal Methods (SEFM 2005)","author":"B. Jacobs","year":"2005","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Proc. Int. Conf. Software Engineering and Formal Methods (SEFM 2005), pp. 137\u2013146. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"6","key":"23_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"23_CR13","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/964001.964023","volume-title":"POPL 2004","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: POPL 2004. SIGPLAN Notices, vol.\u00a039, pp. 256\u2013267. ACM, New York (2004)"},{"issue":"10","key":"23_CR14","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C.A.R. Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: An operating system structuring concept. Communications of the ACM\u00a017(10), 549\u2013557 (1974)","journal-title":"Communications of the ACM"},{"issue":"4","key":"23_CR15","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Transactions on Computer Systems"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-540-24851-4_24","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"A. Welc","year":"2004","unstructured":"Welc, A., Jagannathan, S., Hosking, A.L.: Transactional monitors for concurrent objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 518\u2013541. Springer, Heidelberg (2004)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants: Soundness proof. Technical Report MSR-TR-2005-85, Microsoft Research (2005)","DOI":"10.1109\/SEFM.2005.39"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:37:05Z","timestamp":1619509025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11901433_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}