A Formal Proof in Coq of LaSalle's Invariance Principle

Cyril Cohen 1 Damien Rouhling 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Stability analysis of dynamical systems plays an important role in the study of control techniques. LaSalle's invariance principle is a result about the asymptotic stability of the solutions to a nonlinear system of differential equations and several extensions of this principle have been designed to fit different particular kinds of system. In this paper we present a formalization, in the Coq proof assistant, of a slightly improved version of the original principle. This is a step towards a formal verification of dynamical systems.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01612293
Contributor : Damien Rouhling <>
Submitted on : Friday, October 6, 2017 - 4:48:27 PM
Last modification on : Thursday, January 11, 2018 - 3:51:51 PM
Long-term archiving on : Monday, January 8, 2018 - 2:17:10 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Cyril Cohen, Damien Rouhling. A Formal Proof in Coq of LaSalle's Invariance Principle. Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. ⟨10.1007/978-3-319-66107-0_10⟩. ⟨hal-01612293⟩

Share

Metrics

Record views

580

Files downloads

243