Pegasus: a framework for sound continuous invariant generation
From MaRDI portal
Publication:6535946
Recommendations
- Pegasus: sound continuous invariant generation
- 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
- Deductive verification of continuous dynamical systems
Cites work
- 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 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?)
- 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
- Abstractions for hybrid systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Barrier certificates revisited
- 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
- Constraint-Based Approach for Analysis of Hybrid Systems
- Constructing invariants for hybrid systems
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Differential dynamic logic for hybrid systems
- Differential equation axiomatization. The impressive power of differential ghosts
- 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
- 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
- Integrating a SAT solver with an LCF-style theorem prover
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré.
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- Reachability Analysis for Solvable Dynamical Systems
- Real World Verification
- Recherches sur la théorie de la démonstration.
- 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 barrier certificates and comparison systems
- Verification and synthesis using real quantifier elimination
This page was built for publication: Pegasus: a framework for sound continuous invariant generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535946)
