Deductive stability proofs for ordinary differential equations

DOI10.1007/978-3-030-72013-1_10zbMath1474.68195arXiv2010.13096OpenAlexW3145752227MaRDI QIDQ2233505

André Platzer, Yong Kiam Tan

Publication date: 18 October 2021

Full work available at URL: https://arxiv.org/abs/2010.13096

zbMATH Keywords

stabilitydifferential equationsdifferential dynamic logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by ordinary differential equations (93C15) Stability theory for ordinary differential equations (34D99) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Verifying Switched System Stability With Logic ⋮ Notes on Recent Achievements in Proving Stability using KeYmaeraX

Uses Software

• Coq
• Isabelle/HOL
• Bellerophon
• KeYmaera X

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The twisting tennis racket
• Local stability analysis using simulations and sum-of-squares programming
• Stability theory by Liapunov's direct method
• Switching in systems and control
• A formal proof in Coq of Lasalle's invariance principle
• Bellerophon: tactical theorem proving for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
• An axiomatic approach to existence and liveness for differential equations
• Handbook of networked and embedded control systems.
• The Complete Proof Theory of Hybrid Systems
• Simulation-guided lyapunov analysis for hybrid dynamical systems
• Verification of Hybrid Systems
• The dynamical systems approach to differential equations
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Logical Foundations of Cyber-Physical Systems
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
• Differential Equation Invariance Axiomatization
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Hybrid Systems: Computation and Control

This page was built for publication: Deductive stability proofs for ordinary differential equations