Pegasus: a framework for sound continuous invariant generation

DOI10.1007/978-3-030-30942-8_10zbMath1539.68364MaRDI QIDQ6535946

Yong Kiam Tan, Stefan Mitsch, Katherine Cordwell, Andrew Sogokon, André Platzer

Publication date: 14 March 2024

zbMATH Keywords

ordinary differential equationstheorem provinginvariant generationcontinuous invariants

Mathematics Subject Classification ID

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Barrier certificates revisited
• 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
• Computing differential invariants of hybrid systems as fixed points
• Differential dynamic logic for hybrid systems
• Stability theory by Liapunov's direct method
• Computing closed form solutions of first order ODEs using the Prelle- Singer procedure
• Extracting and representing qualitative behaviors of complex systems in phase space
• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré.
• Bellerophon: tactical theorem proving for hybrid systems
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Recherches sur la théorie de la démonstration.
• Vector barrier certificates and comparison systems
• A linear programming relaxation based approach for generating barrier certificates of hybrid systems
• Generating invariants for non-linear hybrid systems
• Abstractions for hybrid systems
• Constructing invariants for hybrid systems
• A Method for Invariant Generation for Polynomial Continuous Systems
• Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
• Automatic invariant generation for hybrid systems using ideal fixed points
• The Complete Proof Theory of Hybrid Systems
• Simulation-guided lyapunov analysis for hybrid dynamical systems
• Elementary First Integrals of Differential Equations
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Constraint-Based Approach for Analysis of Hybrid Systems
• Generating Box Invariants
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Reachability Analysis for Solvable Dynamical Systems
• Differential Equation Axiomatization
• Real World Verification
• Ideals, Varieties, and Algorithms
• Verification and synthesis using real quantifier elimination
• Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Fast LCF-Style Proof Reconstruction for Z3
• Validating numerical semidefinite programming solvers for polynomial invariants
• Symbolic reachability computation for families of linear vector fields

This page was built for publication: Pegasus: a framework for sound continuous invariant generation