129 citations · 181 across the 11 of their papers we have counts for
3 papers · 1 filter
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
Daniele Ahmed, Andrea Peruffo, Alessandro Abate
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as t…
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
Andrea Peruffo, Daniele Ahmed, Alessandro Abate
We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The…
Formal Synthesis of Lyapunov Neural Networks
Alessandro Abate, Daniele Ahmed, Mirco Giacobbe +1
We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either…