{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:51:59Z","timestamp":1725796319988},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089690"},{"type":"electronic","value":"9783319089706"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_9","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:13:26Z","timestamp":1403939606000},"page":"128-143","source":"Crossref","is-referenced-by-count":3,"title":["Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code"],"prefix":"10.1007","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.W.: WYSINWYX: What you see is not what you eXecute. ACM Trans. Program. Lang. Syst.\u00a032(6) (2010)","DOI":"10.1145\/1749608.1749612"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-18275-4_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Bardin","year":"2011","unstructured":"Bardin, S., Herrmann, P., V\u00e9drine, F.: Refinement-Based CFG Reconstruction from Unstructured Programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 54\u201369. Springer, Heidelberg (2011)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-38856-9_18","volume-title":"Static Analysis","author":"S. Blazy","year":"2013","unstructured":"Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal Verification of a C Value Analysis Based on Abstract Interpretation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 324\u2013344. Springer, Heidelberg (2013)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Marion, J.Y., Reynaud-Plantey, D.: A Computability Perspective on Self-Modifying Programs. In: SEFM, pp. 231\u2013239 (2009)","DOI":"10.1109\/SEFM.2009.25"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-14052-5_3","volume-title":"Interactive Theorem Proving","author":"D. Cachera","year":"2010","unstructured":"Cachera, D., Pichardie, D.: A Certified Denotational Abstract Interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 9\u201324. Springer, Heidelberg (2010)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified Self-Modifying Code. In: PLDI, pp. 66\u201377. ACM (2007)","DOI":"10.1145\/1273442.1250743"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI. ACM (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"9_CR8","unstructured":"Companion website, \n                    \n                      http:\/\/www.irisa.fr\/celtique\/ext\/smc"},{"key":"9_CR9","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, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Jensen, J., Benton, N., Kennedy, A.: High-Level Separation Logic for Low-Level Code. In: POPL. ACM (2013)","DOI":"10.1145\/2429069.2429105"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Kennedy, A., et al.: Coq: The world\u2019s best macro assembler? In: PPDP, pp. 13\u201324. ACM (2013)","DOI":"10.1145\/2505879.2505897"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Kinder, J.: Towards static analysis of virtualization-obfuscated binaries. In: WCRE, pp. 61\u201370 (2012)","DOI":"10.1109\/WCRE.2012.16"},{"issue":"4","key":"9_CR13","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. ACM TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Morrisett, G., et al.: RockSalt: better, faster, stronger SFI for the x86. In: PLDI, pp. 395\u2013404 (2012)","DOI":"10.1145\/2345156.2254111"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: POPL, pp. 107\u2013118. ACM (2010)","DOI":"10.1145\/1707801.1706313"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-32347-8_9","volume-title":"Interactive Theorem Proving","author":"T. Nipkow","year":"2012","unstructured":"Nipkow, T.: Abstract Interpretation of Annotated Commands. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 116\u2013132. Springer, Heidelberg (2012)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-35308-6_5","volume-title":"Certified Programs and Proofs","author":"V. Robert","year":"2012","unstructured":"Robert, V., Leroy, X.: A Formally-Verified Alias Analysis. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 11\u201326. Springer, Heidelberg (2012)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Stewart, G., Beringer, L., Appel, A.W.: Verified heap theorem prover by paramodulation. In: ICFP, pp. 3\u201314. ACM (2012)","DOI":"10.1145\/2398856.2364531"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08970-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:07:52Z","timestamp":1558919272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}