Differential dynamic logics: Automated theorem proving for hybrid systems

Designing and analyzing hybrid systems, which are models for complex physical systems, is expensive and error-prone. The dissertation presented in this article introduces a verification logic that is suitable for analyzing the behavior of hybrid systems. It presents a proof calculus and a new deductive verification tool for hybrid systems that has been used successfully to verify aircraft and train control.

@ARTICLE{DBLP:journals/ki/Platzer10,

  author    = {Andr{\'e} Platzer},
  title     = {Differential Dynamic Logics:
               Automated Theorem Proving for Hybrid
               Systems},
  journal   = {K\"unstliche Intelligenz},
  year      = {2010},
  volume    = {24},
  number    = {1},
  doi       = {10.1007/s13218-010-0014-6},
  pages     = {75-77},
  issn      = {0933-1875},
  abstract  = {
    Designing and analyzing hybrid systems, which are
    models for complex physical systems, is expensive and
    error-prone. The dissertation presented in this article
    introduces a verification logic that is suitable for
    analyzing the behavior of hybrid systems. It presents a
    proof calculus and a new deductive verification tool
    for hybrid systems that has been used successfully to
    verify aircraft and train control.}
}```