Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm

Autor: Davy, Guillaume, Féron, Eric, Garoche, Pierre-Loïc, Henrion, Didier

Publikováno v: 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-22), Nov 2018, Awassa, Ethiopia. https://easychair.org/smart-program/LPAR-22/

Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more complex controls such as aggressive maneuvering or performing fuel-effici

Externí odkaz: http://arxiv.org/abs/1801.03833

Generation of codes and provable annotations of interior-point algorithms for critical embedded systems

Autor: Davy, Guillaume

Publikováno v: Algorithme et structure de données [cs.DS]. Institut Supérieur de l'Aéronautique et de l'Espace (ISAE), 2018. Français

The objective of this thesis is to contribute to the formal verification of such systems. We will focus in particular on the certification of the compilation of the model to the code. In particular, through the annotation generation at the core of th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::a6824296e56f47c310543e1591b54a7c
https://hal.archives-ouvertes.fr/tel-02190142