Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In CPP 2012: Certified Programs and Proofs, number 7679 in LNCS, pages 11--26. Springer, 2012.

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.

bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.