Pegasus: a framework for sound continuous invariant generation
From MaRDI portal
Publication:6535946
DOI10.1007/978-3-030-30942-8_10zbMATH Open1539.68364MaRDI QIDQ6535946FDOQ6535946
Authors: Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer 
Publication date: 14 March 2024
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
Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by ordinary differential equations (93C15) 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
- Ideals, Varieties, and Algorithms
- Differential dynamic logic for hybrid systems
- Hybrid Systems: Computation and Control
- Stability theory by Liapunov's direct method
- Integrability and nonintegrability of dynamical systems
- Simulation-guided Lyapunov analysis for hybrid dynamical systems
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- Constructing invariants for hybrid systems
- 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?)
- Computing closed form solutions of first order ODEs using the Prelle- Singer procedure
- 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
- 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?)
- Recherches sur la théorie de la démonstration.
- 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 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
- Differential equation axiomatization. The impressive power of differential ghosts
- Generating Box Invariants
- Extracting and representing qualitative behaviors of complex systems in phase space
- Title not available (Why is that?)
- Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré.
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Validating numerical semidefinite programming solvers for polynomial invariants
- Safety verification of nonlinear hybrid systems based on invariant clusters
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)
