Pages that link to "Item:Q3454120"
From MaRDI portal
The following pages link to KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (Q3454120):
Displaying 28 items.
- ModelPlex: verified runtime validation of verified cyber-physical system models (Q681465) (← links)
- Implicit semi-algebraic abstraction for polynomial dynamical systems (Q832202) (← links)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- A complete uniform substitution calculus for differential dynamic logic (Q1707599) (← links)
- An axiomatic approach to existence and liveness for differential equations (Q1982634) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- Implicit definitions with differential equations for KeYmaera X (system description) (Q2104559) (← links)
- A mechanically verified theory of contracts (Q2119969) (← links)
- Pegasus: sound continuous invariant generation (Q2147687) (← links)
- Deductive stability proofs for ordinary differential equations (Q2233505) (← links)
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic (Q2305408) (← links)
- Uniform substitution at one Fell swoop (Q2305431) (← links)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (Q2331077) (← links)
- Numerically-aided deductive safety proof for a powertrain control system (Q2520674) (← links)
- The refinement calculus of reactive systems (Q2672236) (← links)
- Verification of Hybrid Systems (Q3176388) (← links)
- Rigorous Simulation-Based Analysis of Linear Hybrid Systems (Q3303914) (← links)
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (Q3541700) (← links)
- Skill-Based Verification of Cyber-Physical Systems (Q5039533) (← links)
- Reusable contracts for safe integration of reinforcement learning in hybrid systems (Q6103163) (← links)
- On proving that an unsafe controller is not proven safe (Q6151623) (← links)
- Verified Quadratic Virtual Substitution for Real Arithmetic (Q6488467) (← links)
- Integrating ADTs in KeY and Their Application to History-Based Reasoning (Q6488468) (← links)
- Pegasus: a framework for sound continuous invariant generation (Q6535946) (← links)
- Parallel composition and modular verification of computer controlled systems in differential dynamic logic (Q6535960) (← links)
- Constraint-driven nonlinear reachability analysis with automated tuning of tool properties (Q6643189) (← links)
- IsaVODEs: Interactive verification of cyber-physical systems at scale (Q6653093) (← links)
