Cargando…
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
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 the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specifi...
Autores principales: | Ahmed, Daniele, Peruffo, Andrea, Abate, Alessandro |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439753/ http://dx.doi.org/10.1007/978-3-030-45190-5_6 |
Ejemplares similares
-
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
por: Scott, Joseph, et al.
Publicado: (2021) -
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
por: Peruffo, Andrea, et al.
Publicado: (2021) -
Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
por: Jonáš, Martin, et al.
Publicado: (2020) -
SMT soldering handbook
por: Strauss, Rudolf, et al.
Publicado: (1998) -
Synthesis of Super-Optimized Smart Contracts Using Max-SMT
por: Albert, Elvira, et al.
Publicado: (2020)