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)
- 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
- \(\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
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
- Generating invariants for non-linear hybrid systems
- Pegasus: sound continuous invariant generation
- Formal verification of braking while swerving in automobiles
- A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems
- MetiTarski's menagerie of cooperating systems
- Uniform substitution for differential game logic
- 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
- ParaPlan
- Programming with Infinitesimals: A While-Language for Hybrid System Modeling
- Uniform substitution at one Fell swoop
- ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems
- Differential game logic
- Constructive hybrid games
- 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
This page was built for software: KeYmaera
