KeYmaera
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Computing differential invariants of hybrid systems as fixed points
- Aligator
- GSPeeDI
- KeY-C
- MetiTarski
- QEPCAD
- ParaPlan
- SPeeDI
- Scicos
- HySAT
- MARCO
- PHAVer
- HyTech
- SMV
- RSOLVER
- Benchmarks
- Bellerophon: tactical theorem proving for hybrid systems
- A complete uniform substitution calculus for differential dynamic logic
- ScicosLab
- Orbital library
- Uniform substitution for differential game logic
- ClawZ
- Ariadne
- C-CoRN
- HSolver
- A system for compositional verification of asynchronous objects
- An axiomatic approach to existence and liveness for differential equations
- Using machine learning to improve cylindrical algebraic decomposition
- Constructive hybrid games
- Implicit definitions with differential equations for KeYmaera X (system description)
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- A mechanically verified theory of contracts
- NLTOOLBOX
- AERN
- Pegasus: sound continuous invariant generation
- ProjectionCAD
- KeY
- Milawa
- ATL
- Ellipsoidal Toolbox
- SpaceEx
- pyHybrid Analysis
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Uniform substitution at one Fell swoop
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Coquelicot
- Generating invariants for non-linear hybrid systems
- HybridSal
- BACH
- PVSio-web
- Manip
- Numerically-aided deductive safety proof for a powertrain control system
- Theorem-proving analysis of digital control logic interacting with continuous dynamics
- Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point
- Deadness and how to disprove liveness in hybrid dynamical systems
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- The refinement calculus of reactive systems
- MetiTarski's menagerie of cooperating systems
- A heuristic prover for real inequalities
- Playing Hybrid Games with KeYmaera
- Programming with Infinitesimals: A While-Language for Hybrid System Modeling
- SPHIN
- Crossing the Bridge between Similar Games
- Verification of Hybrid Systems
- Stabhyli
- Averist
- C2e2
- LySHA
- SL2SX
- Flow*
- HyComp
- dReach
- Breach
- Rigorous simulation-based analysis of linear hybrid systems
- ABsolver
- ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- SystemModeler
- A uniform substitution calculus for differential dynamic logic
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- CTIGAR
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Sapo
- Bellerophon
- ModelPlex
- BranchCuts
- ASMKeY
- CORA
- JuliaReach
- HyPro
- Ordinary Differential Equations
- PEORL
- VeriPhy
- Kleene Algebra
- Algebraic_VCs
- KAD
- Differential_Game_Logic
- aaflib
- PyInterval
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
This page was built for software: KeYmaera
