A Formal Proof in Coq of a Control Function for the Inverted Pendulum

Damien Rouhling 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Control theory provides techniques to design controllers, or control functions, for dynamical systems with inputs, so as to grant a particular behaviour of such a system. The inverted pendulum is a classic system in control theory: it is used as a benchmark for nonlinear control techniques and is a model for several other systems with various applications. We formalized in the Coq proof assistant the proof of soundness of a control function for the inverted pendulum. This is a first step towards the formal verification of more complex systems for which safety may be critical.
Liste complète des métadonnées

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-01639819
Contributor : Damien Rouhling <>
Submitted on : Monday, January 22, 2018 - 9:18:43 AM
Last modification on : Friday, April 27, 2018 - 2:40:07 PM

File

poplws18cppmain-id41-p-ef0777f...
Explicit agreement for this submission

Identifiers

Collections

Citation

Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.1-14, ⟨10.1145/3167101⟩. ⟨hal-01639819v2⟩

Share

Metrics

Record views

160

Files downloads

244