{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:49:08Z","timestamp":1742939348192,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_27","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"355-372","source":"Crossref","is-referenced-by-count":2,"title":["Semantics for Locking Specifications"],"prefix":"10.1007","author":[{"given":"Michael D.","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damiano","family":"Macedonio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Merro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fausto","family":"Spoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"issue":"2","key":"27_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1119479.1119480","volume":"28","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Flanagan, C., Freund, S.: Types for safe locking: static race detection for Java. ACM TOPLAS 28(2), 207\u2013255 (2006)","journal-title":"ACM TOPLAS"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 2303, pp. 5\u201320. Springer, Heidelberg (2002)"},{"key":"27_CR3","unstructured":"Bandera: About Bandera. http:\/\/bandera.projects.cis.ksu.edu"},{"issue":"7","key":"27_CR4","first-page":"82","volume":"82","author":"GM Bierman","year":"2003","unstructured":"Bierman, G.M., Parkinson, M.J.: Effects and effect inference for a core java calculus. ENTCS 82(7), 82\u2013107 (2003)","journal-title":"ENTCS"},{"issue":"6","key":"27_CR5","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1145\/945885.945886","volume":"25","author":"B Blanchet","year":"2003","unstructured":"Blanchet, B.: Escape analysis for java: theory and practice. ACM TOPLAS 25(6), 713\u2013775 (2003)","journal-title":"ACM TOPLAS"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Bogdanas, D., Rosu, G.: K-java: a complete semantics of java. In: ACM SIGPLAN-SIGACT POPL, pp. 445\u2013456, Mumbai, India (2015)","DOI":"10.1145\/2676726.2676982"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0000464","volume-title":"Algebraic Methodology and Software Technology","author":"P Cenciarelli","year":"1997","unstructured":"Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: From sequential to multi-threaded java: an event-based operational semantics. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 75\u201390. Springer, Heidelberg (1997)"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Taylor, R.N., Gall, H.C. (eds.) ICSE 2011 (2011)","DOI":"10.1145\/1985793.1985889"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Macedonio, D., Merro, M., Spoto, F.: Semantics for locking specifications. CoRR abs\/1501.05338 (2015)","DOI":"10.1007\/978-3-319-40648-0_27"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Ernst, M., Lovato, A., Macedonio, D., Spoto, F., Thaine, J.: Locking discipline inference and checking. In: ICSE 2016, Austin, TX, USA (2016)","DOI":"10.1145\/2884781.2884882"},{"key":"27_CR11","volume-title":"Java Concurrency in Practice","author":"B Goetz","year":"2006","unstructured":"Goetz, B., Peierls, T., Bloch, J., Bowbeer, J.: Java Concurrency in Practice. Addison Wesley, Boston (2006)"},{"key":"27_CR12","unstructured":"Google: Guava: Google Core Libraries for Java 1.6+. https:\/\/code.google.com\/p\/guava-libraries"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 - Concurrency Theory","author":"J Hatcliff","year":"2001","unstructured":"Hatcliff, J., Dwyer, M.B.: Using the bandera tool set to model-check properties of concurrent java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 39. Springer, Heidelberg (2001)"},{"issue":"3","key":"27_CR14","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/503502.503505","volume":"23","author":"A Igarashi","year":"2001","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight java: a minimal core calculus for Java and GJ. ACM TOPLAS 23(3), 396\u2013450 (2001)","journal-title":"ACM TOPLAS"},{"key":"27_CR15","unstructured":"Javadoc for @GuardedBy. https:\/\/jsr-305.googlecode.com\/svn\/trunk\/javadoc\/javax\/annotation\/concurrent\/GuardedBy.html"},{"key":"27_CR16","unstructured":"Julia, S.: The Julia Static Analyzer. http:\/\/www.juliasoft.com\/julia"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Long, B., Long, B.W.: Formal specification of java concurrency to assist software verification. In: Dongarra, J. (ed.) IPDPS 2003. IEEE Computer Society (2003)","DOI":"10.1109\/IPDPS.2003.1213262"},{"key":"27_CR18","unstructured":"NASA: Java PathFinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/978-3-642-32943-2_6","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"DJ Nikoli\u0107","year":"2012","unstructured":"Nikoli\u0107, D.J., Spoto, F.: Definite expression aliasing analysis for java bytecode. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 74\u201389. Springer, Heidelberg (2012)"},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-642-13953-6_6","volume-title":"Objects, Models, Components, Patterns","author":"J \u00d6stlund","year":"2010","unstructured":"\u00d6stlund, J., Wrigstad, T.: Welterweight java. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 97\u2013116. Springer, Heidelberg (2010)"},{"key":"27_CR21","first-page":"146","volume-title":"OOPSLA 1991","author":"J Palsberg","year":"1991","unstructured":"Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Paepcke, A. (ed.) OOPSLA 1991, pp. 146\u2013161. ACM SIGPLAN Notices, ACM, New York (1991)"},{"key":"27_CR22","unstructured":"Pech, V.: Concurrency is hot, try the JCIP annotations (2010). http:\/\/jetbrains.dzone.com\/tips\/concurrency-hot-try-jcip"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T03:11:28Z","timestamp":1567998688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}