Abstract
We consider the problem of formalizing in higher-order logic the familiar notion of widening from abstract interpretation. It turns out that many axioms of widening (e.g. widening sequences are ascending) are not useful for proving correctness. After keeping only useful axioms, we give an equivalent characterization of widening as a lazily constructed well-founded tree. In type systems supporting dependent products and sums, this tree can be made to reflect the condition of correct termination of the widening sequence.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. In: Hankin, C. (ed.) Static Analysis (SAS). LNCS, vol. 3672, pp. 3–18. Springer, Berlin (2005). ISBN 3-540-28584-9. doi:10.1007/11547662_3
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Berlin (2004). ISBN 3-540-20854-2
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ, Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation: Complexity, Analysis, Transformation. LNCS, vol. 2566, pp. 85–108. Springer, Berlin (2002). ISBN 3-540-00326-6. doi:10.1007/3-540-36377-7_5
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), pp. 196–207. ACM, New York (2003). ISBN 1-58113-662-5. doi:10.1145/781131.781153
Clarke, E.M. Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999). ISBN 0-262-03270-8.
Costan, A., Gaubert, S., Goubault, É., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification (CAV). LNCS, vol. 4590, pp. 462–475. Springer, Berlin (2005). ISBN 3-540-27231-3. doi:10.1007/11513988_46
Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. State doctorate thesis, Université scientifique et médicale de Grenoble & Institut national polytechnique de Grenoble (1978). http://tel.archives-ouvertes.fr/tel-00288657/en/. In French
Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’05), January 17–19, 2005, pp. 1–24. Springer, Berlin (2005). ISBN 3-540-24297-X. doi:10.1007/b105073. http://www.di.ens.fr/~cousot/COUSOTpapers/VMCAI05.shtml
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput., 511–547 (1992). ISSN 0955-792X. doi:10.1093/logcom/2.4.511
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL), pp. 84–96. ACM, New York (1978). doi:10.1145/512760.512770
D’Silva, V.: Widening for automata. Diplomarbeit, Universität Zürich (2006)
Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: de Nicola, R. (ed.): Programming Languages and Systems (ESOP). LNCS, vol. 4421, pp. 300–315. Springer, Berlin (2007). ISBN 978-3-540-71316-6. doi:10.1007/978-3-540-71316-6_21
Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. PhD thesis, Université scientifique et médicale de Grenoble & Institut national polytechnique de Grenoble (1979). http://tel.archives-ouvertes.fr/tel-00288805/en/. In French
Halbwachs, N.: Delay analysis in synchronous programs. In: Computer Aided Verification (CAV), pp. 333–346. Springer, Berlin (1993). ISBN 3-540-56922-7. doi:10.1007/3-540-56922-7_28
Miné, A.: Weakly relational numerical abstract domains. PhD thesis, École polytechnique, Palaiseau, France (December 2004). In English
Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Verification, Model Checking, and Abstract Interpretation (VMCAI’06). LNCS, vol. 3855, pp. 348–363. Springer, Berlin (2006). ISBN 3-540-31139-4. doi:10.1007/11609773
Monniaux, D.: Optimal abstraction on real-valued programs. In: Filé, G., Nielson, H.R. (eds.) Static Analysis (SAS ’07). LNCS, vol. 4634, pp. 104–120. Springer, Berlin (2007)
Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL (Principles of Programming Languages). ACM, New York (2009). ISBN 978-1-60558-379-2. doi:10.1145/1480881.1480899
Pichardie, D.: Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1 (2005). In French
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: VMCAI. LNCS, vol. 3385, pp. 21–47. Springer, Berlin (2005)
Author information
Authors and Affiliations
Corresponding author
Additional information
VERIMAG is a joint laboratory of CNRS, Université Joseph Fourier and Grenoble-INP.
Rights and permissions
About this article
Cite this article
Monniaux, D. A minimalistic look at widening operators. Higher-Order Symb Comput 22, 145–154 (2009). https://doi.org/10.1007/s10990-009-9046-8
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10990-009-9046-8