Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download
Contributor : Damien Rouhling <>
Submitted on : Sunday, November 26, 2017 - 6:30:49 PM
Last modification on : Monday, February 3, 2020 - 10:06:02 AM


Files produced by the author(s)


  • HAL Id : hal-01639819, version 1



Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. 2017. ⟨hal-01639819v1⟩



Record views


Files downloads