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

Raphael Cohen, Eric Feron, Pierre Loïc Garoche

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish (US)
Title of host publicationProceedings of the IEEE Conference on Decision and Control
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages7
ISBN (Print)9781538613955
StatePublished - Jan 18 2019
Externally publishedYes

Bibliographical note

Generated from Scopus record by KAUST IRTS on 2021-02-18


Dive into the research topics of 'Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs'. Together they form a unique fingerprint.

Cite this