Cited in
(only showing first 100 items - show all)- A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Uniform substitution for differential game logic
- Quantales
- Transformer semantics
- 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
- Generalized property-directed reachability for hybrid systems
- Numerically-aided deductive safety proof for a powertrain control system
- ParaPlan
- Theorem-proving analysis of digital control logic interacting with continuous dynamics
- 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
- Bellerophon: tactical theorem proving for hybrid systems
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Constructive hybrid games
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Sapo: reachability computation and parameter synthesis of polynomial dynamical systems
- Reachability computation for polynomial dynamical systems
- Differential game logic
- Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- An axiomatic approach to existence and liveness for differential equations
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Implicit definitions with differential equations for KeYmaera X (system description)
- Skill-based verification of cyber-physical systems
- 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
- Relational differential dynamic logic
- Using machine learning to improve cylindrical algebraic decomposition
- Change and delay contracts for hybrid system component verification
- Rigorous simulation-based analysis of linear hybrid systems
- Playing Hybrid Games with KeYmaera
- Fixing Zeno gaps
- Deadness and how to disprove liveness in hybrid dynamical systems
- 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
- A heuristic prover for real inequalities
- Real World Verification
- 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
- Aligator
- GSPeeDI
- KeY-C
- MetiTarski
- 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
- Averist
- C2e2
- dReach
- Flow*
- HyComp
- LySHA
- SL2SX
- SPHIN
- Breach
- Stabhyli
- ABsolver
- CTIGAR
- SystemModeler
- Bellerophon
- Sapo
This page was built for software: KeYmaera
