KeYmaera
From MaRDI portal
swMATH3709MaRDI QIDQ16063FDOQ16063
Author name not available (Why is that?)
Official website: http://symbolaris.com/info/KeYmaera.html
Cited In (only showing first 100 items - show all)
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- 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)
- 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
- Computing differential invariants of hybrid systems as fixed points
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Verification of Hybrid Systems
- Aligator
- GSPeeDI
- KeY-C
- MetiTarski
- A mechanically verified theory of contracts
- QEPCAD
- SPeeDI
- HySAT
- Scicos
- MARCO
- HyTech
- PHAVer
- SMV
- RSOLVER
- Benchmarks
- ScicosLab
- Orbital library
- ClawZ
- Ariadne
- C-CoRN
- HSolver
- NLTOOLBOX
- AERN
- ATL
- KeY
- ProjectionCAD
- Milawa
- Ellipsoidal Toolbox
- pyHybrid Analysis
- SpaceEx
- Coquelicot
- BACH
- HybridSal
- PVSio-web
- Manip
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Averist
- C2e2
- dReach
- Flow*
- HyComp
- LySHA
- SL2SX
- SPHIN
- Breach
- Stabhyli
- ABsolver
- CTIGAR
- SystemModeler
- Bellerophon
- Sapo
- ModelPlex
- BranchCuts
- ASMKeY
- CORA
- HyPro
- JuliaReach
- Ordinary Differential Equations
- PEORL
- VeriPhy
- Algebraic_VCs
- Differential_Game_Logic
- Kleene Algebra
- KAD
- aaflib
- PyInterval
- HybridSystemsLab
- PRECiSA
- sitar
- KeYmaera X
- 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
- Generalized property-directed reachability for hybrid systems
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Bellerophon: tactical theorem proving for hybrid systems
- Sapo: reachability computation and parameter synthesis of polynomial dynamical systems
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Reachability computation for polynomial dynamical systems
- An axiomatic approach to existence and liveness for differential equations
- Skill-based verification of cyber-physical systems
- Quantales
- Transformer semantics
- 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
- Relational differential dynamic logic
This page was built for software: KeYmaera
