Pegasus: sound continuous invariant generation
From MaRDI portal
Publication:2147687
DOI10.1007/S10703-020-00355-ZzbMATH Open1505.68045arXiv2005.09348OpenAlexW3123500159MaRDI QIDQ2147687FDOQ2147687
Authors: Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer 
Publication date: 20 June 2022
Published in: Formal Methods in System Design (Search for Journal in Brave)
Abstract: Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.
Full work available at URL: https://arxiv.org/abs/2005.09348
Recommendations
- A method for invariant generation for polynomial continuous systems
- Transcendental inductive invariants generation for non-linear differential and hybrid systems
- Bellerophon: tactical theorem proving for hybrid systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Hybrid Systems: Computation and Control
Specification and verification (program logics, model checking, etc.) (68Q60) Attainable sets, reachability (93B03) Software, source code, etc. for problems pertaining to ordinary differential equations (34-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Bellerophon: tactical theorem proving for hybrid systems
- Bellerophon
- ModelPlex
- Ideals, Varieties, and Algorithms
- Differential dynamic logic for hybrid systems
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- Nonlinear dynamical systems and control. A Lyapunov-based approach
- Stability theory by Liapunov's direct method
- Nonlinear systems
- Integrability and nonintegrability of dynamical systems
- Simulation-guided Lyapunov analysis for hybrid dynamical systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- Ordinary differential equations with applications
- Vector Lyapunov Functions
- Constructing invariants for hybrid systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Integrating a SAT solver with an LCF-style theorem prover
- Title not available (Why is that?)
- Real World Verification
- Fast LCF-Style Proof Reconstruction for Z3
- Elementary First Integrals of Differential Equations
- Title not available (Why is that?)
- Invariant algebraic surfaces of the Lorenz system
- First integrals of autonomous systems of differential equations and the Prelle-Singer procedure
- Computing closed form solutions of first order ODEs using the Prelle- Singer procedure
- On the nonexistence of rational first integrals for nonlinear systems and semiquasihomogeneous systems
- \(n-1\) independent first integrals for linear differential systems in \(\mathbb{R}^n\) or \(\mathbb{C}^n\)
- Title not available (Why is that?)
- Computing differential invariants of hybrid systems as fixed points
- Abstractions for hybrid systems
- Constraint-Based Approach for Analysis of Hybrid Systems
- A new algorithm for finding rational first integrals of polynomial vector fields
- Symbolic reachability computation for families of linear vector fields
- Title not available (Why is that?)
- Verification and synthesis using real quantifier elimination
- Vector barrier certificates and comparison systems
- Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Barrier certificates revisited
- Hybrid Systems: Computation and Control
- Title not available (Why is that?)
- Integrability of dynamical systems: algebra and analysis
- Construction of parametric barrier functions for dynamical systems using interval analysis
- A differential operator approach to equational differential invariants (invited paper)
- Logics of dynamical systems
- The Complete Proof Theory of Hybrid Systems
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- A complete uniform substitution calculus for differential dynamic logic
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
- Generating invariants for non-linear hybrid systems
- A method for invariant generation for polynomial continuous systems
- Reachability Analysis for Solvable Dynamical Systems
- Generating Box Invariants
- Extracting and representing qualitative behaviors of complex systems in phase space
- Title not available (Why is that?)
- Conic abstractions for hybrid systems
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Differential equation invariance axiomatization
- An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems
- Validating numerical semidefinite programming solvers for polynomial invariants
- Safety verification of nonlinear hybrid systems based on invariant clusters
Cited In (1)
Uses Software
This page was built for publication: Pegasus: sound continuous invariant generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147687)
