A formal proof in Coq of Lasalle's invariance principle

DOI10.1007/978-3-319-66107-0_10zbMath1484.68315OpenAlexW2745776412MaRDI QIDQ1687728

Damien Rouhling, Cyril Cohen

Publication date: 4 January 2018

Full work available at URL: https://hal.inria.fr/hal-01612293/file/main.pdf

zbMATH Keywords

stabilitydynamical systemsformal proofsCoq

Mathematics Subject Classification ID

Stability of solutions to ordinary differential equations (34D20) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (4)

A Theory of Auto-Scaling for Resource Reservation in Cloud Services ⋮ Unnamed Item ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Deductive stability proofs for ordinary differential equations

Uses Software

• Coq
• PVS
• Coquelicot

Cites Work

• Unnamed Item
• Unnamed Item
• Stabilization of the inverted pendulum around its homoclinic orbit
• Coquelicot: a user-friendly library of real analysis for Coq
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• An extension of LaSalle's invariance principle for switched systems
• A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
• Defending the beauty of the Invariance Principle
• A Machine-Checked Proof of the Odd Order Theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• LaSalle-Yoshizawa Corollaries for Nonsmooth Systems
• Generalized Lyapunov and invariant set theorems for nonlinear dynamical systems

This page was built for publication: A formal proof in Coq of Lasalle's invariance principle