{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:47:09Z","timestamp":1777348029891,"version":"3.51.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296128","type":"print"},{"value":"9783319296135","type":"electronic"}],"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-29613-5_12","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"202-222","source":"Crossref","is-referenced-by-count":8,"title":["AUSPICE: Automatic Safety Property Verification for Unmodified Executables"],"prefix":"10.1007","author":[{"given":"Jiaqi","family":"Tan","sequence":"first","affiliation":[]},{"given":"Hui Jun","family":"Tay","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Gandhi","sequence":"additional","affiliation":[]},{"given":"Priya","family":"Narasimhan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"The ARM-THUMB Procedure Call Standard (2000). \n                    http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.espc0002\/ATPCS.pdf"},{"key":"12_CR2","unstructured":"ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition (2014)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Budiu, M., Erlingsson, U., Ligatti, J.: Control-flow Integrity. In: ACM CCS (2005)","DOI":"10.1145\/1102120.1102165"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Blackham, B., Heiser, G.: Sequel: a framework for model checking binaries. In: IEEE RTAS (2013)","DOI":"10.1109\/RTAS.2013.6531083"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Candea, G.: Enabling sophisticated analyses of x86 binaries with RevGen. In: HotDep (2011)","DOI":"10.1109\/DSNW.2011.5958815"},{"issue":"6","key":"12_CR6","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/1993316.1993526","volume":"46","author":"Adam Chlipala","year":"2011","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"12_CR8","unstructured":"Erlingsson, U., Abadi, M., Vrable, M., Budiu, M., Necula, G.: XFI: software guards for system address spaces. In: OSDI (2006)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25\u201340. Springer, Heidelberg (2003)"},{"key":"12_CR10","unstructured":"Guthaus, M.R., Ringenberg, J.S., Ernst, D., Austin, T.M., Mudge, T., Brown, R.B.: Mibench: a free, commercially representative embedded benchmark suite. In: IEEE WWC Workshop (2001)"},{"issue":"10","key":"12_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"12_CR12","unstructured":"McCamant, S., Morrisett, G.: Evaluating SFI for a CISC architecture. In: USENIX Security (2006)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., Zdancewic, S.: TALx86: a realistic typed assembly language. In: Workshop on Compiler Support for System Software (WCSSS) (1999)","DOI":"10.21236\/ADA358572"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: PLDI (2012)","DOI":"10.1145\/2254064.2254111"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-75698-9_18","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"MO Myreen","year":"2007","unstructured":"Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MO Myreen","year":"2007","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568\u2013582. Springer, Heidelberg (2007)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Myreen, M., Gordon, M., Slind, K.: Machine-code verification for multiple architectures: an application of decompilation into logic. In: FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL (2006)","DOI":"10.1145\/1111037.1111066"},{"key":"12_CR19","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS (2002)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Tan","year":"2006","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80\u201394. Springer, Heidelberg (2006)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Tate, R., Chen, J., Hawblitzel, C.: Inferable object-oriented typed assembly language. In: PLDI (2010)","DOI":"10.1145\/1806596.1806644"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-14295-6_27","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2010","unstructured":"Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288\u2013305. Springer, Heidelberg (2010)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Wahbe, R., Lucco, S., Anderson, T., Graham, S.: Efficient software-based fault isolation. In: SOSP (1993)","DOI":"10.1145\/168619.168635"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Xu, Z., Miller, B., Reps, T.: Safety checking of machine code. In: PLDI (2000)","DOI":"10.1145\/349299.349313"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363\u2013379. Springer, Heidelberg (2003)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Zhao, L., Li, G., Sutter, B.D., Regehr, J.: ARMor: fully verified software fault isolation. In: EMSOFT (2011)","DOI":"10.1145\/2038642.2038687"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:51:16Z","timestamp":1559375476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}