Template polyhedra and bilinear optimization. (English) Zbl 1426.65079
Summary: In this paper, we study the template polyhedral abstract domain using connections to bilinear optimization techniques. The connections between abstract interpretation and convex optimization approaches have been studied for nearly a decade now. Specifically, data flow constraints for numerical domains such as polyhedra can be expressed in terms of bilinear constraints. Algorithms such as policy and strategy iteration have been proposed for the special case of bilinear constraints that arise from template polyhedra wherein the desired invariants conform to a fixed template form. In particular, policy iteration improves upon a known post-fixed point by alternating between solving for an improved post-fixed point against finding certificates that are used to prove the new fixed point. In the first part of this paper, we propose a policy iteration scheme that changes the template on the fly in order to prove a target reachability property of interest. We show how the change to the template
naturally fits inside a policy iteration scheme, and thus, propose a scheme that updates the template matrices associated with each program location. We demonstrate that the approach is effective over a set of benchmark instances, wherein, starting from a simple predefined choice of templates, the approach is able to infer appropriate template directions to prove a property of interest. However, it is well known that policy iteration can end up “stuck” in a saddle point from which future iterations cannot make progress. In the second part of this paper, we study this problem further by empirically comparing policy iteration with a variety of other approaches for bilinear programming. These approaches adapt well-known algorithms to the special case of bilinear programs as well as using off-the-shelf tools for nonlinear programming. Our initial experience suggests that policy iteration seems to be the most advantageous approach for problems arising from abstract interpretation, despite the potential problems
of getting stuck at a saddle point.
MSC:
| 65K05 | Numerical mathematical programming methods |
| 90C25 | Convex programming |
| 90C51 | Interior-point methods |
Keywords:
abstract interpretation; static analysis; bilinear programs; convex optimization; policy iteration; interior-point methodsSoftware:
LBFGS-B; BARON; Gurobi; PENNON; PPL; CVX; Ipopt; SeDuMi; QCQP; ASTREE; PolySpace; Bonmin; SpaceEx; CouenneReferences:
| [1] | Adjé A, Garoche P (2015) Automatic synthesis of piecewise linear quadratic invariants for programs. In: Verification, model checking, and abstract interpretation (VMCAI), pp 99-116 · Zbl 1432.68254 |
| [2] | Adjé A, Gaubert S, Goubault E (2012) Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. LMCS. https://doi.org/10.2168/LMCS-8(1:01)2012 · Zbl 1237.68054 |
| [3] | Adjé A, Gaubert S, Goubault E (2014) Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs. J Math Anal Appl 410(1):227-240 · Zbl 1309.47057 · doi:10.1016/j.jmaa.2013.07.076 |
| [4] | Amato G, Parton M, Scozzari F (2010) Deriving numerical abstract domains via principal component analysis. Springer, Berlin, pp 134-150 · Zbl 1306.68018 |
| [5] | Anstreicher KM (2009) Semidefinite programming versus the reformulation-linearization technique for nonconvex quadratically constrained quadratic programming. J Glob Optim 43(2):471-484 · Zbl 1169.90425 · doi:10.1007/s10898-008-9372-0 |
| [6] | Audet C, Hansen P, Jaumard B, Savard G (2000) A branch and cut algorithm for nonconvex quadratically constrained quadratic programming. Math Program 87(1):131-152 · Zbl 0966.90057 · doi:10.1007/s101079900106 |
| [7] | Bagnara R, Hill PM, Zaffanella E (2006) The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy |
| [8] | Bagnara R, Ricci E, Zaffanella E, Hill PM (2002) Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Static analysis symposium, vol 2477, pp 213-229 · Zbl 1015.68215 |
| [9] | Belotti P (2009) Couenne: a users manual. Technical report, Lehigh University |
| [10] | Bertsekas DP, Nedić A, Ozdaglar AE (2003) Convex analysis and optimization. Athena Scientific, Belmont · Zbl 1140.90001 |
| [11] | Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Programming language design and implementation, pp 196-207. ACM Press · Zbl 1026.68514 |
| [12] | Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2005) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software (invited chapter). In: In The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D. Jones. LNCS, vol. 2566, pp 85-108. Springer · Zbl 1026.68514 |
| [13] | Bogomolov S, Frehse G, Giacobbe M, Henzinger T (2017) Counterexample-guided refinement of template polyhedra. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin · Zbl 1452.68099 |
| [14] | Bonami P, Biegler LT, Conn AR, Cornuéjols G, Grossmann IE, Laird CD, Lee J, Lodi A, Margot F, Sawaya N (2008) An algorithmic framework for convex mixed integer nonlinear programs. Discrete Optim 5(2):186-204 · Zbl 1151.90028 · doi:10.1016/j.disopt.2006.10.011 |
| [15] | Byrd RH, Lu P, Nocedal J (1995) A limited memory algorithm for bound constrained optimization. SIAM J Sci Stat Comput 16(5):1190-1208 · Zbl 0836.65080 · doi:10.1137/0916069 |
| [16] | Chen X, Abraham E, Sankaranarayanan S (2012) Taylor model flowpipe construction for non-linear hybrid systems. In: Real time systems symposium (RTSS), pp 183-192. IEEE Press |
| [17] | Chen X, Erika Á (2012) Choice of directions for the approximation of reachable sets for hybrid systems. In: EUROCAST’11, pp 535-542. Springer, Berlin |
| [18] | Chvátal V (1983) Linear programming. Freeman, San Francisco · Zbl 0537.90067 |
| [19] | Clariso R, Cortadella J (2007) The octahedron abstract domain. Sci Comput Program 64(1):115-139 · Zbl 1171.68540 · doi:10.1016/j.scico.2006.03.009 |
| [20] | Colón M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: CAV, vol 2725, pp 420-433 · Zbl 1278.68164 |
| [21] | Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: Computer aided verification (CAV). Lecture notes in computer science, vol 3576, pp 462-475. Springer · Zbl 1081.68616 |
| [22] | Couenne, a solver for nonconvex minlp problems (2016). https://www.coin-or.org/Couenne/. Accessed 1 Sep 2018 |
| [23] | Cousot P (2005) Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: VMCAI. Lecture notes in computer science, vol 3385, pp 1-24. Springer · Zbl 1111.68503 |
| [24] | Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Proc. ISOP’76. Dunod, Paris, pp 106-130 · Zbl 0393.68080 |
| [25] | Cousot P, Cousot R (1992) Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In: PLILP’92. LNCS, vol 631, pp 269-295. Springer · Zbl 0776.68024 |
| [26] | Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM principles of programming languages, pp 238-252 |
| [27] | Dauphin YN, Pascanu R, Gulcehre C, Cho K, Ganguli S, Bengio Y (2014) Identifying and attacking the saddle point problem in high-dimensional non-convex optimization. In: Advances in neural information processing systems, pp 2933-2941 |
| [28] | Delmas D, Souyris J (2007) Astrée: from research to industry. In: Proceedings of 14th international static analysis symposium, SAS 2007. LNCS, vol 4634, pp 437-451. Springer, Berlin |
| [29] | Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV’11, vol 6806, pp 379-395 |
| [30] | Gaubert S, Goubault E, Taly A, Zennou S (2007) Static analysis by policy iteration on relational domains. In: European symposium on programming. Lecture notes in computer science, vol 4421, pp 237-252. Springer · Zbl 1187.68151 |
| [31] | Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: European symposium on programming (ESOP). Lecture notes in computer science, vol 4421, pp 300-315. Springer · Zbl 1187.68152 |
| [32] | Gawlitza TM, Seidl H (2011) Solving systems of rational equations through strategy iteration. ACM Trans Program Lang Syst 33(3):11:1-11:48 · doi:10.1145/1961204.1961207 |
| [33] | Ghaoui LE, Balakrishnan V (1994) Synthesis of fixed-structure controllers via numerical optimization. In: Proceedings of the 33rd conference on decision and control (CDC). IEEE |
| [34] | Goubault E, Putot S, Baufreton P, Gassino J (2008) Static analysis of the accuracy in control systems: principles and experiments. In: FMICS. LNCS, vol 4916, pp 3-20. Springer |
| [35] | Grant M, Boyd S (2008) Graph implementations for nonsmooth convex programs. In: Recent advances in learning and control, pp 95-110 · Zbl 1205.90223 |
| [36] | Grant M, Boyd S, Ye Y (2008) Cvx: Matlab software for disciplined convex programming |
| [37] | Guernic CL, Girard A (2010) Reachability analysis of linear systems using support functions. Nonlinear Anal Hybrid Syst 4(2):250-262 · Zbl 1201.93018 · doi:10.1016/j.nahs.2009.03.002 |
| [38] | Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: PLDI, pp 281-292. ACM |
| [39] | Gurobi Optimization Inc. (2017) Gurobi optimizer reference manual. http://www.gurobi.com. Accessed 1 Sep 2018 |
| [40] | Helton J, Merino O (1997) Coordinate optimization for bi-convex matrix inequalities. In: IEEE conference on decision and control (CDC), pp 3609-3613 |
| [41] | Jin C, Ge R, Netrapalli P, Kakade SM, Jordan MI (2017) How to escape saddle points efficiently. In: ICML |
| [42] | Kim S, Kojima M (2001) Second order cone programming relaxation of nonconvex quadratic optimization problems. Optim Methods Soft 15(3-4):201-224 · Zbl 1109.90327 · doi:10.1080/10556780108805819 |
| [43] | Kočvara M, Stingl M (2003) PENNON: a code for convex nonlinear and semidefinite programming. Optim Methods Softw 18(3):317-333 · Zbl 1037.90003 · doi:10.1080/1055678031000098773 |
| [44] | Lee JD, Simchowitz M, Jordan MI, Recht B (2016) Gradient descent only converges to minimizers. In: Conference on learning theory, pp 1246-1257 |
| [45] | Linderoth J (2005) A simplicial branch-and-bound algorithm for solving quadratically constrained quadratic programs. Math Program 103(2):251-282 · Zbl 1099.90039 · doi:10.1007/s10107-005-0582-7 |
| [46] | Logozzo F, Fähndrich M (2008) Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Symposium on applied computing, SAC ’08. ACM, New York, pp 184-188 · Zbl 1197.68035 |
| [47] | Mathworks Inc. PolySpace design verifier. http://www.mathworks.com/products/polyspace/. Accessed Apr 2017 |
| [48] | Miné A (2001) A new numerical abstract domain based on difference-bound matrices. In: PADO II, vol 2053, pp 155-172 · Zbl 0984.68034 |
| [49] | Miné A (October 2001) The octagon abstract domain. In: AST 2001 in WCRE 2001. IEEE, IEEE CS Press, pp 310-319 |
| [50] | Nielson F, Nielson HR, Hankin C (1999) Principles of program analysis. Springer, Berlin · Zbl 0932.68013 · doi:10.1007/978-3-662-03811-6 |
| [51] | Nocedal J, Wright S (2006) Numerical optimization, 2nd edn. Springer, Berlin · Zbl 1104.65059 |
| [52] | Park J, Boyd S (2017) General heuristics for nonconvex quadratically constrained quadratic programming. arXiv preprint arXiv:1703.07870 |
| [53] | Qualizza, A.; Belotti, P.; Margot, F.; Lee, J. (ed.); Leyffer, S. (ed.), Linear programming relaxations of quadratically constrained quadratic programs, 407-426 (2012), Berlin · Zbl 1242.90155 · doi:10.1007/978-1-4614-1927-3_14 |
| [54] | Rockafellar R, Wets R (2009) Variational analysis. Springer, Berlin · Zbl 0888.49001 |
| [55] | Roux P, Voronin YL, Sankaranarayanan S (2016) Validating numerical semidefinite programming solvers for polynomial invariants. In: Static analysis symposium (SAS). Lecture notes in computer science, vol 9837, pp 424-446. Springer · Zbl 1394.68085 |
| [56] | Sahinidis NV (2017) BARON 17.8.9: global optimization of mixed-integer nonlinear programs. User’s manual |
| [57] | Sankaranarayanan S (2005) Mathematical analysis of programs. PhD thesis, Stanford University |
| [58] | Sankaranarayanan S, Dang T, Ivančić F (2008) Symbolic model checking of hybrid systems using template polyhedra. In: TACAS. LNCS, vol 4963, pp 188-202. Springer · Zbl 1134.68419 |
| [59] | Sankaranarayanan S, Sipma HB, Manna Z (2004) Constraint-based linear-relations analysis. In: Static analysis symposium (SAS 2004), vol 3148, pp 53-69, Aug 2017 · Zbl 1104.68023 |
| [60] | Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Verification, model-checking and abstract-interpretation (VMCAI 2005), vol 3385, Jan 2005 · Zbl 1111.68514 |
| [61] | Sassi MAB, Girard A, Sankaranarayanan S (2014) Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: IEEE conference on decision and control (CDC), pp 6348-6353. IEEE Press |
| [62] | Sassi MAB, Sankaranarayanan S, Chen X, Ábraham E (2016) Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis. IMA J Math Control Inf 33:723-756 · Zbl 1397.93189 · doi:10.1093/imamci/dnv003 |
| [63] | Sherali HD, Dalkiran E, Liberti L (2012) Reduced rlt representations for nonconvex polynomial programming problems. J Glob Optim 52(3):447-469 · Zbl 1244.90185 · doi:10.1007/s10898-011-9757-3 |
| [64] | Sherali HD, Fraticelli BM (2002) Enhancing rlt relaxations via a new class of semidefinite cuts. J Glob Optim 22(1):233-261 · Zbl 1045.90044 · doi:10.1023/A:1013819515732 |
| [65] | Sturm JF (1999) Using SeDuMi 1.02, a Matlab toolbox for optimization over symmetric cones. Optim Methods Softw 11(1-4):625-653 · Zbl 0973.90526 · doi:10.1080/10556789908805766 |
| [66] | Tawarmalani M, Sahinidis NV (2005) A polyhedral branch-and-cut approach to global optimization. Math Program 103:225-249 · Zbl 1099.90047 · doi:10.1007/s10107-005-0581-8 |
| [67] | Venet A, Brat GP (2004) Precise and efficient static array bound checking for large embedded C programs. In: PLDI, pp 231-242. ACM |
| [68] | Wächter A, Biegler LT (2006) On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Math Program 106(1):25-57 · Zbl 1134.90542 · doi:10.1007/s10107-004-0559-y |
| [69] | Weispfenning V (1997) Quantifier elimination for real algebra – the quadratic case and beyond. In: Applied algebra and error-correcting codes (AAECC), vol 8, pp 85-101 · Zbl 0867.03003 |
| [70] | Zheng XJ, Sun XL, Li D (2011) Convex relaxations for nonconvex quadratically constrained quadratic programming: matrix cone decomposition and polyhedral approximation. Math Program 129(2):301-329 · Zbl 1236.90089 · doi:10.1007/s10107-011-0466-y |
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.
