Implicit definitions with differential equations for KeYmaera X (system description)

DOI10.1007/978-3-031-10769-6_42MaRDI QIDQ2104559OpenAlexFDO

Authors James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer

Publication date 7 December 2022

Full work available at URL https://arxiv.org/abs/2203.01272

zbMATH Keywords

theorem provingdifferential dynamic logicdefinitionsverification of hybrid systems

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A complete uniform substitution calculus for differential dynamic logic
• An axiomatic approach to existence and liveness for differential equations
• Differential dynamic logic for hybrid systems
• Differential equation invariance axiomatization
• Formalization of real analysis: a survey of proof assistants and libraries
• Hybrid Systems: Computation and Control
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Logical foundations of cyber-physical systems
• MetiTarski: An automatic theorem prover for real-valued special functions
• Nonlinear systems
• Some undecidable problems involving elementary functions of a real variable
• Stateless HOL
• The Complete Proof Theory of Hybrid Systems
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• dReal: an SMT solver for nonlinear theories over the reals

Cited in

(3)

• IsaVODEs: Interactive verification of cyber-physical systems at scale
• KeYmaera X
• Verifying Switched System Stability With Logic

Describes a project that uses

Uses Software

• MetiTarski
• KeYmaera
• RSOLVER
• Benchmarks
• Zenon
• dReal
• HSolver

This page was built for publication: Implicit definitions with differential equations for KeYmaera X (system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104559)