Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs

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.