{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:49Z","timestamp":1740098929476,"version":"3.37.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_11","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"161-176","source":"Crossref","is-referenced-by-count":0,"title":["Algebraic Compilation of Safety-Critical Java Bytecode"],"prefix":"10.1007","author":[{"given":"James","family":"Baxter","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"crossref","first-page":"5:1","DOI":"10.1145\/1324969.1324974","volume":"7","author":"A Armbruster","year":"2007","unstructured":"Armbruster, A., Baker, J., Cunei, A., et al.: A real-time Java virtual machine with applications in avionics. ACM Trans. Embed. Comput. Syst. 7(1), 5:1\u20135:49 (2007)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"11_CR2","unstructured":"Baxter, J.: An Approach to verification of Safety-Critical Java Virtual Machines with Ahead-of-time compilation. Technical report, University of York (2017). \nwww-users.cs.york.ac.uk\/~jeb531\/2017report.pdf"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Baxter, J., Cavalcanti, A., Wellings, A., Freitas, L.: Safety-critical Java virtual machine services. In: JTRES 2015, pp. 7:1\u20137:10. ACM (2015)","DOI":"10.1145\/2822304.2822307"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460\u2013475. Springer, Heidelberg (2006). doi:\n10.1007\/11813040_31"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in circus. In: JTRES 2011, pp. 20\u201329. ACM (2011)","DOI":"10.1145\/2043910.2043915"},{"issue":"5","key":"11_CR6","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1007\/s11241-013-9182-4","volume":"49","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Zeyda, F., Wellings, A., Woodcock, J., Wei, K.: Safety-critical Java programs from Circus models. Real-Time Syst. 49(5), 614\u2013667 (2013)","journal-title":"Real-Time Syst."},{"issue":"2","key":"11_CR7","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u0131-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoret. Comput. Sci. 285(2), 187\u2013243 (2002)","journal-title":"Theoret. Comput. Sci."},{"issue":"8","key":"11_CR8","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"11_CR9","unstructured":"Duran, A.: An Algebraic Approach to the Design of Compilers for Object-Oriented Languages. Ph.D. thesis, Universidade Federal de Pernambuco (2005)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-319-33693-0_5","volume-title":"Integrated Formal Methods","author":"L Freitas","year":"2016","unstructured":"Freitas, L., Baxter, J., Cavalcanti, A., Wellings, A.: Modelling and verifying a priority scheduler for an SCJ runtime environment. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 63\u201378. Springer, Cham (2016). doi:\n10.1007\/978-3-319-33693-0_5"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Kalibera, T., Parizek, P., Malohlava, M., Schoeberl, M.: Exhaustive testing of safety critical java. In: JTRES 2010, pp. 164\u2013174. ACM (2010)","DOI":"10.1145\/1850771.1850794"},{"issue":"4","key":"11_CR12","doi-asserted-by":"crossref","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)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"11_CR13","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"11_CR14","doi-asserted-by":"crossref","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."},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-11957-6_23","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2010","unstructured":"Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427\u2013447. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-11957-6_23"},{"key":"11_CR16","unstructured":"Locke, D., et al.: Safety-Critical Java Technology Specification. \nhttps:\/\/jcp.org\/aboutJava\/communityprocess\/edr\/jsr302\/index2.html"},{"key":"11_CR17","unstructured":"Marriott, C.: Checking Memory Safety of Level 1 Safety-Critical Java Programs using Static-Analysis without Annotations. Ph.D. thesis, University of York (2014)"},{"key":"11_CR18","unstructured":"Motor Industry Software Reliability Association Guidelines: Guidelines for Use of the C Language in Critical Systems (2012)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"issue":"1\u20132","key":"11_CR20","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21(1\u20132), 3\u201332 (2009)","journal-title":"Formal Aspects Comput."},{"key":"11_CR21","unstructured":"Perna, J.: A verified compiler for Handel-C. Ph.D. thesis, University of York (2010)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Pizlo, F., Ziarek, L., Vitek, J.: Real time Java on resource-constrained platforms with Fiji VM. In: JTRES 2009, pp. 110\u2013119. ACM (2009)","DOI":"10.1145\/1620405.1620421"},{"key":"11_CR23","unstructured":"Proebsting, T.A., Townsend, G., Bridges, P., et al.: Toba: Java for applications a way ahead of time (wat) compiler. In: Proceedings of the 3rd Conference on Object-Oriented Technologies and Systems (1997)"},{"key":"11_CR24","series-title":"Texts in Computer Science","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2011","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)"},{"key":"11_CR25","doi-asserted-by":"crossref","DOI":"10.1142\/2870","volume-title":"An Algebraic Approach to Compiler Design","author":"A Sampaio","year":"1997","unstructured":"Sampaio, A.: An Algebraic Approach to Compiler Design. World Scientific, Singapore (1997)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Sawadpong, P., Allen, E.B., Williams, B.J.: Exception handling defects: an empirical study. In: HASE 2012, pp. 90\u201397. IEEE (2012)","DOI":"10.1109\/HASE.2012.24"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"S\u00f8ndergaard, H., Korsholm, S.E., Ravn, A.P.: Safety-critical Java for low-end embedded platforms. In: JTRES 2012, pp. 44\u201353. ACM (2012)","DOI":"10.1145\/2388936.2388945"},{"key":"11_CR28","doi-asserted-by":"crossref","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":"11_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction\u2014CADE-18","author":"M Strecker","year":"2002","unstructured":"Strecker, M.: Formal verification of a Java compiler in isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 63\u201377. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45620-1_5"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Varma, A., Bhattacharyya, S.S.: Java-through-C compilation: an enabling technology for Java in embedded systems. In: Proceedings of the Conference on Design, Automation and Test in Europe, vol. 3, p. 30161. IEEE Computer Society (2004)","DOI":"10.1109\/DATE.2004.1269224"},{"key":"11_CR31","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall Inc., Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:41:03Z","timestamp":1503747663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}