The Zonotope Abstract Domain Taylor1+

  • Khalil Ghorbal
  • Eric Goubault
  • Sylvie Putot
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


Static analysis by abstract interpretation [1] aims at automatically inferring properties on the behaviour of programs. We focus here on a specific kind of numerical invariants: the set of values taken by numerical variables, with a real numbers semantics, at each control point of a program.


  1. 1.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977, pp. 238–252 (1977)Google Scholar
  2. 2.
    APRON Project. Numerical abstract domain library (2007),
  3. 3.
    Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SIBGRAPI 1993 (1993)Google Scholar
  4. 4.
    Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis (2008),
  6. 6.
    Miné, A.: The Octagon abstract domain. Higher-Order and Symbolic Computation, 31–100 (2006)Google Scholar
  7. 7.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978, pp. 84–97 (1978)Google Scholar
  8. 8.
    Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Symposium on Discrete Algorithms, pp. 803–812 (2003)Google Scholar
  10. 10.
    Kühn, W.: Zonotope dynamics in numerical quality control. In: Mathematical Visualization, pp. 125–134. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Jeannet., B., et al.: Newpolka library,
  12. 12.
    PPL Project. The Parma Polyhedra Library,
  13. 13.
    Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: FMICS (2007)Google Scholar
  15. 15.
    Borchers, B.: A C library for Semidefinite Programming (1999),
  16. 16.
    Jansson, C., Chaykin, D., Keil, C.: Rigorous error bounds for the optimal value in semidefinite programming. SIAM J. Numer. Anal. 46(1), 180–200 (2007)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Khalil Ghorbal
    • 1
  • Eric Goubault
    • 1
  • Sylvie Putot
    • 1
  1. 1.CEA, LIST, Modelisation and Analysis of Systems in InteractionGif-sur-Yvette CedexFrance

Personalised recommendations