@inproceedings{DBLP:conf/tableaux/Platzer07,
pdf = {pub/dL.pdf},
slides = {pub/dL-slides.pdf},
study = {info/KeYmaera.html#case-studies},
TR = {DBLP:conf/tableaux/Platzer07:TR},
author = {['André Platzer']},
title = {Differential Dynamic Logic for Verifying
Parametric Hybrid Systems.},
booktitle = {TABLEAUX},
longbooktitle = {Automated Reasoning with Analytic
Tableaux and Related Methods, 16th
International Conference, TABLEAUX 2007,
Aix en Provence, France, July 3-6, 2007,
Proceedings},
year = {2007},
pages = {216-232},
doi = {10.1007/978-3-540-73099-6_17},
editor = {['Nicola Olivetti']},
volume = {4548},
series = {LNCS},
publisher = {Springer},
isbn = {978-3-540-73098-9},
keywords = {dynamic logic, sequent calculus,
verification of parametric hybrid systems,
quantifier elimination},
abstract = {
We introduce a first-order dynamic logic for reasoning
about systems with discrete and continuous state
transitions, and we present a sequent calculus for this
logic. As a uniform model, our logic supports hybrid
programs with discrete and differential actions. For
handling real arithmetic during proofs, we lift
quantifier elimination to dynamic logic. To obtain a
modular combination, we use side deductions for
verifying interacting dynamics. With this, our logic
supports deductive verification of hybrid systems with
symbolic parameters and first-order definable flows.
Using our calculus, we prove a parametric inductive
safety constraint for speed supervision in a train
control system.}
}