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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)
Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press (1998)
Bertot, Y.: Structural Abstract Interpretation: A Formal Study Using Coq. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 153–194. Springer, Heidelberg (2009)
Besson, F., Cachera, D., Jensen, T.P., Pichardie, D.: Certified Static Analysis by Abstract Interpretation. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 223–257. Springer, Heidelberg (2009)
Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation to fixpoint compression. Theoretical Computer Science 364(3), 273–291 (2006)
Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Dabrowski, F., Pichardie, D.: A Certified Data Race Analysis for a Java-like Language. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 212–227. Springer, Heidelberg (2009)
Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Program Analysis For Software Tools and Engineering (PASTE 2001), pp. 54–61. ACM (2001)
Kildall, G.A.: A unified approach to global program optimization. In: 1st Symposium Principles of Programming Languages, pp. 194–206. ACM Press, New York (1973)
Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: Programming Language Design and Implementation (PLDI 1988), pp. 21–34. ACM Press, New York (1988)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Leroy, X.: A formally verified compiler back-end. J. Automated Reasoning 43(4), 363–446 (2009)
Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Research report RR-7987, INRIA (June 2012)
Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Automated Reasoning 41(1) (2008)
Nipkow, T.: Abstract Interpretation of Annotated Commands. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 116–132. Springer, Heidelberg (2012)
Steensgaard, B.: Points-to analysis in almost linear time. In: 23rd Symp. Principles of Programming Languages (POPL 1996), pp. 32–41. ACM (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Robert, V., Leroy, X. (2012). A Formally-Verified Alias Analysis. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)