{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:14:47Z","timestamp":1750306487318,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T00:00:00Z","timestamp":1444176000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/H017461\/1"],"award-info":[{"award-number":["EP\/H017461\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,7]]},"DOI":"10.1145\/2822304.2822307","type":"proceedings-article","created":{"date-parts":[[2015,10,30]],"date-time":"2015-10-30T15:27:07Z","timestamp":1446218827000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Safety-Critical Java Virtual Machine Services"],"prefix":"10.1145","author":[{"given":"James","family":"Baxter","sequence":"first","affiliation":[{"name":"University of York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[{"name":"University of York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[{"name":"University of York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leo","family":"Freitas","sequence":"additional","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1324969.1324974"},{"key":"e_1_3_2_1_2_1","unstructured":"Atego. Atego Perc Pico - Products - Atego. http:\/\/www.atego.com\/products\/atego-perc-pico\/ 2015.  Atego. Atego Perc Pico - Products - Atego. http:\/\/www.atego.com\/products\/atego-perc-pico\/ 2015."},{"key":"e_1_3_2_1_3_1","volume-title":"Requirements for Safety-Critical Java Virtual Machines. Technical report","author":"Baxter J.","year":"2015","unstructured":"J. Baxter . Requirements for Safety-Critical Java Virtual Machines. Technical report , University of York , 2015 . http:\/\/www.cs.york.ac.uk\/circus\/publications\/techreports\/reports\/scjvm-requirements.pdf. J. Baxter. Requirements for Safety-Critical Java Virtual Machines. Technical report, University of York, 2015. http:\/\/www.cs.york.ac.uk\/circus\/publications\/techreports\/reports\/scjvm-requirements.pdf."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-739X(99)00094-1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"A.\n      Cavalcanti A.\n      Wellings and \n      J.\n      Woodcock\n  . \n  The Safety-Critical Java memory model: A formal account\n  . In M. Butler and W. Schulte editors FM \n  2011\n  : Formal Methods volume \n  6664\n   of \n  Lect\n  . Notes Comput. Sc. pages \n  246\n  --\n  261\n  . \n  Springer Berlin Heidelberg 2011.   A. Cavalcanti A. Wellings and J. Woodcock. The Safety-Critical Java memory model: A formal account. In M. Butler and W. Schulte editors FM 2011: Formal Methods volume 6664 of Lect. Notes Comput. Sc. pages 246--261. Springer Berlin Heidelberg 2011.","DOI":"10.1007\/978-3-642-21437-0_20"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-013-9182-4"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1978802.1978814"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0124-9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0307-4"},{"key":"e_1_3_2_1_10_1","volume-title":"The Real-Time Specification for Java","author":"Gosling J.","year":"2000","unstructured":"J. Gosling and G. Bollella . The Real-Time Specification for Java . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA , 2000 . J. Gosling and G. Bollella. The Real-Time Specification for Java. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2000."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000075"},{"key":"e_1_3_2_1_12_1","volume-title":"Workshop on the Formal Underpinnings of the Java Paradigm","author":"Jones M.","year":"1998","unstructured":"M. Jones . The functions of Java bytecode . In Workshop on the Formal Underpinnings of the Java Paradigm , 1998 . M. Jones. The functions of Java bytecode. In Workshop on the Formal Underpinnings of the Java Paradigm, 1998."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-008-9059-0"},{"key":"e_1_3_2_1_15_1","volume-title":"Pearson Education","author":"Lindholm T.","year":"2014","unstructured":"T. Lindholm , F. Yellin , G. Bracha , and A. Buckley . The Java virtual machine specification . Pearson Education , 2014 . T. Lindholm, F. Yellin, G. Bracha, and A. Buckley. The Java virtual machine specification. Pearson Education, 2014."},{"key":"e_1_3_2_1_16_1","volume-title":"Virtual Machine, Memory Model, and Verified Compiler","author":"Lochbihler A.","year":"2012","unstructured":"A. Lochbihler . A Machine-Checked , Type-Safe Model of Java Concurrency: Language , Virtual Machine, Memory Model, and Verified Compiler . KIT Scientific Publishing , 2012 . A. Lochbihler. A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. KIT Scientific Publishing, 2012."},{"key":"e_1_3_2_1_17_1","volume-title":"Safety-Critical Java Technology Specification","author":"Locke D.","year":"2013","unstructured":"D. Locke , B. S. Andersen , B. Brosgol , M. Fulton , T. Henties , J. J. Hunt , J. O. Nielsen , K. Nilsen , M. Schoeberl , J. Tokar , J. Vitek , A. Wellings , Safety-Critical Java Technology Specification . The Open Group , Jun 2013 . D. Locke, B. S. Andersen, B. Brosgol, M. Fulton, T. Henties, J. J. Hunt, J. O. Nielsen, K. Nilsen, M. Schoeberl, J. Tokar, J. Vitek, A. Wellings, et al. Safety-Critical Java Technology Specification. The Open Group, Jun 2013."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661020.2661022"},{"key":"e_1_3_2_1_19_1","series-title":"NATO Science Series F: Computer and Systems Sciences","first-page":"117","volume-title":"Foundations of Secure Computation","author":"Nipkow T.","year":"2000","unstructured":"T. Nipkow , D. von Oheimb , and C. Pusch . \u00b5java: Embedding a programming language in a theorem prover . In F. L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation , volume 175 of NATO Science Series F: Computer and Systems Sciences , pages 117 -- 144 . IOS Press , 2000 . T. Nipkow, D. von Oheimb, and C. Pusch. \u00b5java: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 117--144. IOS Press, 2000."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620405.1620421"},{"key":"e_1_3_2_1_22_1","volume-title":"Conference Proceedings: Embedded Real-Time Software and Systems","author":"Richard-Foy M.","year":"2010","unstructured":"M. Richard-Foy , T. Schoofs , E. Jenn , L. Gauthier , and K. Nilsen . Use of PERC Pico for safety critical Java . In Conference Proceedings: Embedded Real-Time Software and Systems , Toulouse, France , 2010 . M. Richard-Foy, T. Schoofs, E. Jenn, L. Gauthier, and K. Nilsen. Use of PERC Pico for safety critical Java. In Conference Proceedings: Embedded Real-Time Software and Systems, Toulouse, France, 2010."},{"key":"e_1_3_2_1_23_1","volume-title":"Understanding Concurrent Systems. Texts in Computer Science","author":"Roscoe A. W.","year":"2011","unstructured":"A. W. Roscoe . Understanding Concurrent Systems. Texts in Computer Science . Springer , 2011 . A. W. Roscoe. Understanding Concurrent Systems. Texts in Computer Science. Springer, 2011."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2388936.2388945"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/559207"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction --- CADE-18","author":"Strecker M.","year":"2002","unstructured":"M. Strecker . Formal verification of a Java compiler in Isabelle . In A. Voronkov, editor, Automated Deduction --- CADE-18 , pages 63 -- 77 . Springer , 2002 . M. Strecker. Formal verification of a Java compiler in Isabelle. In A. Voronkov, editor, Automated Deduction --- CADE-18, pages 63--77. Springer, 2002."},{"key":"e_1_3_2_1_27_1","volume-title":"Using Z: specification, refinement, and proof","author":"Woodcock J.","year":"1996","unstructured":"J. Woodcock and J. Davies . Using Z: specification, refinement, and proof . Prentice-Hall, Inc. , 1996 . J. Woodcock and J. Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., 1996."}],"event":{"name":"JTRES '15: The 13th International Workshop on Java Technologies for Real-time and Embedded Systems","acronym":"JTRES '15","location":"Paris France"},"container-title":["Proceedings of the 13th International Workshop on Java Technologies for Real-time and Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2822304.2822307","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2822304.2822307","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:31Z","timestamp":1750225711000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2822304.2822307"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,7]]},"references-count":27,"alternative-id":["10.1145\/2822304.2822307","10.1145\/2822304"],"URL":"https:\/\/doi.org\/10.1145\/2822304.2822307","relation":{},"subject":[],"published":{"date-parts":[[2015,10,7]]},"assertion":[{"value":"2015-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}