The following pages link to KeYmaera (Q16063):
Displaying 50 items.
- Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point (Q254170) (← links)
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (Q264193) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Reachability computation for polynomial dynamical systems (Q526433) (← links)
- Fixing Zeno gaps (Q549197) (← links)
- ModelPlex: verified runtime validation of verified cyber-physical system models (Q681465) (← links)
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Q779625) (← links)
- Generalized property-directed reachability for hybrid systems (Q784143) (← links)
- Implicit semi-algebraic abstraction for polynomial dynamical systems (Q832202) (← links)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- Computing differential invariants of hybrid systems as fixed points (Q1039853) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- A complete uniform substitution calculus for differential dynamic logic (Q1707599) (← links)
- Uniform substitution for differential game logic (Q1799081) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- An axiomatic approach to existence and liveness for differential equations (Q1982634) (← links)
- Using machine learning to improve cylindrical algebraic decomposition (Q2009221) (← links)
- Constructive hybrid games (Q2096468) (← links)
- Implicit definitions with differential equations for KeYmaera X (system description) (Q2104559) (← links)
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro} (Q2105429) (← links)
- A mechanically verified theory of contracts (Q2119969) (← links)
- Pegasus: sound continuous invariant generation (Q2147687) (← links)
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic (Q2305408) (← links)
- Uniform substitution at one Fell swoop (Q2305431) (← links)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (Q2331077) (← links)
- Generating invariants for non-linear hybrid systems (Q2355695) (← links)
- Numerically-aided deductive safety proof for a powertrain control system (Q2520674) (← links)
- Theorem-proving analysis of digital control logic interacting with continuous dynamics (Q2520681) (← links)
- Deadness and how to disprove liveness in hybrid dynamical systems (Q2629097) (← links)
- The refinement calculus of reactive systems (Q2672236) (← links)
- MetiTarski’s Menagerie of Cooperating Systems (Q2849476) (← links)
- Playing Hybrid Games with KeYmaera (Q2908514) (← links)
- Programming with Infinitesimals: A While-Language for Hybrid System Modeling (Q3012935) (← links)
- Crossing the Bridge between Similar Games (Q3172850) (← links)
- Verification of Hybrid Systems (Q3176388) (← links)
- Rigorous Simulation-Based Analysis of Linear Hybrid Systems (Q3303914) (← links)
- (Q3384178) (← links)
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs (Q3406693) (← links)
- A Uniform Substitution Calculus for Differential Dynamic Logic (Q3454116) (← links)
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (Q3454120) (← links)
- Computing Differential Invariants of Hybrid Systems as Fixedpoints (Q3512492) (← links)
- Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis (Q4899145) (← links)
- A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems (Q5026187) (← links)
- Skill-Based Verification of Cyber-Physical Systems (Q5039533) (← links)
- Formal verification of braking while swerving in automobiles (Q5146396) (← links)
- Real World Verification (Q5191121) (← links)
- Change and Delay Contracts for Hybrid System Component Verification (Q5215905) (← links)
- A Verified Theorem Prover Backend Supported by a Monotonic Library (Q5222980) (← links)
- Relational differential dynamic logic (Q5239265) (← links)
- Sapo (Q5275315) (← links)
