{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:37:54Z","timestamp":1759991874352},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_20","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"246-261","source":"Crossref","is-referenced-by-count":13,"title":["The Safety-Critical Java Memory Model: A Formal Account"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"key":"20_CR2","volume-title":"Programming in Ada 95","author":"J. Barnes","year":"2005","unstructured":"Barnes, J.: Programming in Ada 95. Addison-Wesley, Reading (2005)"},{"issue":"3","key":"20_CR3","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"Software Tools for Technology Transfer"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/340396.340450","volume":"XIX","author":"A. Burns","year":"1999","unstructured":"Burns, A.: The Ravenscar Profile. Ada Letters\u00a0XIX, 49\u201352 (1999)","journal-title":"Ada Letters"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-73210-5_5","volume-title":"Integrated Formal Methods","author":"A. Butterfield","year":"2007","unstructured":"Butterfield, A., Sherif, A., Woodcock, J.C.P.: Slotted-circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 75\u201397. Springer, Heidelberg (2007)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.L.C., Wellings, A., Woodcock, J.C.P.: The Safety-Critical Java Mission Model: a formal account \u2013 Extended Version. Technical report (2011), http:\/\/www-users.cs.york.ac.uk\/~alcc\/CWW11b.pdf","DOI":"10.1007\/978-3-642-21437-0_20"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11783596_10","volume-title":"Mathematics of Program Construction","author":"Y. Chen","year":"2006","unstructured":"Chen, Y., Sanders, J.: Compositional Reasoning for Pointer Structures. In: Yu, H.-J. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 115\u2013139. Springer, Heidelberg (2006)"},{"key":"20_CR8","volume-title":"JTRES","author":"G. Haddad","year":"2010","unstructured":"Haddad, G., Hussain, F., Leavens, G.T.: The Design of SafeJML, A Specification Language for SCJ with Support for WCET Specification. In: JTRES. ACM, New York (2010)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-85762-4_10","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"W. Harwood","year":"2008","unstructured":"Harwood, W., Cavalcanti, A.L.C., Woodcock, J.C.P.: A Theory of Pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 141\u2013155. Springer, Heidelberg (2008)"},{"key":"20_CR10","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. Programming methodology, pp. 223\u2013245 (2003)","DOI":"10.1007\/978-0-387-21798-7_11"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-73210-5_19","volume-title":"Integrated Formal Methods","author":"H. Jifeng","year":"2007","unstructured":"Jifeng, H.: UTP semantics for web services. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 353\u2013372. Springer, Heidelberg (2007)"},{"key":"20_CR13","unstructured":"Locke, D., et al.: Safety Critical Java Specification. The Open Group, UK (2010), jcp.org\/aboutJava\/communityprocess\/edr\/jsr302\/index.html"},{"issue":"1-2","key":"20_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M.V.M. Oliveira","year":"2009","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP Semantics for Circus. Formal Aspects of Computing\u00a021(1-2), 3\u201332 (2009)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11768173_2","volume-title":"Unifying Theories of Programming","author":"T.L.V.L. Santos","year":"2006","unstructured":"Santos, T.L.V.L., Cavalcanti, A.L.C., Sampaio, A.C.A.: Object-Orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 18\u201337. Springer, Heidelberg (2006)"},{"issue":"2","key":"20_CR16","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A. Sherif","year":"2010","unstructured":"Sherif, A., et al.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing\u00a022(2), 153\u2013191 (2010)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR17","volume-title":"JTRES","author":"D. Tang","year":"2010","unstructured":"Tang, D., Plsek, A., Vitek, J.: Static Checking of Safety Critical Java Annotations. In: JTRES.ACM, New York (2010)"},{"issue":"2","key":"20_CR18","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation\u00a0132(2), 109\u2013176 (1997)","journal-title":"Information and Computation"},{"key":"20_CR19","volume-title":"Concurrent and Real-Time Programming in Java","author":"A. Wellings","year":"2004","unstructured":"Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley, Chichester (2004)"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Wellings, A., Kim, M.: Asynchronous event handling and safety critical Java. In: JTRES. ACM, New York","DOI":"10.1145\/1850771.1850778"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:07:07Z","timestamp":1560298027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}