KeYmaera
From MaRDI portal
Software:16063
swMATH3709MaRDI QIDQ16063FDOQ16063
Author name not available (Why is that?)
Cited In (52)
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- An axiomatic approach to existence and liveness for differential equations
- Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Implicit definitions with differential equations for KeYmaera X (system description)
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- The refinement calculus of reactive systems
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Using machine learning to improve cylindrical algebraic decomposition
- Playing Hybrid Games with KeYmaera
- Deadness and how to disprove liveness in hybrid dynamical systems
- Fixing Zeno gaps
- A complete uniform substitution calculus for differential dynamic logic
- Real World Verification
- A heuristic prover for real inequalities
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
- A Verified Theorem Prover Backend Supported by a Monotonic Library
- Generating invariants for non-linear hybrid systems
- Computing differential invariants of hybrid systems as fixed points
- Pegasus: sound continuous invariant generation
- Rigorous Simulation-Based Analysis of Linear Hybrid Systems
- Formal verification of braking while swerving in automobiles
- MetiTarski’s Menagerie of Cooperating Systems
- Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis
- Title not available (Why is that?)
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Verification of Hybrid Systems
- A mechanically verified theory of contracts
- A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- A Uniform Substitution Calculus for Differential Dynamic Logic
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Sapo
- Differential Game Logic
- Uniform substitution for differential game logic
- Skill-Based Verification of Cyber-Physical Systems
- Crossing the Bridge between Similar Games
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- A system for compositional verification of asynchronous objects
- Numerically-aided deductive safety proof for a powertrain control system
- Theorem-proving analysis of digital control logic interacting with continuous dynamics
- Generalized property-directed reachability for hybrid systems
- Change and Delay Contracts for Hybrid System Component Verification
- Programming with Infinitesimals: A While-Language for Hybrid System Modeling
- Uniform substitution at one Fell swoop
- Bellerophon: tactical theorem proving for hybrid systems
- Constructive hybrid games
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Reachability computation for polynomial dynamical systems
- Relational differential dynamic logic
This page was built for software: KeYmaera
