Higher-Order and Symbolic Computation

, Volume 22, Issue 2, pp 145–154 | Cite as

A minimalistic look at widening operators

  • David Monniaux


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.

Abstract interpretation Widening Termination Abstraction Well-founded tree Higher order Inductive definition Coq 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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 CrossRefGoogle Scholar
  2. 2.
    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 MATHGoogle Scholar
  3. 3.
    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 Google Scholar
  4. 4.
    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 CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M. Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999). ISBN 0-262-03270-8. Google Scholar
  6. 6.
    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 Google Scholar
  7. 7.
    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). In French
  8. 8.
    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. Google Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput., 511–547 (1992). ISSN 0955-792X. doi: 10.1093/logcom/2.4.511
  10. 10.
    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 Google Scholar
  11. 11.
    D’Silva, V.: Widening for automata. Diplomarbeit, Universität Zürich (2006) Google Scholar
  12. 12.
    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 CrossRefGoogle Scholar
  13. 13.
    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). In French
  14. 14.
    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 Google Scholar
  15. 15.
    Miné, A.: Weakly relational numerical abstract domains. PhD thesis, École polytechnique, Palaiseau, France (December 2004). In English Google Scholar
  16. 16.
    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 CrossRefGoogle Scholar
  17. 17.
    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) CrossRefGoogle Scholar
  18. 18.
    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 Google Scholar
  19. 19.
    Pichardie, D.: Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1 (2005). In French Google Scholar
  20. 20.
    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) Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2009

Authors and Affiliations

  1. 1.CNRS/VERIMAGGièresFrance

Personalised recommendations