Abstract
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.
This work was partially funded by the ANR project ASOPT.
Chapter PDF
Similar content being viewed by others
References
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)
APRON Project. Numerical abstract domain library (2007), http://apron.cri.ensmp.fr
Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SIBGRAPI 1993 (1993)
Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)
Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis (2008), http://arxiv.org/abs/0807.2961
Miné, A.: The Octagon abstract domain. Higher-Order and Symbolic Computation, 31–100 (2006)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978, pp. 84–97 (1978)
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)
Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Symposium on Discrete Algorithms, pp. 803–812 (2003)
Kühn, W.: Zonotope dynamics in numerical quality control. In: Mathematical Visualization, pp. 125–134. Springer, Heidelberg (1998)
Jeannet., B., et al.: Newpolka library, http://www.inrialpes.fr/pop-art/people/bjeannet/newpolka
PPL Project. The Parma Polyhedra Library, http://www.cs.unipr.it/ppl/
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)
Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: FMICS (2007)
Borchers, B.: A C library for Semidefinite Programming (1999), https://projects.coin-or.org/Csdp
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghorbal, K., Goubault, E., Putot, S. (2009). The Zonotope Abstract Domain Taylor1+. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_47
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)