{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:04:50Z","timestamp":1750089890599,"version":"3.37.3"},"reference-count":87,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,2,8]],"date-time":"2018-02-08T00:00:00Z","timestamp":1518048000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Sn11\/10-1","SN11\/10-2"],"award-info":[{"award-number":["Sn11\/10-1","SN11\/10-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9452-x","type":"journal-article","created":{"date-parts":[[2018,2,7]],"date-time":"2018-02-07T23:18:55Z","timestamp":1518045535000},"page":"243-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5851-494X","authenticated-orcid":false,"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,8]]},"reference":[{"issue":"1","key":"9452_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. Inf. Comput. 127(1), 26\u201340 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0047","journal-title":"Inf. Comput."},{"key":"9452_CR2","doi-asserted-by":"publisher","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java, LNCS, vol. 1523. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48737-9","DOI":"10.1007\/3-540-48737-9"},{"key":"9452_CR3","doi-asserted-by":"publisher","unstructured":"Backes, M., Busenius, A., Hri\u0163cu, C.: On the development and formalization of an extensible code generator for real life security protocols. In: Goodloe, A.E., Person, S. (eds.) NFM 2012, LNCS, vol. 7226, pp. 371\u2013387. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_34","DOI":"10.1007\/978-3-642-28891-3_34"},{"issue":"2","key":"9452_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"9452_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de\u00a0Boer, F., Bonsangue, M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, LNCS, vol. 5382, pp. 1\u201324. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_1","DOI":"10.1007\/978-3-540-92188-2_1"},{"key":"9452_CR6","doi-asserted-by":"publisher","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015, LNCS, vol. 9032, pp. 283\u2013307. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12","DOI":"10.1007\/978-3-662-46669-8_12"},{"issue":"3","key":"9452_CR7","doi-asserted-by":"publisher","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. J. Object Technol. 6(3), 71\u2013100 (2007)","journal-title":"J. Object Technol."},{"key":"9452_CR8","doi-asserted-by":"publisher","unstructured":"Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: COCV 2003, ENTCS, vol. 82(2), pp. 377\u2013394 (2003). https:\/\/doi.org\/10.1016\/S1571-0661(05)82598-8","DOI":"10.1016\/S1571-0661(05)82598-8"},{"key":"9452_CR9","unstructured":"Bergstra, J.A., Klop, J.W., Olderog, E.R.: Failures without chaos: a new process semantics for fair abstraction. In: Formal Description of Programming Concepts III (IFIP 1987), pp. 77\u2013103. Elsevier Science Publishing (1987)"},{"key":"9452_CR10","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 131\u2013146. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"9452_CR11","doi-asserted-by":"publisher","unstructured":"Bogd\u0103na\u015f, D., Ro\u015fu, G.: K-Java: A complete semantics of Java. In: POPL 2015, pp. 445\u2013456. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"9452_CR12","doi-asserted-by":"publisher","unstructured":"Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: On improvements of low-deterministic security. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016, LNCS, vol. 9635, pp. 68\u201388. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-662-49635-0_4","DOI":"10.1007\/978-3-662-49635-0_4"},{"key":"9452_CR13","unstructured":"Connected limited device configuration (CLDC) specification 1.1. http:\/\/jcp.org\/aboutJava\/communityprocess\/final\/jsr139\/index.html"},{"key":"9452_CR14","doi-asserted-by":"crossref","unstructured":"Czarnik, P., Schubert, A.: Extending operational semantics of the Java bytecode. In: Barthe, G., Fournet, C. (eds.) TGC 2008, LNCS, vol. 4912, pp. 57\u201372. Springer (2008)","DOI":"10.1007\/978-3-540-78663-4_6"},{"issue":"6","key":"9452_CR15","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"MA Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2\u20132 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"9452_CR16","doi-asserted-by":"publisher","unstructured":"Drossopoulou, S., Eisenbach, S.: Describing the semantics of Java and proving type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java, LNCS, vol. 1523, pp. 542\u2013542. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48737-9_2","DOI":"10.1007\/3-540-48737-9_2"},{"key":"9452_CR17","doi-asserted-by":"publisher","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D. (eds.) CAV 2004, LNCS, vol. 3114, pp. 501\u2013505. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_46","DOI":"10.1007\/978-3-540-27813-9_46"},{"key":"9452_CR18","doi-asserted-by":"publisher","unstructured":"Farzan, A., Meseguer, J., Ro\u015fu, G.: Formal JVM code analysis in Java FAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004, LNCS, vol. 3116, pp. 132\u2013147. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27815-3_14","DOI":"10.1007\/978-3-540-27815-3_14"},{"issue":"4","key":"9452_CR19","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 Trans. Program. Lang. Syst. 30(4), 1\u201353 (2008). https:\/\/doi.org\/10.1145\/1377492.1377495","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9452_CR20","unstructured":"Giffhorn, D.: Slicing of concurrent programs and its application to information flow control. Ph.D. thesis, Fakult\u00e4t f\u00fcr Informatik, Karlsruher Institut f\u00fcr Technologie (2012)"},{"key":"9452_CR21","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A.: The Java Language Specification: Java SE 8 Edition. Oracle America, Inc. (2015)"},{"key":"9452_CR22","doi-asserted-by":"publisher","unstructured":"Goto, M., Jagadeesan, R., Pitcher, C., Riely, J.: Types for relaxed memory models. In: TLDI 2012, pp. 25\u201338. ACM (2012). https:\/\/doi.org\/10.1145\/2103786.2103791","DOI":"10.1145\/2103786.2103791"},{"key":"9452_CR23","doi-asserted-by":"publisher","unstructured":"Grossman, D.: Type-safe multithreading in Cyclone. In: TLDI 2003, pp. 13\u201325. ACM (2003). https:\/\/doi.org\/10.1145\/604174.604177","DOI":"10.1145\/604174.604177"},{"key":"9452_CR24","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"PH Hartel","year":"2001","unstructured":"Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Comput. Surv. 33, 517\u2013558 (2001). https:\/\/doi.org\/10.1145\/503112.503115","journal-title":"ACM Comput. Surv."},{"key":"9452_CR25","unstructured":"Huisman, M., Petri, G.: BicolanoMT: a formalization of multi-threaded Java at bytecode level. In: BYTECODE 2008, Electronic Notes in Theoretical Computer Science (2008)"},{"key":"9452_CR26","unstructured":"Java platform, standard edition 8 API specification (2014). http:\/\/docs.oracle.com\/javase\/8\/docs\/api\/"},{"key":"9452_CR27","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194\u2013206. ACM (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"9452_CR28","unstructured":"Klein, G.: Verified Java bytecode verification. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"issue":"13","key":"9452_CR29","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1002\/cpe.597","volume":"13","author":"G Klein","year":"2001","unstructured":"Klein, G., Nipkow, T.: Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. 13(13), 1133\u20131151 (2001)","journal-title":"Concurr. Comput. Pract. Exp."},{"issue":"3","key":"9452_CR30","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G Klein","year":"2002","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comput. Sci. 298(3), 583\u2013626 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(02)00869-1","journal-title":"Theor. Comput. Sci."},{"key":"9452_CR31","unstructured":"Klein, G., Nipkow, T.: Jinja is not Java. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http:\/\/www.isa-afp.org\/entries\/Jinja.shtml (2005). Formal proof development. Accessed 31 Jan 2018"},{"issue":"4","key":"9452_CR32","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 Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006). https:\/\/doi.org\/10.1145\/1146809.1146811","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9452_CR33","doi-asserted-by":"crossref","unstructured":"Klein, G., Nipkow, T., von Oheimb, D., Nieto, L.P., Schirmer, N., Strecker, M.: Java source and bytecode formalizations in Isabelle: Bali. Isabelle sources in Isabelle\/HOL\/Bali (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1\u20132","key":"9452_CR34","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.jlap.2003.07.004","volume":"58","author":"G Klein","year":"2004","unstructured":"Klein, G., Strecker, M.: Verified bytecode verification and type-certifying compilation. J. Log. Algebraic Program. 58(1\u20132), 27\u201360 (2004). https:\/\/doi.org\/10.1016\/j.jlap.2003.07.004","journal-title":"J. Log. Algebraic Program."},{"issue":"3\u20134","key":"9452_CR35","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1023\/A:1025095122199","volume":"30","author":"G Klein","year":"2003","unstructured":"Klein, G., Wildmoser, M.: Verified bytecode subroutines. J. Autom. Reason. 30(3\u20134), 363\u2013398 (2003). https:\/\/doi.org\/10.1023\/A:1025095122199","journal-title":"J. Autom. Reason."},{"key":"9452_CR36","unstructured":"Krebbers, R.: The C standard formalized in Coq. Ph.D. thesis, Radboud University Nijmegen (2015)"},{"key":"9452_CR37","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: POPL 2014, pp. 179\u2013191. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"issue":"9","key":"9452_CR38","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"9452_CR39","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler backend or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM (2006). https:\/\/doi.org\/10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"issue":"4","key":"9452_CR40","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. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9452_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1\u201331 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9099-0","journal-title":"J. Autom. Reason."},{"key":"9452_CR42","volume-title":"The Java Virtual Machine Specification","author":"T Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)","edition":"2"},{"key":"9452_CR43","doi-asserted-by":"publisher","unstructured":"Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. In: IVME 2003, pp. 15\u201323. ACM (2003). https:\/\/doi.org\/10.1145\/858570.858572","DOI":"10.1145\/858570.858572"},{"key":"9452_CR44","doi-asserted-by":"publisher","unstructured":"Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004, LNCS, vol. 3223, pp. 117\u2013125. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30142-4_14","DOI":"10.1007\/978-3-540-30142-4_14"},{"key":"9452_CR45","unstructured":"Lochbihler, A.: Jinja with threads. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http:\/\/www.isa-afp.org\/entries\/JinjaThreads.shtml (2007). Formal proof development"},{"key":"9452_CR46","unstructured":"Lochbihler, A.: Type safe nondeterminism\u2014a formal semantics of Java threads. In: Proceedings of the 2008 International Workshop on Foundations of Object-Oriented Languages (FOOL 2008) (2008)"},{"key":"9452_CR47","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010, LNCS, vol. 6012, pp. 427\u2013447. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_23","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"9452_CR48","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Java and the Java memory model\u2013a unified, machine-checked formalisation. In: Seidl, H. (ed.) ESOP 2012, LNCS, vol. 7211, pp. 497\u2013517. Springer (2012)","DOI":"10.1007\/978-3-642-28869-2_25"},{"key":"9452_CR49","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Ph.D. thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik (2012). https:\/\/doi.org\/10.5445\/KSP\/1000028867","DOI":"10.5445\/KSP\/1000028867"},{"issue":"4","key":"9452_CR50","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/2518191","volume":"35","author":"A Lochbihler","year":"2014","unstructured":"Lochbihler, A.: Making the Java memory model safe. ACM Trans. Program. Lang. Syst. 35(4), 12:1\u201312:65 (2014). https:\/\/doi.org\/10.1145\/2518191","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9452_CR51","doi-asserted-by":"publisher","unstructured":"Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen, M., Geuvers, H., Schmalz, J., Wiedijk, F. (eds.) ITP 2011, LNCS, vol. 6898, pp. 216\u2013232. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_17","DOI":"10.1007\/978-3-642-22863-6_17"},{"issue":"1","key":"9452_CR52","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/32.481534","volume":"22","author":"J McLean","year":"1996","unstructured":"McLean, J.: A general theory of composition for a class of \u201cpossibilistic\u201d properties. IEEE Trans. Softw. Eng. 22(1), 53\u201367 (1996). https:\/\/doi.org\/10.1109\/32.481534","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9452_CR53","doi-asserted-by":"publisher","unstructured":"Milner, R.: A modal characterisation of observable machine-behaviour. In: Astesiano, E., B\u00f6hm, C. (eds.) CAAP 1981, LNCS, vol. 112, pp. 25\u201334. Springer (1981). https:\/\/doi.org\/10.1007\/3-540-10828-9_52","DOI":"10.1007\/3-540-10828-9_52"},{"key":"9452_CR54","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)"},{"key":"9452_CR55","unstructured":"Mobius consortium. Deliverable D3.1. Byte code level specification language and program logic (2006)"},{"issue":"3","key":"9452_CR56","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/514188.514189","volume":"24","author":"JS Moore","year":"2002","unstructured":"Moore, J.S., Porter, G.: The apprentice challenge. ACM Trans. Program. Lang. Syst. 24(3), 193\u2013216 (2002). https:\/\/doi.org\/10.1145\/514188.514189","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9452_CR57","unstructured":"Moser, G., Schaper, M.: From Jinja bytecode to term rewriting: a complexity reflecting transformation. Inf. Comput. (to appear). http:\/\/cbr.uibk.ac.at\/publications\/ic16.pdf"},{"key":"9452_CR58","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001, LNCS, vol. 2030, pp. 347\u2013363. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_23","DOI":"10.1007\/3-540-45315-6_23"},{"key":"9452_CR59","doi-asserted-by":"publisher","unstructured":"Nipkow, T., von Oheimb, D.: Java $$_{{\\ell }ight}$$ \u2113 i g h t is type-safe\u2014definitely. In: POPL 1998, pp. 161\u2013170. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268960","DOI":"10.1145\/268946.268960"},{"key":"9452_CR60","unstructured":"Nipkow, T., von Oheimb, D., Pusch, C.: $$\\mu $$ \u03bc Java: embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbr\u00fcggen, R. (eds.) Foundations of Secure Computation, NATO Science Series F: Computer and Systems Sciences, vol. 175, pp. 117\u2013144. IOS Press (2000)"},{"key":"9452_CR61","unstructured":"Norrish, M.: A formal semantics for C++. Tech. rep., NICTA (2008). Available from http:\/\/nicta.com.au\/people\/norrishm\/attachments\/bibliographies_and_papers\/C-TR.pdf"},{"key":"9452_CR62","unstructured":"Oheimb, D.v.: Analyzing Java in Isabelle\/HOL. formalization, type safety and hoare logic. Ph.D. thesis, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2000). http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2001\/oheimb.html"},{"key":"9452_CR63","doi-asserted-by":"crossref","unstructured":"Oheimb, D.v.: Hoare logic for Java in Isabelle\/HOL. Concurr. Comput. Pract. Exp. 13(13), 1173\u20131214 (2001).","DOI":"10.1002\/cpe.598"},{"key":"9452_CR64","doi-asserted-by":"crossref","unstructured":"Oheimb, D.v., Nipkow, T.: Machine-checking the Java specification: proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java, LNCS, vol. 1523, pp. 119\u2013156. Springer (1999)","DOI":"10.1007\/3-540-48737-9_4"},{"key":"9452_CR65","doi-asserted-by":"publisher","unstructured":"Oheimb, D.v., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.H., Lindsay, P. (eds.) FME 2002, LNCS, vol. 2391, pp. 89\u2013105. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_6","DOI":"10.1007\/3-540-45614-7_6"},{"key":"9452_CR66","doi-asserted-by":"publisher","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016, LNCS, vol. 9632, pp. 589\u2013615. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"9452_CR67","doi-asserted-by":"publisher","unstructured":"Pusch, C.: Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In: Cleaveland, R. (ed.) TACAS 1999, LNCS, vol. 1579, pp. 89\u2013103. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_7","DOI":"10.1007\/3-540-49059-0_7"},{"key":"9452_CR68","unstructured":"Quis custodiet\u2014machine-checked software security analyses. https:\/\/pp.info.uni-karlsruhe.de\/projects\/quis-custodiet\/"},{"key":"9452_CR69","doi-asserted-by":"publisher","unstructured":"Ramananandro, T., Dos\u00a0Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. In: POPL 2011, pp. 67\u201380. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926395","DOI":"10.1145\/1926385.1926395"},{"key":"9452_CR70","unstructured":"Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, G\u00f6teborg University (1988)"},{"issue":"6","key":"9452_CR71","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","journal-title":"J. Log. Algebraic Program."},{"key":"9452_CR72","unstructured":"Rushby, J.: Formal methods and the certification of critical systems. Tech. Rep. SRI-CSL-93-7, Computer Science Laboratory, SRI International (1993). http:\/\/www.csl.sri.com\/papers\/csl-93-7\/"},{"key":"9452_CR73","unstructured":"Sampson, J., Boehm, H., Otenko, O., Levart, P., Holmes, D., Haley, A., Buchholz, M., Lea, D., Davidovich, V., Terekhov, A., Diestelhorst, S.: Varieties of CAS semantics (another doc fix request). Thread the on concurrency-interest mailing list, first post at http:\/\/altair.cs.oswego.edu\/pipermail\/concurrency-interest\/2015-January\/013613.html (2015). Accessed 17 Oct 2017"},{"key":"9452_CR74","unstructured":"Schirmer, N.: Java definite assignment in Isabelle\/HOL. In: Proceedings of ECOOP Workshop on Formal Techniques for Java-like Programs. Technical Report 408, ETH Zurich (2003)"},{"key":"9452_CR75","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1002\/cpe.800","volume":"16","author":"N Schirmer","year":"2004","unstructured":"Schirmer, N.: Analysing the Java package\/access concepts in Isabelle\/HOL. Concurr. Comput. Pract. Exp\u2013Form. Tech. Java Program. 16, 689\u2013706 (2004). https:\/\/doi.org\/10.1002\/cpe.v16:7","journal-title":"Concurr. Comput. Pract. Exp\u2013Form. Tech. Java Program."},{"key":"9452_CR76","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004, Lecture Notes in Artificial Intelligence, vol. 3452, pp. 398\u2013414. Springer (2005)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9452_CR77","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"issue":"3","key":"9452_CR78","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013). https:\/\/doi.org\/10.1145\/2487241.2487248","journal-title":"J. ACM"},{"key":"9452_CR79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer, Berlin (2001)"},{"key":"9452_CR80","doi-asserted-by":"crossref","unstructured":"Strecker, M.: Formal verification of a Java compiler in Isabelle. In: CADE 2002, LNCS, vol. 2392, pp. 63\u201377. Springer (2002)","DOI":"10.1007\/3-540-45620-1_5"},{"key":"9452_CR81","doi-asserted-by":"publisher","unstructured":"Strecker, M.: Investigating type-certifying compilation with Isabelle. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002, LNCS, vol. 2514, pp. 403\u2013417. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-36078-6_27","DOI":"10.1007\/3-540-36078-6_27"},{"key":"9452_CR82","unstructured":"Tool-assisted specification and verification of javacard programmes: Verificard. http:\/\/cordis.europa.eu\/project\/rcn\/53643_en.html"},{"key":"9452_CR83","unstructured":"Wagner, D., et\u00a0al. (eds.): Ausgezeichnete Informatik. Dissertation (2003), LNI, vol. D-3. K\u00f6llen Verlag (2003)"},{"key":"9452_CR84","doi-asserted-by":"crossref","unstructured":"Wand, M.: Compiler correctness for parallel languages. In: FPCA 1995, pp. 120\u2013134. ACM (1995)","DOI":"10.1145\/224164.224193"},{"key":"9452_CR85","unstructured":"Wasserrab, D.: From formal semantics to verified slicing\u2014a modular framework with applications in language based security. Ph.D. thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik (2010)"},{"key":"9452_CR86","unstructured":"Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: 6th International Verification Workshop (VERIFY 2010), 2010"},{"issue":"1","key":"9452_CR87","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9452-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9452-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9452-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T10:58:03Z","timestamp":1570705083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9452-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,8]]},"references-count":87,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9452"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9452-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,2,8]]},"assertion":[{"value":"23 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}