{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T06:33:26Z","timestamp":1743143606037,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_16","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"212-227","source":"Crossref","is-referenced-by-count":7,"title":["A Certified Data Race Analysis for a Java-like Language"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Dabrowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"AMD. Amd64 architecture programmer\u2019s manual volume 2: System programming. Technical Report 24593 (2007)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-74591-4_4","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Sevc\u00edk, J.: Formalising java\u2019s data race free guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 22\u201337. Springer, Heidelberg (2007)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: preventing data races and deadlocks. In: ACM Press (ed.) Proc. of OOPSLA 2002, New York, NY, USA, pp. 211\u2013230 (2002)","DOI":"10.1145\/583854.582440"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: ACM Press (ed.) Proc. of OOPSLA 2001, New York, NY, USA, pp. 56\u201369 (2001)","DOI":"10.1145\/504311.504287"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-49099-X_7","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"1999","unstructured":"Flanagan, C., Abadi, M.: Types for safe locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 91\u2013108. Springer, Heidelberg (1999)"},{"issue":"1","key":"16_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.tcs.2005.06.004","volume":"342","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science\u00a0342(1), 56\u201378 (2005)","journal-title":"Theoretical Computer Science"},{"key":"16_CR7","first-page":"219","volume-title":"Proc. of PLDI 2000","author":"C. Flanagan","year":"2000","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for java. In: Proc. of PLDI 2000, pp. 219\u2013232. ACM Press, New York (2000)"},{"key":"16_CR8","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.W., Zappa Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"16_CR9","unstructured":"Huisman, M., Petri, G.: The Java memory model: a formal explanation. In: Verification and Analysis of Multi-threaded Java-like Programs, VAMP (2007) (to appear)"},{"key":"16_CR10","unstructured":"Intel. Intel 64 architecture memory ordering white paper. Technical Report SKU 318147-001 (2007)"},{"issue":"4","key":"16_CR11","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR12","unstructured":"Lammich, P., M\u00fcller-Olm, M.: Formalization of conflict analysis of programs with procedures, thread creation, and monitors. In: The Archive of Formal Proofs (2007)"},{"key":"16_CR13","first-page":"42","volume-title":"Proc. of POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proc. of POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"16_CR14","volume-title":"Safeware: system safety and computers","author":"N.G. Leveson","year":"1995","unstructured":"Leveson, N.G.: Safeware: system safety and computers. ACM, NY (1995)"},{"key":"16_CR15","first-page":"378","volume-title":"Proc. of POPL 2005","author":"J. Manson","year":"2005","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: Proc. of POPL 2005, pp. 378\u2013391. ACM Press, New York (2005)"},{"key":"16_CR16","unstructured":"Naik, M.: Effective Static Data Race Detection For Java. PhD thesis, Standford University (2008)"},{"key":"16_CR17","first-page":"327","volume-title":"Proc. of POPL 2007","author":"M. Naik","year":"2007","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proc. of POPL 2007, pp. 327\u2013338. ACM Press, New York (2007)"},{"key":"16_CR18","first-page":"308","volume-title":"Proc. of PLDI 2006","author":"M. Naik","year":"2006","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for java. In: Proc. of PLDI 2006, pp. 308\u2013319. ACM Press, New York (2006)"},{"key":"16_CR19","unstructured":"Petri, G., Huisman, M.: BicolanoMT: a formalization of multi-threaded Java at bytecode level. In: Bytecode 2008. Electronic Notes in Theoretical Computer Science (2008)"},{"key":"16_CR20","unstructured":"Poulsen, K.: Tracking the blackout bug (2004)"},{"key":"16_CR21","unstructured":"Sun Microsystems, Inc. JSR 133 Expert Group, Java Memory Model and Thread Specification Revision (2004)"},{"key":"16_CR22","first-page":"131","volume-title":"Proc. of PLDI 2004","author":"J. Whaley","year":"2004","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Proc. of PLDI 2004, pp. 131\u2013144. ACM, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:13:37Z","timestamp":1558268017000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}