Pegasus: sound continuous invariant generation
From MaRDI portal
(Redirected from Publication:2147687)
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)
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.
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
Cites work
- scientific article; zbMATH DE number 3181355 (Why is no real title available?)
- scientific article; zbMATH DE number 53595 (Why is no real title available?)
- scientific article; zbMATH DE number 66690 (Why is no real title available?)
- scientific article; zbMATH DE number 107497 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 510309 (Why is no real title available?)
- scientific article; zbMATH DE number 517393 (Why is no real title available?)
- scientific article; zbMATH DE number 1023365 (Why is no real title available?)
- scientific article; zbMATH DE number 1956651 (Why is no real title available?)
- scientific article; zbMATH DE number 2085344 (Why is no real title available?)
- scientific article; zbMATH DE number 1414330 (Why is no real title available?)
- A complete uniform substitution calculus for differential dynamic logic
- A differential operator approach to equational differential invariants (invited paper)
- A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
- A method for invariant generation for polynomial continuous systems
- A new algorithm for finding rational first integrals of polynomial vector fields
- Abstractions for hybrid systems
- An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Barrier certificates revisited
- Bellerophon
- Bellerophon: tactical theorem proving for hybrid systems
- Computing closed form solutions of first order ODEs using the Prelle- Singer procedure
- Computing differential invariants of hybrid systems as fixed points
- Conic abstractions for hybrid systems
- Constraint-Based Approach for Analysis of Hybrid Systems
- Constructing invariants for hybrid systems
- Construction of parametric barrier functions for dynamical systems using interval analysis
- Differential dynamic logic for hybrid systems
- Differential equation invariance axiomatization
- Elementary First Integrals of Differential Equations
- Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
- Extracting and representing qualitative behaviors of complex systems in phase space
- Fast LCF-Style Proof Reconstruction for Z3
- First integrals of autonomous systems of differential equations and the Prelle-Singer procedure
- Generating Box Invariants
- Generating invariants for non-linear hybrid systems
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Ideals, Varieties, and Algorithms
- Integrability and nonintegrability of dynamical systems
- Integrability of dynamical systems: algebra and analysis
- Integrating a SAT solver with an LCF-style theorem prover
- Invariant algebraic surfaces of the Lorenz system
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Logics of dynamical systems
- ModelPlex
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Nonlinear dynamical systems and control. A Lyapunov-based approach
- Nonlinear systems
- On the nonexistence of rational first integrals for nonlinear systems and semiquasihomogeneous systems
- Ordinary differential equations with applications
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- Reachability Analysis for Solvable Dynamical Systems
- Real World Verification
- Safety verification of nonlinear hybrid systems based on invariant clusters
- Simulation-guided Lyapunov analysis for hybrid dynamical systems
- Stability theory by Liapunov's direct method
- Symbolic reachability computation for families of linear vector fields
- The Complete Proof Theory of Hybrid Systems
- Validating numerical semidefinite programming solvers for polynomial invariants
- Vector Lyapunov Functions
- Vector barrier certificates and comparison systems
- Verification and synthesis using real quantifier elimination
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- \(n-1\) independent first integrals for linear differential systems in \(\mathbb{R}^n\) or \(\mathbb{C}^n\)
Describes a project that uses
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)
