Validating numerical semidefinite programming solvers for polynomial invariants | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

Validating numerical semidefinite programming solvers for polynomial invariants

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Semidefinite programming (SDP) solvers are increasingly used as primitives in many program verification tasks to synthesize and verify polynomial invariants for a variety of systems including programs, hybrid systems and stochastic models. On one hand, they provide a tractable alternative to reasoning about semi-algebraic constraints. However, the results are often unreliable due to “numerical issues” that include a large number of reasons such as floating-point errors, ill-conditioned problems, failure of strict feasibility, and more generally, the specifics of the algorithms used to solve SDPs. These issues influence whether the final numerical results are trustworthy or not. In this paper, we briefly survey the emerging use of SDP solvers in the static analysis community. We report on the perils of using SDP solvers for common invariant synthesis tasks, characterizing the common failures that can lead to unreliable answers. Next, we demonstrate existing tools for guaranteed semidefinite programming that often prove inadequate to our needs. Finally, we present a solution for verified semidefinite programming that can be used to check the reliability of the solution output by the solver and a padding procedure that can check the presence of a feasible nearby solution to the one output by the solver. We report on some successful preliminary experiments involving our padding procedure.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. In the remainder of this paper, the word “invariant” is used for inductive invariant.

  2. Control theorists call (opposite of) such functions Lyapunov functions [32].

  3. Changing \(\sigma _i \ge 0\) to \(\sigma _i\) SOS in (4) is actually a strengthening rather than a relaxation. However, (4) can be viewed as a dual (maximize \(\gamma \text { s.t. } p - \gamma = \sum _i \sigma _i p_i\)) of the problem (3) of primary interest (minimize \(p(x) \text { s.t. } p_i(x) \ge 0\) for all i), which is then relaxed.

  4. Typically, matrices \(C_j\) can be of size \(n \times n\) for n up to a few hundreds.

  5. \(\left( {\begin{array}{c}n+d\\ n\end{array}}\right) \) of up to a few hundreds, for instance \(n \sim 10\) and \(d \sim 3\).

  6. There also exist first order methods handling larger problems but they provide less accurate solutions.

  7. If a matrix is positive semidefinite and one of its diagonal entry (e.g. the (1, 1) entry) equals 0, then the entire row and column that contain that diagonal entry (e.g., the first row and column) equal 0.

  8. As the linear system tends to become more and more ill-conditioned when approaching an optimal solution.

  9. An SDP defined by rational data does not necessarily have a rational solution [58, 85].

  10. Type double in C.

  11. The emulated floating-point operations are about thousand times slower than native processor operations.

  12. To get a “small” invariant, one minimizes the radius of the ball enclosing it [1].

  13. Assignments \(\tau \) often admit a fixpoint \({{\mathbf {x}}}_0 = \tau ({{\mathbf {x}}}_0)\) meaning that the condition \((p\circ \tau ) - p + \sigma \,g \ge 0\) boils down in \({{\mathbf {x}}}_0\) to \(\sigma ({{\mathbf {x}}}_0)\,g({{\mathbf {x}}}_0) \ge 0\) implying \(\sigma ({{\mathbf {x}}}_0) = 0\) when \(g({{\mathbf {x}}}_0) < 0\).

  14. In practice, \(c < 10^{-3}\) when coefficients of p are of order of magnitude 1.

  15. For \(n = 2\), \(d_\tau = 3\) and \(d = 8\), \(\left( {\begin{array}{c}n+\frac{d}{2}\\ n\end{array}}\right) = \left( {\begin{array}{c}6\\ 2\end{array}}\right) = 15\) whereas \(\left( {\begin{array}{c}n+\frac{d\,d_\tau }{2}\\ n\end{array}}\right) = \left( {\begin{array}{c}14\\ 2\end{array}}\right) = 91\).

  16. But less than 80 loc are needed to express the SOS problems (13) and (14), call SDP solvers and validate the result, thanks to the OSDP library.

  17. Semidefinite programming has already been used in SMT solvers [59, 80] but the issue of soundness in case of unsatisfiability answers remains to be studied.

References

  1. Adjé A, Garoche P-L, Magron, V (2015) Property-based polynomial invariant generation using sums-of-squares optimization. In: SAS, pp 235–251

  2. Adjé A, Gaubert S, Goubault É (2010) Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: ESOP

  3. Ahmadi AA, Majumdar A (2014) DSOS and SDSOS optimization: LP and SOCP-based alternatives to sum of squares optimization. In: Annual conference on information sciences and systems (CISS)

  4. Alipanahi B, Krislock N, Ghodsi A, Wolkowicz H, Donaldson L, Li M (2013) Determining protein structures from NOESY distance constraints by semidefinite programming. J Comput Biol 20(4):296–310

    Article  MathSciNet  Google Scholar 

  5. Alizadeh F, Haeberly J-PA, Overton ML (1998) Primal-dual interior-point methods for semidefinite programming: convergence rates, stability and numerical results. SIAM J Optim 8(3):746–768 (electronic)

    Article  MathSciNet  Google Scholar 

  6. Allamigeon X, Gaubert S, Goubault E, Putot S, Stott N (2015) A scalable algebraic method to infer quadratic invariants of switched systems. In: EMSOFT

  7. Anjos MF, Lasserre JB (2012) Introduction to semidefinite, conic and polynomial optimization. In: Handbook on semidefinite, conic and polynomial optimization. Springer

  8. Bagnara R, Rodríguez-Carbonell E, Zaffanella E (2005) Generation of basic semi-algebraic invariants using convex polyhedra. In: SAS

  9. Basu S, Pollock R, Roy M-F (2006) Algorithms in real algebraic geometry. Springer, Berlin

    Google Scholar 

  10. Ben-Tal A, Ghaoui LE (2009) Robust optimization. Princeton series in applied mathematics. Princeton University Press, Princeton

    Book  Google Scholar 

  11. Ben Sassi MA, Sankaranarayanan S, Chen X, Abraham E (2015) Linear relaxations of polynomial positivity for polynomial lyapunov function synthesis. IMA J Math Control Inf

  12. Bernstein SN (1912) Démonstration du théoréme de Weierstrass fondée sur le calcul des probabilités. Communcations de la Société Mathématique de Kharkov 2

  13. Borchers B (1999) CSDP, a C library for semidefinite programming. Optim Methods Softw

  14. Borwein JM (1980) Characterization of optimality for the abstract convex program with finite-dimensional range. J. Aust. Math. Soc. Ser. A 30(4):390–411 81

    Article  MathSciNet  Google Scholar 

  15. Borwein JM, Wolkowicz H (1980/81) Facial reduction for a cone-convex programming problem. J. Aust. Math. Soc. Ser. A,

  16. Borwein JM, Wolkowicz H (1981) Regularizing the abstract convex program. J Math Anal Appl 83(2):495–530

    Article  MathSciNet  Google Scholar 

  17. Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge university press, Cambridge

    Book  Google Scholar 

  18. Burkowski F, Cheung Y-L, Wolkowicz H (2014) Efficient use of semidefinite programming for selection of rotamers in protein conformations. Inform J Comput 26(4):748–766

    Article  MathSciNet  Google Scholar 

  19. Chakarov A, Voronin Y-L, Sankaranarayanan S (2016) Deductive proofs of almost sure persistence and recurrence properties. In: TACAS

  20. Cheung Y-L, Schurr S, Wolkowicz H (2013) Preprocessing and regularization for degenerate semidefinite programs. In: Bailey DH, Bauschke HH, Borwein P, Garvan F, Thera M, Vanderwerff J, Wolkowicz H (eds) Computational and analytical mathematics, in honor of Jonathan Borwein’s 60th birthday, volume 50 of springer proceedings in mathematics & statistics. Springer, Berlin

    Google Scholar 

  21. Cheung Y-L (2013) Preprocessing and reduction for semidefinite programming via facial reduction: theory and practice. PhD thesis, University of Waterloo

  22. Collins GE (1975) Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata theory and formal languages

  23. Collins GE, Hong H (1991) Partial cylindrical algebraic decomposition for quantifier elimination. J Symb Comput

  24. Cousot P (2005) Proving program invariance and termination by parametric abstraction. lagrangian relaxation and semidefinite programming. In: VMCAI

  25. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL

  26. Dang T, Gawlitza TM (2011) Template-based unbounded time verification of affine hybrid automata. In: APLAS

  27. Demmel J (1989) On floating point errors in Cholesky. LAPACK Working Note 14 CS-89-87. Department of Computer Science, University of Tennessee, Knoxville, TN, USA

  28. Dolzmann A, Sturm T (1997) REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull

  29. Dür M, Jargalsaikhan B, Still G (2012) The Slater condition is generic in linear conic programming

  30. El Ghaoui L, Oustry F, Lebret H (1998) Robust solutions to uncertain semidefinite programs. SIAM J Optim 9(1):33–52

    Article  MathSciNet  Google Scholar 

  31. Farouki RT (2012) The Bernstein polynomial basis: a centennial retrospective. Comput Aided Geomet Des

  32. Féron É (2010) From control systems to control software. Control Systems, IEEE

  33. Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J Satisf Boolean Model Comput Special Issue on SAT/CP Integr

  34. Gao S, Kong S, Clarke EM (2013) Dreal: an SMT solver for nonlinear theories over the reals. In: International conference on automated deduction (CADE), pp 208–214

  35. Gaubert S, Goubault E, Taly A, Zennou S (2007) Static analysis by policy iteration on relational domains. In: ESOP

  36. Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: ESOP

  37. Gawlitza TM, Monniaux D (2011) Improving strategies via SMT solving. In: ESOP

  38. Gawlitza TM, Seidl H (2010) Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: SAS

  39. Gruber G, Rendl F (2002) Computational experience with ill-posed problems in semidefinite programming. Comput Optim Appl 21(2):201–212

    Article  MathSciNet  Google Scholar 

  40. Handelman D (1988) Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J Math

  41. Harrison J (2007) Verifying nonlinear real formulas via sums of squares. In: TPHOL

  42. Härter V, Jansson C, Lange M (2016) VSDP: verified semidefinite programming. http://www.ti3.tuhh.de/jansson/vsdp/. Accessed on 28 March

  43. Helmberg C (2012) Semidefinite programming. https://www-user.tu-chemnitz.de/~helmberg/semidef.html. Last updated:

  44. Henrion D, Naldi S, Din MS El (2015) Exact algorithms for linear matrix inequalities. arXiv preprint arXiv:1508.03715

  45. IEEE Computer Society. IEEE standard for floating-point arithmetic. IEEE Standard 754-2008, 2008

  46. Jansson C, Chaykin D, Keil C (2007) Rigorous error bounds for the optimal value in semidefinite programming. SIAM J Numer Anal

  47. Kaltofen E, Li B, Yang Z, Zhi L (2012) Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J Symb Comput

  48. Krislock N, Wolkowicz H (2010) Explicit sensor network localization using semidefinite representations and facial reductions. SIAM J Optim 20(5):2679–2708

    Article  MathSciNet  Google Scholar 

  49. Lasserre JB (2001) Global optimization with polynomials and the problem of moments. SIAM J Optim

  50. Löfberg J (2009) Pre- and post-processing sum-of-squares programs in practice. In: IEEE transactions on automatic control

  51. Maréchal A, Fouilhé A, King T, Monniaux D, ël Périn M (2016) Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: VMCAI

  52. Martin-Dorel É, Roux P (2017) A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Yves B, Viktor V (eds) Proceedings of the 6th ACM SIGPLAN conference on certified programs and proofs, CPP 2017, Paris, France, January 16–17, 2017, pp 90–99. ACM,

  53. Mittelmann HD (2016) Decision tree for optimization software: semidefinite programming. http://plato.asu.edu/sub/nlores.html#semidef. Accessed on 28 March

  54. Monniaux D, Corbineau P (2011) On the generation of positivstellensatz witnesses in degenerate cases. In: ITP

  55. MOSEK ApS (2015) The MOSEK C optimizer API manual Version 7.1 (Revision 40)

  56. Nakata M (2010) A numerical evaluation of highly accurate multiple-precision arithmetic version of semidefinite programming solver: SDPA-GMP, -QD and -DD. In: Computer-aided control system design

  57. Nesterov Y, Nemirovskii A (1994) Interior-point polynomial algorithms in convex programming. Soc Ind Appl Math

  58. Nie J, Ranestad K, Sturmfels B (2008) The algebraic degree of semidefinite programming. Math Program 122(2):379–405

    Article  Google Scholar 

  59. Nuzzo P, Puggelli A, Seshia SA, Sangiovanni-Vincentelli AL (2010) Calcs: SMT solving for non-linear convex constraints. In: Bloem R, Sharygina N (eds) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design. Switzerland, FMCAD 2010, Lugano, October 20–23, pp 71–79. IEEE

  60. Oulamara M, Venet AJ (2015) Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation. In: CAV

  61. Parrilo P (2000) Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. PhD thesis, California Institute of Technology

  62. Parrilo PA (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program

  63. Pataki G (2013) Strong duality in conic linear programming: facial reduction and extended duals. In: Bailey DH, Bauschke HH, Borwein P, Garvan F, Thera M, Vanderwerff J, Wolkowicz H (eds) Computational and analytical mathematics, in honor of Jonathan Borwein’s 60th birthday, volume 50 springer proceedings in mathematics & statistics. Springer, Berlin, pp 613–634

    Google Scholar 

  64. Permenter F, Parrilo P (2014) Partial facial reduction: simplified, equivalent sdps via approximations of the psd cone. arXiv preprint arXiv:1408.4685

  65. Permenter F, Parrilo PA (2015) Tools for SDP facial reduction. https://github.com/frankpermenter/frlib. Accessed on 10 Apr 2015

  66. Peyrl H, Parrilo PA (2008) Computing sum of squares decompositions with rational coefficients. Theor Comput Sci

  67. Platzer A, Quesel J-D, Rümmer P (2009) Real world verification. In: CADE

  68. Prajna S, Jadbabaie A (2004) Safety verification using barrier certificates. In: HSCC

  69. Putinar M (1993) Positive polynomials on compact semi-algebraic sets. Indiana Univ Math J

  70. Ramana MV, Tunçel L, Wolkowicz H (1997) Strong duality for semidefinite programming. SIAM J Optim 7(3):641–662

    Article  MathSciNet  Google Scholar 

  71. Reid G, Wang F, Wolkowicz H, Wu W (2016) arxiv:1504.00931. Accessed on 31 Mar

  72. Roux P (2016) Formal proofs of rounding error bounds-with application to an automatic positive definiteness check. J Autom Reason

  73. Roux P, Voronin Y-L, Sankaranarayanan S (2016) Validating numerical semidefinite programming solvers for polynomial invariants. In Xavier R (ed) Static analysis - 23rd international symposium, SAS 2016, Edinburgh, UK, September 8–10, 2016, proceedings, volume 9837 of lecture notes in computer science, pp 424–446. Springer

  74. Rump SM (2006) Verification of positive definiteness. BIT Numer Math

  75. Sankaranarayanan S, Sipma H, Manna Z (2008) Constructing invariants for hybrid systems. Formal Methods Syst Des

  76. Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: VMCAI

  77. Schmieta SH, Pataki G (2016) Reporting solution quality for the DIMACS library of mixed semidefinite-quadratic-linear programs. http://dimacs.rutgers.edu/Challenges/Seventh/Instances/error_report.html. [Online; accessed 23 Mar 2016]

  78. Sherali HD, Cihan H, Tuncbilek CH (1991) A global optimization algorithm for polynomial programming using a reformulation-linearization technique. J Global Optim

  79. Shor NZ (1987) Class of global minimum bounds on polynomial functions. Cybernetics 1987. Originally in Russian: Kibernetika

  80. Shoukry Y, Nuzzo P, Sangiovanni-Vincentelli AL, Seshia SA, Pappas GJ, Tabuada P (2017) SMC: satisfiability modulo convex optimization. In: Goran F, Sayan M (eds) Proceedings of the 20th international conference on hybrid systems: computation and control, HSCC 2017, Pittsburgh, PA, USA, April 18–20, 2017, pages 19–28. ACM

  81. Sturm JF (2000) Error bounds for linear matrix inequalities. SIAM J Optim 10(4):1228–1248 (electronic)

    Article  MathSciNet  Google Scholar 

  82. Sturm JF (1999) Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim Methods Softw

  83. Sturm JF (2002) Implementation of interior point methods for mixed semidefinite and second order cone optimization problems. Optim Methods Softw 17(6):1105–1154

    Article  MathSciNet  Google Scholar 

  84. Tarski A (1951) A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley, Technical report

  85. Tuncel L (2010) Polyhedral and semidefinite programming methods in combinatorial optimization. American Mathematical Society

  86. Tütüncü RH, Toh KC, Todd MJ (2003) Solving semidefinite-quadratic-linear programs using SDPT3. Mathematical programming

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

    Article  MathSciNet  Google Scholar 

  88. Waki H, Muramatsu M (2010) A facial reduction algorithm for finding sparse SOS representations. Oper Res Lett 38(5):361–365

    Article  MathSciNet  Google Scholar 

  89. Waki H, Muramatsu M (2013) Facial reduction algorithms for conic optimization problems. J Optim Theory Appl 158(1):188–215

    Article  MathSciNet  Google Scholar 

  90. Waki H, Nakata M, Muramatsu M (2011) Strange behaviors of interior-point methods for solving semidefinite programming problems in polynomial optimization. Comput Optim Appl

  91. Weispfenning V (1997) Quantifier elimination for real algebra—the quadratic case and beyond. In: Applied algebra and error-correcting codes (AAECC)

  92. Wolkowicz H, Zhao Q (1999) Semidefinite programming relaxations for the graph partitioning problem. Discrete Appl. Math. 96/97:461–479 (The satisfiability problem (Certosa di Pontignano, 1996); Boolean functions)

    Article  MathSciNet  Google Scholar 

  93. Wolkowicz H, Saigal R, Vandenberghe L (2000) Handbook of semidefinite programming. Kluwer Academic Publishers, Dordrecht

    Book  Google Scholar 

  94. Yamashita M, Fujisawa K, Nakata K, Nakata M, Fukuda M, Kobayashi K, Goto K (2010) A high-performance software package for semidefinite programs: SDPA 7. Technical Report B-460, Tokyo Institute of Technology

  95. Zhao Q, Karisch SE, Rendl F, Wolkowicz H (1998) Semidefinite programming relaxations for the quadratic assignment problem. J Comb Optim 2(1):71–109. Semidefinite programming and interior-point approaches for combinatorial optimization problems (Toronto, ON, 1996)

Download references

Acknowledgements

The authors would like to thank Didier Henrion, Pierre-Loïc Garoche and Assalé Adjé for interesting discussions on this subject.

Author information

Authors and Affiliations

  1. ONERA – The French Aerospace Lab, Toulouse, France

    Pierre Roux

  2. University of Colorado, Boulder, CO, USA

    Yuen-Lam Voronin & Sriram Sankaranarayanan

Authors
  1. Pierre Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yuen-Lam Voronin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pierre Roux.

Additional information

This work was supported by the US National Science Foundation (NSF) under CNS-0953941 and CCF-1527075. All opinions expressed are those of the authors and not necessarily of the NSF.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Roux, P., Voronin, YL. & Sankaranarayanan, S. Validating numerical semidefinite programming solvers for polynomial invariants. Form Methods Syst Des 53, 286–312 (2018). https://doi.org/10.1007/s10703-017-0302-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-017-0302-y

Keywords

Search

Navigation