Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, 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 | Local copy | At publisher's ] Back


This file was generated by bibtex2html 1.97.