Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Damien Rouhling Connect in order to contact the contributor
Submitted on : Friday, October 6, 2017 - 4:48:27 PM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Monday, January 8, 2018 - 2:17:10 PM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles