{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:34:28Z","timestamp":1761323668601},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_23","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"427-447","source":"Crossref","is-referenced-by-count":39,"title":["Verifying a Compiler for Java Threads"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1006\/inco.1996.0047","volume":"127","author":"L. Aceto","year":"1996","unstructured":"Aceto, L., van Glabbeek, R.J., Fokkink, W., Ing\u00f3lfsd\u00f3ttir, A.: Axiomatizing prefix iteration with silent steps. Information and Computation\u00a0127(1), 26\u201340 (1996)","journal-title":"Information and Computation"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523. Springer, Heidelberg (1999)"},{"key":"23_CR3","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., \u0160ev\u010d\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)"},{"issue":"3","key":"23_CR4","doi-asserted-by":"crossref","first-page":"71","DOI":"10.5381\/jot.2007.6.3.a2","volume":"6","author":"N. Belblidia","year":"2007","unstructured":"Belblidia, N., Debbabi, M.: A dynamic operational semantics for JVML. Journal of Object Technology\u00a06(3), 71\u2013100 (2007)","journal-title":"Journal of Object Technology"},{"key":"23_CR5","first-page":"77","volume-title":"IFIP 1987, Formal Description of Programming Concepts III","author":"J.A. Bergstra","year":"1987","unstructured":"Bergstra, J.A., Klop, J.W., Olderog, E.R.: Failures without chaos: a new process semantics for fair abstraction. In: IFIP 1987, Formal Description of Programming Concepts III, pp. 77\u2013103. Elsevier Science Publishing, Amsterdam (1987)"},{"issue":"6","key":"23_CR6","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes\u00a028(6), 2 (2003)","journal-title":"SIGSOFT Software Engineering Notes"},{"issue":"4","key":"23_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1377492.1377495","volume":"30","author":"C. Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: Static checking and inference for Java. ACM TOPLAS\u00a030(4), 1\u201353 (2008)","journal-title":"ACM TOPLAS"},{"key":"23_CR8","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"issue":"6","key":"23_CR9","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C. Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security\u00a08(6), 399\u2013422 (2009)","journal-title":"International Journal of Information Security"},{"key":"23_CR10","unstructured":"Huisman, M., Petri, G.: BicolanoMT: a formalization of multi-threaded Java at bytecode level. In: BYTECODE 2008. ENTCS (2008)"},{"key":"23_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 TOPLAS\u00a028, 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"23_CR12","unstructured":"Leinenbach, D.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University (2008)"},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler backend or: Programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM, New York (2006)"},{"issue":"7","key":"23_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"issue":"4","key":"23_CR15","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR16","volume-title":"The Java Virtual Machine Specification, Second Edition","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, Second Edition. Addison-Wesley, Reading (1999)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Liu, H., Moore, J.S.: Executable JVM Model for Analytical Reasoning: A Study. In: IVME 2003, pp. 15\u201323 (2003)","DOI":"10.1145\/858570.858572"},{"key":"23_CR18","unstructured":"Lochbihler, A.: Type safe nondeterminism - a formal semantics of Java threads. In: FOOL 2008 (2008)"},{"key":"23_CR19","unstructured":"Lochbihler, A.: Jinja with threads. In: The Archive of Formal Proofs (2009), \n                  \n                    http:\/\/afp.sf.net\/devel-entries\/JinjaThreads.shtml\n                  \n                  \n                 (Formal proof development)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/3-540-10828-9_52","volume-title":"CAAP \u201981","author":"R. Milner","year":"1981","unstructured":"Milner, R.: A modal characterisation of observable machine-behaviour. In: Astesiano, E., B\u00f6hm, C. (eds.) CAAP 1981. LNCS, vol.\u00a0112, pp. 25\u201334. Springer, Heidelberg (1981)"},{"key":"23_CR21","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)"},{"key":"23_CR22","series-title":"Journal of Automated Reasoning","volume-title":"Special Issue on Java Bytecode Verification","year":"2003","unstructured":"Nipkow, T. (ed.): Special Issue on Java Bytecode Verification. Journal of Automated Reasoning, vol.\u00a030(3-4). Springer, Heidelberg (2003)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"23_CR24","unstructured":"Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, G\u00f6teborg University (1988)"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-70592-5_3","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"J. \u0160ev\u010d\u00edk","year":"2008","unstructured":"\u0160ev\u010d\u00edk, J., Aspinall, D.: On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 27\u201351. Springer, Heidelberg (2008)"},{"key":"23_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R.F. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer, Heidelberg (2001)"},{"key":"23_CR27","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/224164.224193","volume-title":"FPCA 1995","author":"M. Wand","year":"1995","unstructured":"Wand, M.: Compiler correctness for parallel languages. In: FPCA 1995, pp. 120\u2013134. ACM, New York (1995)"},{"key":"23_CR28","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1554339.1554345","volume-title":"PLAS 2009","author":"D. Wasserrab","year":"2009","unstructured":"Wasserrab, D., Lohner, D., Snelting, G.: On PDG-based noninterference and its modular proof. In: PLAS 2009, pp. 31\u201344. ACM, New York (2009)"}],"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-642-11957-6_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:45Z","timestamp":1606185945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}