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

Abstract

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.
Pages3585-3591
Number of pages7
ISBN (Print)9781538613955
DOIs
StatePublished - Jan 18 2019
Externally publishedYes

Fingerprint 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