Implicit semi-algebraic abstraction for polynomial dynamical systems

DOI10.1007/978-3-030-81685-8_25zbMath1493.68217OpenAlexW3186194270MaRDI QIDQ832202

Ahmed Irfan, Alberto Griggio, Stefano Tonetta, Sergio Mover, Alessandro Cimatti

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_25

Mathematics Subject Classification ID

Nonlinear ordinary differential equations and systems (34A34) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Abstract simulation of reaction networks via Boolean networks

Uses Software

• SymPy
• KeYmaera
• z3
• MathSAT5
• PySMT
• CTIGAR
• KeYmaera X

Cites Work

• Unnamed Item
• Unnamed Item
• A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
• Computing differential invariants of hybrid systems as fixed points
• Differential dynamic logic for hybrid systems
• Infinite-state invariant checking with IC3 and predicate abstraction
• Abstractions for hybrid systems
• Barrier certificates for nonlinear model validation
• A Method for Invariant Generation for Polynomial Continuous Systems
• Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• Predicate abstraction for software verification
• The MathSAT5 SMT Solver
• Computer Aided Verification

This page was built for publication: Implicit semi-algebraic abstraction for polynomial dynamical systems