A Formal Proof in Coq of LaSalle's Invariance Principle - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

A Formal Proof in Coq of LaSalle's Invariance Principle

Cyril Cohen
Damien Rouhling

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

Citer

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⟩
503 Consultations
670 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More