Abstract
This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is intraprocedural, flow-sensitive, field-sensitive, and untyped. Its soundness proof follows the general style of abstract interpretation. The analysis is designed to fit in the CompCert C verified compiler, supporting future aggressive optimizations over memory accesses. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Robert, V., & Leroy, X. (2012). A formally-verified alias analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 11–26). https://doi.org/10.1007/978-3-642-35308-6_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
