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 1MB |
Official URL: https://doi.org/10.1016/j.ifacol.2017.08.1300
Abstract
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: | |
Statistics: | download |
Deposited On: | 14 Mar 2019 12:14 |
Repository Staff Only: item control page