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é Platzer']},
	title = {Differential Dynamic Logics:
               Automated Theorem Proving for Hybrid
               Systems},
	journal = {Künstliche 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.}
}