Skip to main content

Quadratic Zonotopes

An Extension of Zonotopes to Quadratic Arithmetics

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9458))

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.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

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

    Typically this involves a large number of loop unrolling, trying to minimize the number of actual uses of join/meet.

  3. 3.

    Tool and experiments available at https://cavale.enseeiht.fr/QuadZonotopes/.

References

  1. Bouissou, O., Mimram, S., Chapoutot, A.: Hyson: set-based simulation of hybrid systems. In: RSP, pp. 79–85. IEEE (2012)

    Google Scholar 

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

    Google Scholar 

  3. Dekker, T.J.: A floating-point technique for extending the available precision. Numerische Mathematik 18(3), 224–242 (1971)

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  6. Goubault, E., Le Gall, T., Putot, S.: An accurate join for zonotopes, preserving affine input/output relations. ENTCS 287, 65–76 (2012)

    Google Scholar 

  7. Ghorbal, K.: Static analysis of numerical programs: constrained affine sets abstract domain. Theses, Ecole Polytechnique X (2011)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  9. Grötschel, M., Lovász, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. Algorithms and Combinatorics. Springer, Heidelberg (1988)

    Book  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  11. Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. In: CoRR, abs/0910.1763 (2009)

    Google Scholar 

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

    Chapter  Google Scholar 

  13. Hansen, E.R.: A generalized interval arithmetic. In: Nickel, K. (ed.) Interval Mathematics. LNCS, vol. 29, pp. 7–18. Springer, Heidelberg (1975)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  15. Knuth, D.E.: Art of Computer Programming: Seminumerical Algorithms, vol. 2. Addison-Wesley Professional, New York (1997)

    Google Scholar 

  16. Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, December 2004

    Google Scholar 

  17. Messine, F., Touhami, A.: A general reliable quadratic form: an extension of affine arithmetic. Reliable Comput. 12(3), 171–192 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  18. Nesterov, Y., Nemirovskii, A.: Interior-Point Polynomial Algorithms in Convex Programming, vol. 13. SIAM, Philadelphia (1994)

    Book  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  20. Stolfi, J., De Figueiredo, L.H.: Self-validated numerical methods and applications. In: Brazilian Mathematics Colloquium monograph, IMPA, Rio de Janeiro, Brazil (1997)

    Google Scholar 

  21. Vavasis, S.A.: Quadratic programming is in NP. Inf. Process. Lett. 36(2), 73–77 (1990)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Pierre-Loïc Garoche .

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics