{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T04:03:23Z","timestamp":1781064203261,"version":"3.54.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,1,25]],"date-time":"2016-01-25T00:00:00Z","timestamp":1453680000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-INSE-003"],"award-info":[{"award-number":["ANR-11-INSE-003"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s10817-015-9359-8","type":"journal-article","created":{"date-parts":[[2016,1,25]],"date-time":"2016-01-25T02:56:44Z","timestamp":1453690604000},"page":"283-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code"],"prefix":"10.1007","volume":"56","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,1,25]]},"reference":[{"key":"9359_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Thomas, W.: Reps. Wysinwyx: What you see is not what you execute. ACM Trans. Program. On Lang. Syst. 32(6), 23 (2010)","DOI":"10.1145\/1749608.1749612"},{"key":"9359_CR2","doi-asserted-by":"crossref","unstructured":"Bardin, S., Herrmann, P., V\u00e9drine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Verification, Model Checking and Abstract Interpretation (VMCAI), vol. 6538 of LNCS, pp 54\u201369. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_6"},{"key":"9359_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y.: Structural abstract interpretation, a formal study in Coq. In: Language Engineering and Rigorous Software Development, International LerNet\u00a0alFA Summer School 2008, vol. 5520 of LNCS, pp. 153\u2013194. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03153-3_4"},{"key":"9359_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gr\u00e9goire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In TYPES, vol. 3839 of LNCS, pp. 66\u201381. Springer, Berlin (2006)","DOI":"10.1007\/11617990_5"},{"key":"9359_CR5","doi-asserted-by":"crossref","unstructured":"Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a c value analysis based on abstract interpretation. In: Static Analysis Symposium (SAS), vol. 7935 of LNCS, pp. 324\u2013344. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38856-9_18"},{"issue":"3","key":"9359_CR6","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy S., Leroy X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reason."},{"key":"9359_CR7","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":"9359_CR8","doi-asserted-by":"crossref","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1), 56\u201378 (2005)","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"9359_CR9","unstructured":"Cachera, D., Pichardie, D.: Comparing techniques for certified static analysis. In: Proceedings of the 1st NASA Formal Methods Symposium (NFM\u201909), pp. 111\u2013115 (2009)"},{"key":"9359_CR10","doi-asserted-by":"crossref","unstructured":"Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Interactive Theorem Proving (ITP), vol. 6172 of LNCS, pp. 9\u201324. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14052-5_3"},{"key":"9359_CR11","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Conference on Programming Language Design and Implementation (PLDI), pp. 66\u201377. ACM, New York (2007)","DOI":"10.1145\/1250734.1250743"},{"key":"9359_CR12","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Conference on Programming Language Design and Implementation (PLDI). ACM, New York (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"9359_CR13","doi-asserted-by":"crossref","unstructured":"Collberg, C., Thomborson, C., Low, D.: Manufacturing cheap, resilient, and stealthy opaque constructs. In 25th Symposium on Principles of Programming Language (POPL), pp. 184\u2013196. ACM, New York (1998)","DOI":"10.1145\/268946.268962"},{"key":"9359_CR14","unstructured":"Companion website. http:\/\/www.irisa.fr\/celtique\/ext\/smc ."},{"key":"9359_CR15","doi-asserted-by":"crossref","unstructured":"Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: TYPES, vol. 3839 of LNCS, pp. 115\u2013137 (2004)","DOI":"10.1007\/11617990_8"},{"key":"9359_CR16","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: Symposium on Principles of Programming Language (POPL), p. 238252. ACM, New York","DOI":"10.1145\/512950.512973"},{"key":"9359_CR17","unstructured":"Debray, S.K., Coogan, K.P., Townsend, G.M.: On the semantics of self-unpacking malware code. Draft, (2008)"},{"key":"9359_CR18","unstructured":"Gerth, R.T.: Formal verification of self modifying code. In: International Conference for Young Computer Scientists. International Academic Publishers, China (1991)"},{"key":"9359_CR19","doi-asserted-by":"crossref","unstructured":"Jensen, J., Benton, N,, Kennedy, A.: High-level separation logic for low-level code. In: Symposium on Principles of Programming Language (POPL). ACM, New York (2013)","DOI":"10.1145\/2429069.2429105"},{"key":"9359_CR20","doi-asserted-by":"crossref","unstructured":"Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: Formal verification of a C static analyzer. In 42nd Symposium Principles of Programming Languages (POPL), pp. 247\u2013259 (2015)","DOI":"10.1145\/2775051.2676966"},{"key":"9359_CR21","doi-asserted-by":"crossref","unstructured":"Kennedy, A., Benton, N., Jensen, J.B,, Dagand, P.: Coq: The world\u2019s best macro assembler? In: Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 13\u201324. ACM, New York (2013)","DOI":"10.1145\/2505879.2505897"},{"key":"9359_CR22","doi-asserted-by":"crossref","unstructured":"Kinder, J.: Towards static analysis of virtualization-obfuscated binaries. In: Reverse Engineering (WCRE), 2012 19th Working Conference on, pp. 61\u201370. IEEE (2012)","DOI":"10.1109\/WCRE.2012.16"},{"issue":"4","key":"9359_CR23","doi-asserted-by":"crossref","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 Trans. Programm. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"9359_CR24","unstructured":"Monniaux, D.: R\u00e9alisation m\u00e9canis\u00e9e d\u2019interpr\u00e9teurs abstraits. Master\u2019s thesis, U. Paris 7 (1998)"},{"key":"9359_CR25","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B., Gan, E.: Rocksalt: better, faster, stronger sfi for the x86. In Conference on Programming Language Design and Implementation (PLDI), pp. 395\u2013404 (2012)","DOI":"10.1145\/2254064.2254111"},{"key":"9359_CR26","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: Symposium on Principles of Programming Language (POPL), pp. 107\u2013118. ACM, New York (2010)","DOI":"10.1145\/1706299.1706313"},{"key":"9359_CR27","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Abstract interpretation of annotated commands. In: Interactive Theorem Proving (ITP), vol. 7406 of LNCS, pp. 116\u2013132. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-32347-8_9"},{"key":"9359_CR28","unstructured":"Pichardie, D.: Interprtation Abstraite en Logique Intuitionniste: Extraction d\u2019analyseurs Java Certifis. PhD thesis, U. Rennes 1, (2005)"},{"key":"9359_CR29","doi-asserted-by":"crossref","unstructured":"Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proceedings of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS), vol. 212 of Electronic Notes in Theoretical Computer Science, pp. 225\u2013239 (2008)","DOI":"10.1016\/j.entcs.2008.04.064"},{"key":"9359_CR30","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/j.entcs.2008.04.064","volume":"212","author":"D. Pichardie","year":"2008","unstructured":"Pichardie D.: Building certified static analysers by modular construction of well-founded lattices. Electr. Notes Theor. Comput. Sci. 212, 225\u2013239 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9359_CR31","doi-asserted-by":"crossref","unstructured":"Robert, V., Leroy, X.: A formally-verified alias analysis. In: Certified Proofs and Programs (CPP), vol. 7679 of LNCS, pp. 11\u201326. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-35308-6_5"},{"key":"9359_CR32","doi-asserted-by":"crossref","unstructured":"Stewart, G., Beringer, L., Appel, A.W.: Verified heap theorem prover by paramodulation. In: International Conference on Functional Programming (ICFP), pp. 3\u201314. ACM, New York (2012)","DOI":"10.1145\/2364527.2364531"},{"key":"9359_CR33","unstructured":"Szor, P.: The Art of Computer Virus Research and Defense. Addison-Wesley Professional, Boston (2005)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9359-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9359-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9359-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T19:59:09Z","timestamp":1567540749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9359-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,25]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["9359"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9359-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,25]]}}}