1. Credible autocoding of convex optimization algorithms
- Author
-
Timothy Wang, Romain Jobredeaux, Didier Henrion, Pierre-Loïc Garoche, Eric Feron, Marc Pantel, Daniel Guggenheim School of Aerospace Engineering (GA TECH), Georgia Institute of Technology [Atlanta], Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et de Télécommunications (ENSEEIHT), Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées, ONERA - The French Aerospace Lab [Toulouse], ONERA, Équipe Méthodes et Algorithmes en Commande (LAAS-MAC), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Université de Toulouse (UT)-Université de Toulouse (UT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), and Université de Toulouse (UT)
- Subjects
Optimization ,PVS ,0209 industrial biotechnology ,Mathematical optimization ,Control and Optimization ,Optimization problem ,Theoretical computer science ,Computer science ,0211 other engineering and technologies ,Aerospace Engineering ,Systems and Control (eess.SY) ,02 engineering and technology ,020901 industrial engineering & automation ,frama-C ,[INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY] ,FOS: Electrical engineering, electronic engineering, information engineering ,Autocoding ,Control Theory ,Electrical and Electronic Engineering ,Formal Verification ,Formal verification ,Interior-point Method ,Civil and Structural Engineering ,021103 operations research ,Mechanical Engineering ,Probabilistic-based design optimization ,Solver ,Formal methods ,Convex optimization ,Computer Science - Systems and Control ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,[MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC] ,Lyapunov proofs ,Algorithm ,Software ,Interior point method - Abstract
International audience; 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 programs 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 (SDP) 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-to-down approach that transforms a high-level analysis of the algorithm into useful code annotations. We formulate some general remarks about 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 adressed in future work.
- Published
- 2016
- Full Text
- View/download PDF