Abstract
We formalize differential dynamic logic, a logic for proving
properties of hybrid systems. The proof calculus in this formalization
is based on the uniform substitution principle. We show it is sound
with respect to our denotational semantics, which provides increased
confidence in the correctness of the KeYmaera X theorem prover based
on this calculus. As an application, we include a proof term checker
embedded in Isabelle/HOL with several example proofs. Published in:
Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André
Platzer: Formally verified differential dynamic logic. CPP 2017.
License
Topics
Session Differential_Dynamic_Logic
- Ids
- Lib
- Syntax
- Denotational_Semantics
- Axioms
- Frechet_Correctness
- Static_Semantics
- Coincidence
- Bound_Effect
- Differential_Axioms
- USubst
- USubst_Lemma
- Uniform_Renaming
- Pretty_Printer
- Proof_Checker
- Differential_Dynamic_Logic