Article

The Zonotope Abstract Domain Taylor1+

Authors:

Khalil Ghorbal,

Sylvie PutotAuthors Info & Claims

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

Pages 627 - 633

https://doi.org/10.1007/978-3-642-02658-4_47

Published: 23 June 2009 Publication History

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.

References

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

[2]

APRON Project. Numerical abstract domain library (2007), http://apron.cri. ensmp.fr

[3]

Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SIBGRAPI 1993 (1993).

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

[5]

Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis (2008), http://arxiv.org/abs/0807.2961

[6]

Miné, A.: The Octagon abstract domain. Higher-Order and Symbolic Computation, 31-100 (2006).

[7]

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978, pp. 84-97 (1978).

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

[9]

Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Symposium on Discrete Algorithms, pp. 803-812 (2003).

[10]

Kühn, W.: Zonotope dynamics in numerical quality control. In: Mathematical Visualization, pp. 125-134. Springer, Heidelberg (1998).

[11]

Jeannet., B., et al.: Newpolka library, http://www.inrialpes.fr/pop-art/ people/bjeannet/newpolka

[12]

PPL Project. The Parma Polyhedra Library, http://www.cs.unipr.it/ppl/

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

[14]

Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: FMICS (2007).

[15]

Borchers, B.: A C library for Semidefinite Programming (1999), https:// projects.coin-or.org/Csdp

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

Cited By

Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
Liu JXing YShi XSong FXu ZMing Z(2024)Abstraction and Refinement: Towards Scalable and Exact Verification of Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/364438733:5(1-35)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3644387
Fassina NRanzato FZanella M(2024)Robustness verification of k-nearest neighbors by abstract interpretationKnowledge and Information Systems10.1007/s10115-024-02108-466:8(4825-4859)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10115-024-02108-4
Show More Cited By

Recommendations

The octagon abstract domain

This article presents the octagon abstract domain , a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form X Y c where X and Y range among program ...
The octahedron abstract domain

An interesting area in static analysis is the study of numerical properties. Complex properties can be analyzed using abstract interpretation, provided that an adequate abstract domain is defined. Each domain can represent and manipulate a family of ...
The Octagon Abstract Domain
WCRE '01: Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01)

This article presents a new numerical abstract domain for static analysis by abstract interpretation. It extends our previously proposed DBM-based numerical abstract domain and allows us to represent invariants of the form (\pm x \pm y lleq c), where x ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

June 2009

720 pages

ISBN:9783642026577

Editors:
Ahmed Bouajjani
LIAFA, University Paris Diderot (Paris 7), Case 7014, Paris Cedex 13, France 75205
,
Oded Maler
Verimag, Centre Equation, Gières, France 38610

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 23 June 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
Liu JXing YShi XSong FXu ZMing Z(2024)Abstraction and Refinement: Towards Scalable and Exact Verification of Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/364438733:5(1-35)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3644387
Fassina NRanzato FZanella M(2024)Robustness verification of k-nearest neighbors by abstract interpretationKnowledge and Information Systems10.1007/s10115-024-02108-466:8(4825-4859)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10115-024-02108-4
Bacci GBacci GLarsen KSquillace GTribastone MTschaikowski MVandin A(2024)Dissimilarity for Linear Dynamical SystemsQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_8(125-142)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_8
Pal ARanzato FUrban CZanella M(2024)Abstract Interpretation-Based Feature Importance for Support Vector MachinesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_2(27-49)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_2
Laurel JQian SSingh GMisailovic S(2023)Synthesizing Precise Static Analyzers for Automatic DifferentiationProceedings of the ACM on Programming Languages10.1145/36228677:OOPSLA2(1964-1992)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622867
Boudardara FBoussif AMeyer PGhazel M(2023)A review of abstraction methods towards verifying neural networksACM Transactions on Embedded Computing Systems10.1145/3617508Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1145/3617508
Müller MFischer MStaab RVechev M(2023)Abstract Interpretation of Fixpoint Iterators with Applications to Neural NetworksProceedings of the ACM on Programming Languages10.1145/35912527:PLDI(786-810)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591252
Bak SDohmen TSubramani KTrivedi AVelasquez AWojciechowski P(2023)The Octatope Abstract Domain for Verification of Neural NetworksFormal Methods10.1007/978-3-031-27481-7_26(454-472)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_26
Laurel JYang RUgare SNagel RSingh GMisailovic S(2022)A general construction for abstract interpretation of higher-order automatic differentiationProceedings of the ACM on Programming Languages10.1145/35633246:OOPSLA2(1007-1035)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563324
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten