Differential Dynamic Logic

Title:	Differential Dynamic Logic
Author:	Brandon Bohrer (bbohrer /at/ cs /dot/ cmu /dot/ edu)
Submission date:	2017-02-13
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: Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer: Formally verified differential dynamic logic. CPP 2017.
BibTeX:	@article{Differential_Dynamic_Logic-AFP, author = {Brandon Bohrer}, title = {Differential Dynamic Logic}, journal = {Archive of Formal Proofs}, month = feb, year = 2017, note = {\url{http://isa-afp.org/entries/Differential_Dynamic_Logic.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Ordinary_Differential_Equations
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.