KeYmaera

swMATH3709MaRDI QIDQ16063FDOQ16063

Author name not available (Why is that?)

Described by source

• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

Cited In (52)

• Relational differential dynamic logic
• 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)
• Skill-based verification of cyber-physical systems
• 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
• Change and delay contracts for hybrid system component verification
• Using machine learning to improve cylindrical algebraic decomposition
• Rigorous simulation-based analysis of linear hybrid systems
• Playing Hybrid Games with KeYmaera
• Deadness and how to disprove liveness in hybrid dynamical systems
• Fixing Zeno gaps
• A uniform substitution calculus for differential dynamic logic
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• 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
• Generating invariants for non-linear hybrid systems
• Computing differential invariants of hybrid systems as fixed points
• Pegasus: sound continuous invariant generation
• Formal verification of braking while swerving in automobiles
• 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
• MetiTarski's menagerie of cooperating systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Uniform substitution for differential game logic
• 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
• A verified theorem prover backend supported by a monotonic library
• 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
• Programming with Infinitesimals: A While-Language for Hybrid System Modeling
• Uniform substitution at one Fell swoop
• Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
• ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems
• Bellerophon: tactical theorem proving for hybrid systems
• Sapo: reachability computation and parameter synthesis of polynomial dynamical systems
• Differential game logic
• Constructive hybrid games
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Reachability computation for polynomial dynamical systems

This page was built for software: KeYmaera