Abstract
Abstract Interpretation proposes advanced techniques for static analysis of programs that raise specific challenges for machine-checked soundness proofs. Most classical dataflow analysis techniques iterate operators on lattices without infinite ascending chains. In contrast, abstract interpreters are looking for fixpoints in infinite lattices where widening and narrowing are used for accelerating the convergence. Smart iteration strategies are crucial when using such accelerating operators because they directly impact the precision of the analysis diagnostic. In this paper, we show how we manage to program and prove correct in Coq an abstract interpreter that uses iteration strategies based on program syntax. A key component of the formalization is the introduction of an intermediate semantics based on a generic least-fixpoint operator on complete lattices and allows us to decompose the soundness proof in an elegant manner.
Work partially supported by ANR-U3CAT grant and FNRAE ASCERT grant.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 115–130. Springer, Heidelberg (2009)
Bertot, Y.: Structural abstract interpretation, a formal study in Coq. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) ALFA. LNCS, vol. 5520, pp. 153–194. Springer, Heidelberg (2009)
Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning 43(3), 263–288 (2009)
Cousot, P.: Visiting Professor at the MIT Aeronautics and Astronautics Department, Course 16.399: Abstract Interpretation
Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL’77, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Current Trends in Hardware Verfication and Automatic Theorem Proving, pp. 387–439. Springer, Heidelberg (1988)
Leroy, X.: Mechanized semantics, with applications to program proof and compiler verification, lecture given at the, Marktoberdorf summer school (2009)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proc. of POPL’06, pp. 42–54. ACM Press, New York (2006)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)
Pichardie, D.: Interprétation abstraite en logique intuitionniste : extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1 (2005) (in french)
Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proc. of FICS’08. ENTCS, vol. 212, pp. 225–239 (2008)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cachera, D., Pichardie, D. (2010). A Certified Denotational Abstract Interpreter. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)