Skip to main content
SpringerLink
Log in

A minimalistic look at widening operators

  • Published:
Higher-Order and Symbolic Computation

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  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

    Chapter  Google Scholar 

  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

    MATH  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  5. Clarke, E.M. Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999). ISBN 0-262-03270-8.

    Google Scholar 

  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. 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

  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. http://www.di.ens.fr/~cousot/COUSOTpapers/VMCAI05.shtml

    Google Scholar 

  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. 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. D’Silva, V.: Widening for automata. Diplomarbeit, Universität Zürich (2006)

  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

    Chapter  Google Scholar 

  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). http://tel.archives-ouvertes.fr/tel-00288805/en/. In French

  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. Miné, A.: Weakly relational numerical abstract domains. PhD thesis, École polytechnique, Palaiseau, France (December 2004). In English

  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

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Pichardie, D.: Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1 (2005). In French

  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 

Download references

Author information

Authors and Affiliations

  1. CNRS/VERIMAG, 2 avenue de Vignate, 36810, Gières, France

    David Monniaux

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Monniaux.

Additional information

VERIMAG is a joint laboratory of CNRS, Université Joseph Fourier and Grenoble-INP.

Rights and permissions

Reprints 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

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10990-009-9046-8

Search

Navigation