{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:32:44Z","timestamp":1725867164437},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"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-47958-3_3","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T09:40:52Z","timestamp":1475919652000},"page":"42-62","source":"Crossref","is-referenced-by-count":0,"title":["AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code"],"prefix":"10.1007","author":[{"given":"Jiaqi","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui Jun","family":"Tay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gandhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Priya","family":"Narasimhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"3_CR1","unstructured":"Application Binary Interface for the ARM Architecture. http:\/\/bit.ly\/22OaMai"},{"key":"3_CR2","unstructured":"Linux Programmer\u2019s Manual: Syscalls. http:\/\/bit.ly\/1VChJMY"},{"key":"3_CR3","unstructured":"The ARM-THUMB Procedure Call Standard (2000). http:\/\/bit.ly\/1NbOQhT"},{"key":"3_CR4","unstructured":"As Gadgets Shrink, ARM Still Reigns As Processor King, September 2013. http:\/\/onforb.es\/19LIzgd"},{"key":"3_CR5","unstructured":"ARM Architecture Reference Manual: ARMv7-A and ARMv7-R edition (2014)"},{"key":"3_CR6","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":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21690-4_20"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19718-5_1"},{"key":"3_CR9","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":"3_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, October 2009","DOI":"10.1145\/1629575.1629596"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Guthaus, M., et al.: MiBench: a free, commercially representative embedded benchmark suite. In: IEEE WWC Workshop (2001)","DOI":"10.1109\/WWC.2001.990739"},{"key":"3_CR13","unstructured":"Jia, N.: Detecting human falls with a 3-axis digital accelerometer (2009). http:\/\/bit.ly\/23fXhFE"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015)","DOI":"10.1145\/2676726.2676966"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"3_CR16","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"},{"key":"3_CR17","unstructured":"Miller, C., Valasek, C.: Remote exploitation of an unaltered passenger vehicle. http:\/\/bit.ly\/1Xk71rn"},{"key":"3_CR18","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). doi: 10.1007\/978-3-540-75698-9_18"},{"key":"3_CR19","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\u00a0code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568\u2013582. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_44"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Goel, S., et al.: Simulation and formal verification of x86 machine-code programs that make system calls. In: FMCAD (2014)","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"3_CR22","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). doi: 10.1007\/978-3-540-71067-7_6"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Tan, J., Tay, H., Drolia, U., Gandhi, R., Narasimhan, P.: PCFIRE: towards provable preventative control-flow integrity enforcement for realistic embedded software. In: EMSOFT (2016)","DOI":"10.1145\/2968478.2968492"},{"key":"3_CR24","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: $$\\underline{\\rm {Au}}$$ tomatic $$\\underline{\\rm {S}}$$ afety $$\\underline{\\rm {P}}$$ roperty verif $$\\underline{\\rm {ic}}$$ ation for unmodified $$\\underline{\\rm {E}}$$ xecutables. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 202\u2013222. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29613-5_12"},{"key":"3_CR25","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":"3_CR26","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI (2011)","DOI":"10.1145\/1993498.1993532"},{"key":"3_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","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47958-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T07:30:54Z","timestamp":1568446254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}