A formally-verified alias analysis

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00773109
Contributor : Xavier Leroy <>
Submitted on : Friday, January 11, 2013 - 3:59:42 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Saturday, April 1, 2017 - 4:00:28 AM

File

alias-analysis.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Valentin Robert, Xavier Leroy. A formally-verified alias analysis. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.11-26, ⟨10.1007/978-3-642-35308-6_5⟩. ⟨hal-00773109⟩

Share

Metrics

Record views

241

Files downloads

167