Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2015: Static Analysis pp 235–251Cite as

Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9291))

Abstract

While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains.

We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This invariant generation can be guided by either boundedness, or in contrary, a given zone of the state space to avoid.

While the target property is not necessarily inductive with respect to the program semantics, our method identifies a stronger inductive polynomial invariant using numerical optimization. Our method applies to a wide set of programs: a main while loop composed of a disjunction (if-then-else) of polynomial updates e.g. piecewise polynomial controllers. It has been evaluated on various programs.

A. Adjé and P.-L. Garoche—is supported by the RTRA /STAE Project BRIEFCASE and the ANR ASTRID VORACE Project.

V. Magron—is supported by EPSRC (EP/I020457/1) Challenging Engineering Grant.

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

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.

    Note that most existing SDP solvers are implemented based on inexact computation. In practice, we perform post-processing verification (Yalmip command “checkset”), ensuring that computed polynomials are SOS.

  2. 2.

    This approach also handles semialgebraic program termination.

References

  1. Adjé, A.: Policy iteration in finite templates domain. In: 7th International Workshop on Numerical Software Verification (NSV 2012), July 2014

    Google Scholar 

  2. Adjé, A., Garoche, P.-L., Magron. V.: A Sums-of-squares extension of policy iterations. Technial report (2015)

    Google Scholar 

  3. Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Log. Methods Comput. Sci. 8(1), 1–32 (2011)

    Google Scholar 

  4. Ahmadi, A.A., Jungers, R.M.: Switched stability of nonlinear systems via sos-convex lyapunov functions and semidefinite programming. In: CDC 2013, pp. 727–732 (2013)

    Google Scholar 

  5. Andersen, E.D., Andersen, K.D.: The mosek interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization. Applied Optimization, vol. 33, pp. 197–232. Springer, US (2000)

    Chapter  Google Scholar 

  6. Bagnara, R., Rodríguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invariants using convex polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 19–34. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to gröbner bases. Sci. Comput. Program. 93, 89–109 (2014)

    Article  Google Scholar 

  8. Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, Los Angeles, California, New York (1977)

    Google Scholar 

  10. Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the bernstein expansion. Reliab. Comput. 17(2), 128–152 (2012)

    MathSciNet  Google Scholar 

  11. Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796–817 (2001)

    Article  MathSciNet  Google Scholar 

  13. Laurent, M.: Sums of squares, moment matrices and optimization over polynomials. In: Putinar, M., Sullivant, S. (eds.) Emerging Applications of AlgebraicGeometry. The IMA Volumes in Mathematics and its Applications, vol. 149, pp. 157–270. Springer, New York (2009)

    Chapter  Google Scholar 

  14. Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. Sci. China Inf. Sci. 57(5), 1–13 (2014)

    Article  MathSciNet  Google Scholar 

  15. Magron, V., Allamigeon, X., Gaubert, S., Werner, B.: Certification of real inequalities - templates and sums of squares. Math. Program. Ser. B 151, 1–30 (2014). Volume on Polynomial Optimization

    Google Scholar 

  16. Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004)

    Article  Google Scholar 

  17. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)

    Article  MathSciNet  Google Scholar 

  18. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)

    Article  Google Scholar 

  20. Roux, P., Garoche, P.-L.: A polynomial template abstract domain based on bernstein polynomials. In: Sixth International Workshop on Numerical Software Verification, NSV 2013 (2013)

    Google Scholar 

  21. Roux, P., Jobredeaux, R., Garoche, P.-L., Feron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: Dang, T., Mitchell, I.M. (eds.) HSCC, pp. 105–114. ACM (2012)

    Google Scholar 

  22. Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A.: Reachability analysis of polynomial systems using linear programming relaxations. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 137–151. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. SIGPLAN Not. 44(6), 223–234 (2009)

    Article  Google Scholar 

  24. Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49–95 (1994)

    Article  MathSciNet  Google Scholar 

  25. Waki, H., Kim, S., Kojima, M., Muramatsu, M.: Sums of squares and semidefinite programming relaxations for polynomial optimization problems with structured sparsity. SIAM J. Optim. 17(1), 218–242 (2006)

    Article  MathSciNet  Google Scholar 

  26. Yamashita, M., Fujisawa, K., Nakata, K., Nakata, M., Fukuda, M., Kobayashi, K., Goto, K.: A high-performance software package for semidefinite programs : Sdpa7. Depatrment of Information Sciences, Tokyo Institute of Technology, Tokyo, Japan, Technical report (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Onera, The French Aerospace laboratory, Université de Toulouse, 31400, Toulouse, France

    Assalé Adjé & Pierre-Loïc Garoche

  2. Circuits and Systems Group, Department of Electrical and Electronic Engineering, Imperial College London, South Kensington Campus, London, SW7 2AZ, UK

    Victor Magron

Authors
  1. Assalé Adjé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre-Loïc Garoche
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Victor Magron
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pierre-Loïc Garoche .

Editor information

Editors and Affiliations

  1. Université Rennes 1, Rennes, France

    Sandrine Blazy

  2. Inria, Rennes, France

    Thomas Jensen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Adjé, A., Garoche, PL., Magron, V. (2015). Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization. In: Blazy, S., Jensen, T. (eds) Static Analysis. SAS 2015. Lecture Notes in Computer Science(), vol 9291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48288-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48288-9_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48287-2

  • Online ISBN: 978-3-662-48288-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation