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.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/978-3-319-66107-0_10〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01612293
Contributeur : Damien Rouhling <>
Soumis le : vendredi 6 octobre 2017 - 16:48:27
Dernière modification le : jeudi 11 janvier 2018 - 15:51:51
Document(s) archivé(s) le : lundi 8 janvier 2018 - 14:17:10

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

381

Téléchargements de fichiers

70