OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formal Verification for Embedded Implementation of Convex Optimization Algorithms

Cohen, Raphael and Davy, Guillaume and Feron, Eric and Garoche, Pierre-Loic Formal Verification for Embedded Implementation of Convex Optimization Algorithms. (2017) In: IFAC 2017 World Congress, 9 July 2017 - 14 July 2017 (Toulouse, France).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1016/j.ifacol.2017.08.1300


Advanced embedded algorithms are growing in complexity and length, related to the growth in autonomy, which allows systems to plan paths of their own. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that safety-critical applications must meet. This paper discusses the formal verification for optimization algorithms with a particular emphasis on receding-horizon controllers. Following a brief historical overview, a prototype autocoder for embedded convex optimization algorithms will be discussed. Options for encoding code properties and proofs, and their applicability and limitations will be detailed as well.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Volume 50, Issue 1
Audience (journal):International peer-reviewed journal
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Other partners > Georgia Institute of Technology (USA)
Other partners > Institut National des Sciences Appliquées - INSA (FRANCE)
Laboratory name:
Deposited On:14 Mar 2019 12:14

Repository Staff Only: item control page