Differential dynamic logic for verifying parametric hybrid systems.

@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{\'e} 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.}
}```