{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:33:33Z","timestamp":1725521613570},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540893295"},{"type":"electronic","value":"9783540893301"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-89330-1_13","type":"book-chapter","created":{"date-parts":[[2008,11,27]],"date-time":"2008-11-27T02:43:37Z","timestamp":1227753817000},"page":"171-187","source":"Crossref","is-referenced-by-count":25,"title":["Reasoning about Java\u2019s Reentrant Locks"],"prefix":"10.1007","author":[{"given":"Christian","family":"Haack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cl\u00e9ment","family":"Hurlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-39656-7_1","volume-title":"Formal Methods for Components and Objects","author":"E. \u00c1brah\u00e1m","year":"2003","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Tool-supported proof system for multithreaded Java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 1\u201332. Springer, Heidelberg (2003)"},{"key":"13_CR2","unstructured":"Andrews, G.: Concurrent Programming: Principles and Practice. Benjamin\/Cummings (1991)"},{"key":"13_CR3","doi-asserted-by":"crossref","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) (2004)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"13_CR4","volume-title":"Principles of Programming Languages","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., O\u2019Hearn, P.W., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages. ACM Press, New York (2005)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (2002)","DOI":"10.1145\/582419.582440"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"13_CR7","series-title":"ACM SIGPLAN Notices","volume-title":"ACM Conference on Object-Oriented Programming Systems, Languages, and Applications","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM SIGPLAN Notices, vol.\u00a033(10). ACM Press, New York (1998)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"de Boer, F.S.: A sound and complete shared-variable concurrency model for multi-threaded Java programs. In: International Conference on Formal Methods for Open Object-based Distributed Systems (2007)","DOI":"10.1007\/978-3-540-72952-5_16"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming (2004)","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Asian Programming Languages and Systems Symposium (2007)","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java\u2019s reentrant locks. Technical Report ICIS-R08014, Radboud University Nijmegen (2008)","DOI":"10.1007\/978-3-540-89330-1_13"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C. Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A., Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (2001)","DOI":"10.1145\/360204.375719"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: International Conference on Formal Engineering Methods (2006)","DOI":"10.1007\/11901433_23"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-45651-1_6","volume-title":"Modular Specification and Verification of Object-Oriented Programs","year":"2002","unstructured":"M\u00fcller, P. (ed.): Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262, p. 195. Springer, Heidelberg (2002)"},{"key":"13_CR17","volume-title":"Java Generics","author":"M. Naftalin","year":"2006","unstructured":"Naftalin, M., Wadler, P.: Java Generics. O\u2019Reilly, Sebastopol (2006)"},{"issue":"1\u20133","key":"13_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science\u00a0375(1\u20133), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2) (1999)","DOI":"10.2307\/421090"},{"key":"13_CR20","unstructured":"Parkinson, M.: Local Reasoning for Java. Ph.D thesis, University of Cambridge (2005)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"13_CR22","volume-title":"Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark. IEEE Press, Los Alamitos (2002)"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Wadler, P.: A taste of linear logic. In: Mathematical Foundations of Computer Science (1993)","DOI":"10.1007\/3-540-57182-5_12"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89330-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T19:47:18Z","timestamp":1557949638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89330-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540893295","9783540893301"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89330-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}