Abstract
Affine forms are a common way to represent convex sets of \(\mathbb {R}\) using a base of error terms \(\epsilon \in [-1, 1]^m\). Quadratic forms are an extension of affine forms enabling the use of quadratic error terms \(\epsilon _i \epsilon _j\).
In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide range of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms.
In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.
This work has been partially supported by an RTRA/STAE BRIEFCASE project grant, the ANR projects INS-2012-007 CAFEIN, and ASTRID VORACE.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
When the function or the set of constraints is convex, e.g. conic problems, numerical solvers can be used to efficiently compute a solution. For example, the cases of LP, QP, SOCP, or SDP programming.
- 2.
Typically this involves a large number of loop unrolling, trying to minimize the number of actual uses of join/meet.
- 3.
Tool and experiments available at https://cavale.enseeiht.fr/QuadZonotopes/.
References
Bouissou, O., Mimram, S., Chapoutot, A.: Hyson: set-based simulation of hybrid systems. In: RSP, pp. 79–85. IEEE (2012)
Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics (1993)
Dekker, T.J.: A floating-point technique for extending the available precision. Numerische Mathematik 18(3), 224–242 (1971)
Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain Taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009)
Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212–226. Springer, Heidelberg (2010)
Goubault, E., Le Gall, T., Putot, S.: An accurate join for zonotopes, preserving affine input/output relations. ENTCS 287, 65–76 (2012)
Ghorbal, K.: Static analysis of numerical programs: constrained affine sets abstract domain. Theses, Ecole Polytechnique X (2011)
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)
Grötschel, M., Lovász, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. Algorithms and Combinatorics. Springer, Heidelberg (1988)
Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 1–3. Springer, Heidelberg (2013)
Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. In: CoRR, abs/0910.1763 (2009)
Goubault, E., Putot, S., Védrine, F.: Modular static analysis with zonotopes. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 24–40. Springer, Heidelberg (2012)
Hansen, E.R.: A generalized interval arithmetic. In: Nickel, K. (ed.) Interval Mathematics. LNCS, vol. 29, pp. 7–18. Springer, Heidelberg (1975)
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)
Knuth, D.E.: Art of Computer Programming: Seminumerical Algorithms, vol. 2. Addison-Wesley Professional, New York (1997)
Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, December 2004
Messine, F., Touhami, A.: A general reliable quadratic form: an extension of affine arithmetic. Reliable Comput. 12(3), 171–192 (2006)
Nesterov, Y., Nemirovskii, A.: Interior-Point Polynomial Algorithms in Convex Programming, vol. 13. SIAM, Philadelphia (1994)
Ramana, M.V., Pardalos, P.M.: Semidefinite programming. In: Terlaky, T. (ed.) Interior Point Methods of Mathematical Programming. Applied Optimization, vol. 5, pp. 369–398. Springer, Heidelberg (1996)
Stolfi, J., De Figueiredo, L.H.: Self-validated numerical methods and applications. In: Brazilian Mathematics Colloquium monograph, IMPA, Rio de Janeiro, Brazil (1997)
Vavasis, S.A.: Quadratic programming is in NP. Inf. Process. Lett. 36(2), 73–77 (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Adjé, A., Garoche, PL., Werey, A. (2015). Quadratic Zonotopes. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-26529-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26528-5
Online ISBN: 978-3-319-26529-2
eBook Packages: Computer ScienceComputer Science (R0)