zbMATH — the first resource for mathematics

Credible autocoding of convex optimization algorithms. (English) Zbl 1364.90247
Summary: The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety-critical roles. There is a considerable body of mathematical proofs on on-line optimization algorithms which can be leveraged to assist in the development and verification of their implementation. In this paper, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the level of the code, thereby making it accessible for the formal methods community. The running example used in this paper is a generic semi-definite programming solver. Semi-definite programs can encode a wide variety of optimization problems and can be solved in polynomial time at a given accuracy. We describe a top-down approach that transforms a high-level analysis of the algorithm into useful code annotations. We formulate some general remarks on how such a task can be incorporated into a convex programming autocoder. We then take a first step towards the automatic verification of the optimization program by identifying key issues to be addressed in future work.
MSC:
 90C22 Semidefinite programming 90C51 Interior-point methods 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 90C25 Convex programming
Software:
ACSL; Chaff; CVXGEN; Frama-C; PVS; SDPT3; SeDuMi; YALMIP; z3
Full Text:
References:
 [1] Alizadeh, F, Interior point methods in semidefinite programming with applications to combinatorial optimization, SIAM J Optim, 5, 13-51, (1993) · Zbl 0833.90087 [2] Alizadeh, F; Haeberly, J-PA; Overton, ML, Primal-dual interior-point methods for semidefinite programming: convergence rates, stability and numerical results, SIAM J Optim, 5, 13-51, (1994) · Zbl 0911.65047 [3] Baudin P, Filliâtre J-C, Marché C, Monate B, Moy Y, Prevosto V (2008) ACSL: ANSI/ISO C specification language. http://frama-c.cea.fr/acsl.html. Accessed 22 Nov 2015 · Zbl 0973.90526 [4] Bodson, M, Evaluation of optimization methods for control allocation, J Guid Control Dyn, 25, 703-711, (2002) [5] Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge University Press, New York · Zbl 1058.90049 [6] Boyd S, El Ghaoui L, Feron E, Balakrishnan V (1994) Linear matrix inequalities in system and control theory. Studies in applied mathematics, vol 15. SIAM, Philadelphia · Zbl 0816.93004 [7] Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-C: a software analysis perspective. In: Proceedings of the 10th international conference on software engineering and formal methods, SEFM’12. Springer, Berlin, pp 233-247 · Zbl 0919.90109 [8] De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS’08/ETAPS’08. Springer, Berlin, pp 337-340 · Zbl 0189.50204 [9] Dieumegard A, Toom A, Pantel M (2012) Model-based formal specification of a DSL library for a qualified code generator. In: Proceedings of the 12th workshop on OCL and textual modelling, OCL ’12, New York, NY, USA, 2012. ACM, Innsbruck, Austria, pp 61-62 · Zbl 1293.65095 [10] Dijkstra, EW, Guarded commands, nondeterminacy and formal derivation of programs, Commun ACM, 18, 453-457, (1975) · Zbl 0308.68017 [11] Dijkstra E (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs · Zbl 0368.68005 [12] Floyd, RW, Assigning meanings to programs, Math Asp Comput Sci, 19, 19-32, (1967) · Zbl 0189.50204 [13] Gahinet, P; Apkarian, P, A linear matrix inequality approach to h$$∞$$ control, Int J Robust Nonlinear Control, 4, 421-448, (1994) · Zbl 0808.93024 [14] Gentzen, G, Untersuchungen über das logische schließen. i, Math Z, 39, 176-210, (1935) · Zbl 0010.14501 [15] Helmberg, C; Rendl, F; Vanderbei, RJ; Wolkowicz, H, An interior-point method for semidefinite programming, SIAM J Optim, 6, 342-361, (1996) · Zbl 0853.65066 [16] Hoare, CAR, An axiomatic basis for computer programming, Commun ACM, 12, 576-580, (1969) · Zbl 0179.23105 [17] Jobredeaux R (2015) Formal verification of control software. PhD Thesis, Georgia Institute of Technology · Zbl 0308.68017 [18] Kojima, M; Shindoh, S; Hara, S, Interior-point methods for the monotone semidefinite linear complementarity problem in symmetric matrices, SIAM J Optim, 7, 86-125, (1997) · Zbl 0872.90098 [19] Löfberg J (2004) YALMIP: a toolbox for modeling and optimization in MATLAB. IEEE international symposium on computer aided control systems design, 2004. Tapei, Taiwan. [20] Mattingley, J; Boyd, S, CVXGEN: a code generator for embedded convex optimization, Optim Eng, 13, 1-27, (2012) · Zbl 1293.65095 [21] McGovern LK (2000) Computational analysis of real-time convex optimization for control systems. PhD Thesis, Massachusetts Institute of Technology, Boston [22] McGovern L, Feron E (1998) Requirements and hard computational bounds for real-time optimization in safety-critical control systems. In: Proceedings of the 37th IEEE conference on decision and control, 1998, vol 3, pp 3366-3371 [23] Monteiro, RDC, Primal-dual path-following algorithms for semidefinite programming, SIAM J Optim, 7, 663-678, (1997) · Zbl 0913.65051 [24] Monteiro, RDC; Zhang, Y, A unified analysis for a class of long-step primal-dual path-following interior-point algorithms for semidefinite programming, Math Program, 81, 281-299, (1998) · Zbl 0919.90109 [25] Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th annual design automation conference, DAC ’01, New York, NY, USA, 2001. ACM, pp 530-535 [26] Nesterov, Y; Nemirovskii, A, A general approach to the design of optimal methods for smooth convex functions minimization, Ekon Mat Metod, 24, 509-517, (1988) [27] Nesterov Y, Nemirovskii A (1989) Self-concordant functions and polynomial time methods in convex programming. Materialy po matematicheskomu obespecheniiu EVM. USSR Academy of Sciences, Central Economic and Mathematic Institute · Zbl 1009.90080 [28] Nesterov Y, Nemirovskii A (1994) Interior-point polynomial algorithms in convex programming. Studies in applied mathematics. Society for Industrial and Applied Mathematics, Philadelphia · Zbl 0824.90112 [29] Nesterov, Y; Todd, MJ, Primal-dual interior-point methods for self-scaled cones, SIAM J Optim, 8, 324-364, (1995) · Zbl 0922.90110 [30] Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: CADE, LNAI, vol 607. Springer, Berlin, pp 748-752 [31] Owre S, Shankar N, Rushby JM, Stringer-Calvert DWJ (1999) PVS language reference. Computer Science Laboratory, SRI International, Menlo Park [32] Richter, S; Jones, CN; Morari, M, Certification aspects of the fast gradient method for solving the dual of parametric convex programs, Math Methods Oper Res, 77, 305-321, (2013) · Zbl 1272.90052 [33] Rinard M (1999) Credible compilation. In: Proceedings of CC 2001: international conference on compiler construction, technical report, 1999 · Zbl 0973.90526 [34] Roux P, Jobredeaux R, Garoche P-L, Feron E (2012) A generic ellipsoid abstract domain for linear time invariant systems. In: HSCC, 2012, pp 105-114 · Zbl 1362.93065 [35] RTCA (2011a) DO-333 formal methods supplement to DO-178C and DO-278A. Technical report [36] RTCA (2011b) DO-178C, software considerations in airborne systems and equipment certification [37] Sturm, JF, Using sedumi 1.02, a MATLAB toolbox for optimization over symmetric cones, Optim Methods Softw, 11, 625-653, (1999) · Zbl 0973.90526 [38] Todd, MJ, A study of search directions in primal-dual interior-point methods for semidefinite programming, Optim Methods Softw, 11, 1-46, (1999) · Zbl 0971.90109 [39] Todd, MJ, Semidefinite optimization, Acta Numer 2001, 10, 515-560, (2001) · Zbl 1105.65334 [40] Todd, M; Toh, K; Tütüncü, R, On the Nesterov-Todd direction in semidefinite programming, SIAM J Optim, 8, 769-796, (1998) · Zbl 0913.90217 [41] Toh, K-C; Todd, MJ; Tütüncü, RH, SDPT3—a MATLAB software package for semidefinite programming, version 1.3, Optim Methods Softw, 11, 545-581, (1999) · Zbl 0997.90060 [42] Turing AM (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines, pp 67-69 [43] Wang TE (2015) Credible autocoding of control software. PhD Thesis, Georgia Institute of Technology · Zbl 0922.90110 [44] Wang T, Jobredeaux R, Feron E (2011) A graphical environment to express the semantics of control systems. arXiv:1108.4048. Accessed 23 Nov 2015 · Zbl 0922.90110 [45] Wang T, Jobredeaux R, Herencia-Zapana H, Garoche P-L, Dieumegard A, Feron E, Pantel M (2013) From design to implementation: an automated, credible autocoding chain for control systems. In: CoRR, abs/1307.2641, 2013 [46] Yamashita M, Fujisawa K, Fukuda M, Kobayashi K, Nakata K, Nakata M (2012) Latest developments in the SDPA family for solving large-scale SDPs. In: Handbook on semidefinite, conic and polynomial optimization. Springer, New York, pp 687-713 · Zbl 1334.90119 [47] Zhang, S, Quadratic maximization and semidefinite relaxation, Math Program, 87, 453-465, (2000) · Zbl 1009.90080
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.