The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in guidance of systems. Unfortunately, those algorithms are still seen as new and obscure and are not considered as a viable option for safety critical roles. This paper deals with the formal verification of convex optimization algorithms. Additionally, we demonstrate how theoretical proofs of real-time convex optimization algorithms can be used to describe functional properties at the code level, thereby making it accessible for the formal methods community. In seeking zero-bug software, we use the Credible Autocoding framework. We focused our attention on the Ellipsoid Algorithm solving second-order cone programs (SOCP). The paper also considers floating-point errors and gives a framework to numerically validate the method.
|Original language||English (US)|
|Title of host publication||Proceedings of the IEEE Conference on Decision and Control|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||7|
|State||Published - Jan 18 2019|