Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers

DOI10.1007/978-3-030-45190-5_6OpenAlexW3016425199MaRDI QIDQ5039505

Alessandro Abate, Daniele Ahmed, Andrea Peruffo

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

Lyapunov functionsautomated synthesisinductive synthesiscounter-example-guided synthesis

Mathematics Subject Classification ID

Lyapunov and storage functions (93D30) Stability of solutions to ordinary differential equations (34D20) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

FOSSIL ⋮ Verifying Switched System Stability With Logic ⋮ Counterexample-guided computation of polyhedral Lyapunov functions for piecewise linear systems ⋮ Learning lyapunov functions for hybrid systems ⋮ Deductive stability proofs for ordinary differential equations ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models

Uses Software

• Mathematica
• Matlab
• Sostools
• SeDuMi
• Gurobi
• z3
• dReal
• Python
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Review on computational methods for Lyapunov functions
• Classical converse theorems in Lyapunov's second method
• Decision procedures. An algorithmic point of view
• Stability by Liapunov's direct method. With applications
• An alternative converse Lyapunov theorem for discrete-time systems
• Automated formal synthesis of provably safe digital controllers for continuous plants
• Simulation-guided lyapunov analysis for hybrid dynamical systems
• Stability of dynamical systems: A constructive approach
• Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
• Handbook of Model Checking
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

This page was built for publication: Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers