×

Validating numerical semidefinite programming solvers for polynomial invariants. (English) Zbl 1425.68081

Summary: 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65K05 Numerical mathematical programming methods
90C22 Semidefinite programming
PDFBibTeX XMLCite
Full Text: DOI HAL

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 · Zbl 1260.68082
[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., Determining protein structures from NOESY distance constraints by semidefinite programming, J Comput Biol, 20, 296-310, (2013)
[5] Alizadeh, F.; Haeberly, J-PA; Overton, ML, Primal-dual interior-point methods for semidefinite programming: convergence rates, stability and numerical results, SIAM J Optim, 8, 746-768, (1998) · Zbl 0911.65047
[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 · Zbl 1235.90002
[8] Bagnara R, Rodríguez-Carbonell E, Zaffanella E (2005) Generation of basic semi-algebraic invariants using convex polyhedra. In: SAS · Zbl 1141.68446
[9] Basu S, Pollock R, Roy M-F (2006) Algorithms in real algebraic geometry. Springer, Berlin
[10] Ben-Tal A, Ghaoui LE (2009) Robust optimization. Princeton series in applied mathematics. Princeton University Press, Princeton
[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 · Zbl 1397.93189
[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, Characterization of optimality for the abstract convex program with finite-dimensional range, J. Aust. Math. Soc. Ser. A, 30, 390-411, (1980)
[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., Regularizing the abstract convex program, J Math Anal Appl, 83, 495-530, (1981) · Zbl 0467.90076
[17] Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge university press, Cambridge · Zbl 1058.90049
[18] Burkowski, F.; Cheung, Y-L; Wolkowicz, H., Efficient use of semidefinite programming for selection of rotamers in protein conformations, Inform J Comput, 26, 748-766, (2014) · Zbl 1304.90224
[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.; Bailey, DH (ed.); Bauschke, HH (ed.); Borwein, P. (ed.); Garvan, F. (ed.); Thera, M. (ed.); Vanderwerff, J. (ed.); Wolkowicz, H. (ed.), Preprocessing and regularization for degenerate semidefinite programs, (2013), Berlin
[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 · Zbl 0754.68063
[24] Cousot P (2005) Proving program invariance and termination by parametric abstraction. lagrangian relaxation and semidefinite programming. In: VMCAI · Zbl 1111.68503
[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 · Zbl 1149.68389
[26] Dang T, Gawlitza TM (2011) Template-based unbounded time verification of affine hybrid automata. In: APLAS · Zbl 1348.68100
[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] Ghaoui, L.; Oustry, F.; Lebret, H., Robust solutions to uncertain semidefinite programs, SIAM J Optim, 9, 33-52, (1998) · Zbl 0960.93007
[31] Farouki RT (2012) The Bernstein polynomial basis: a centennial retrospective. Comput Aided Geomet Des · Zbl 1252.65039
[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 · Zbl 1144.68371
[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 · Zbl 1381.68268
[35] Gaubert S, Goubault E, Taly A, Zennou S (2007) Static analysis by policy iteration on relational domains. In: ESOP · Zbl 1187.68151
[36] Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: ESOP · Zbl 1187.68152
[37] Gawlitza TM, Monniaux D (2011) Improving strategies via SMT solving. In: ESOP · Zbl 1326.68093
[38] Gawlitza TM, Seidl H (2010) Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: SAS · Zbl 1306.68025
[39] Gruber, G.; Rendl, F., Computational experience with ill-posed problems in semidefinite programming, Comput Optim Appl, 21, 201-212, (2002) · Zbl 0988.90024
[40] Handelman D (1988) Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J Math · Zbl 0659.52002
[41] Harrison J (2007) Verifying nonlinear real formulas via sums of squares. In: TPHOL · Zbl 1144.68357
[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: · Zbl 1008.90044
[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 · Zbl 1167.90009
[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 · Zbl 1229.90115
[48] Krislock, N.; Wolkowicz, H., Explicit sensor network localization using semidefinite representations and facial reductions, SIAM J Optim, 20, 2679-2708, (2010) · Zbl 1229.90250
[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 · Zbl 1367.90002
[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 · Zbl 1342.68296
[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 · Zbl 0824.90112
[58] Nie, J.; Ranestad, K.; Sturmfels, B., The algebraic degree of semidefinite programming, Math Program, 122, 379-405, (2008) · Zbl 1184.90119
[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 · Zbl 1381.68178
[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 · Zbl 1043.14018
[63] Pataki, G.; Bailey, DH (ed.); Bauschke, HH (ed.); Borwein, P. (ed.); Garvan, F. (ed.); Thera, M. (ed.); Vanderwerff, J. (ed.); Wolkowicz, H. (ed.), Strong duality in conic linear programming: facial reduction and extended duals, 613-634, (2013), Berlin
[64] Permenter F, Parrilo P (2014) Partial facial reduction: simplified, equivalent sdps via approximations of the psd cone. arXiv preprint arXiv:1408.4685 · Zbl 1405.90098
[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 · Zbl 1156.65062
[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 · Zbl 1135.93317
[69] Putinar M (1993) Positive polynomials on compact semi-algebraic sets. Indiana Univ Math J · Zbl 0796.12002
[70] Ramana, MV; Tunçel, L.; Wolkowicz, H., Strong duality for semidefinite programming, SIAM J Optim, 7, 641-662, (1997) · Zbl 0891.90129
[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 · Zbl 1409.68263
[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 · Zbl 1394.68085
[74] Rump SM (2006) Verification of positive definiteness. BIT Numer Math · Zbl 1101.65039
[75] Sankaranarayanan S, Sipma H, Manna Z (2008) Constructing invariants for hybrid systems. Formal Methods Syst Des · Zbl 1133.68365
[76] Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: VMCAI · Zbl 1111.68514
[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 · Zbl 0787.90088
[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 · Zbl 1366.68102
[81] Sturm, JF, Error bounds for linear matrix inequalities, SIAM J Optim, 10, 1228-1248, (2000) · Zbl 0999.90027
[82] Sturm JF (1999) Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim Methods Softw
[83] Sturm, JF, Implementation of interior point methods for mixed semidefinite and second order cone optimization problems, Optim Methods Softw, 17, 1105-1154, (2002) · Zbl 1032.90021
[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 · Zbl 1207.90005
[86] Tütüncü RH, Toh KC, Todd MJ (2003) Solving semidefinite-quadratic-linear programs using SDPT3. Mathematical programming
[87] Vandenberghe, L.; Boyd, S., Semidefinite programming, SIAM Rev, 38, 49-95, (1996) · Zbl 0845.65023
[88] Waki, H.; Muramatsu, M., A facial reduction algorithm for finding sparse SOS representations, Oper Res Lett, 38, 361-365, (2010) · Zbl 1205.90219
[89] Waki, H.; Muramatsu, M., Facial reduction algorithms for conic optimization problems, J Optim Theory Appl, 158, 188-215, (2013) · Zbl 1272.90048
[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 · Zbl 1264.90162
[91] Weispfenning V (1997) Quantifier elimination for real algebra—the quadratic case and beyond. In: Applied algebra and error-correcting codes (AAECC) · Zbl 0867.03003
[92] Wolkowicz, H.; Zhao, Q., Semidefinite programming relaxations for the graph partitioning problem, Discrete Appl. Math., 96/97, 461-479, (1999) · Zbl 0932.90030
[93] Wolkowicz H, Saigal R, Vandenberghe L (2000) Handbook of semidefinite programming. Kluwer Academic Publishers, Dordrecht
[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) · Zbl 0904.90145
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.