A Formal Proof in Coq of LaSalle's Invariance Principle - Archive ouverte HAL Access content directly
Conference Papers Year :

A Formal Proof in Coq of LaSalle's Invariance Principle

(1) , (1)
1
Cyril Cohen
Damien Rouhling

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.
Fichier principal
Vignette du fichier
main.pdf (397.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01612293 , version 1 (06-10-2017)

Identifiers

Cite

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⟩
473 View
556 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More