{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:59:27Z","timestamp":1743091167850,"version":"3.40.3"},"publisher-location":"Cham","reference-count":6,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_25","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"337-343","source":"Crossref","is-referenced-by-count":1,"title":["A Proof Infrastructure for Binary Programs"],"prefix":"10.1007","author":[{"given":"Ashlie B.","family":"Hocking","sequence":"first","affiliation":[]},{"given":"Benjamin D.","family":"Rodes","sequence":"additional","affiliation":[]},{"given":"John C.","family":"Knight","sequence":"additional","affiliation":[]},{"given":"Jack W.","family":"Davidson","sequence":"additional","affiliation":[]},{"given":"Clark L.","family":"Coleman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"25_CR1","volume-title":"SPARK: The Proven Approach to High Integrity Software","author":"J Barnes","year":"2012","unstructured":"Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis, Bath (2012)"},{"key":"25_CR2","unstructured":"Erlingsson, U., Abadi, M., Vrable, M., Budiu, M., Necula, G.C.: XFI: software guards for system address spaces. In: Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI 2006, pp. 75\u201388. USENIX Association, Berkeley (2006)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"key":"25_CR4","unstructured":"Jager, I., Brumley, D.: Efficient directionless weakest preconditions (cmu-cylab-10-002). CyLab, p. 27 (2010)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-319-29613-5_12","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"J Tan","year":"2016","unstructured":"Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: AUSPICE: automatic safety property verification for unmodified executables. In: Gurfinkel, A., et al. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 202\u2013222. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29613-5_12"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Zhao, L., Li, G., De Sutter, B., Regehr, J.: ARMor: fully verified software fault isolation. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT 2011, pp. 289\u2013298, NY. ACM, New York (2011)","DOI":"10.1145\/2038642.2038687"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T11:41:26Z","timestamp":1498304486000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}