@inproceedings{DBLP:conf/verify/Platzer07,
slides = {pub/cdachsa-slides.pdf},
author = {['André Platzer']},
title = {Combining Deduction and Algebraic
Constraints for Hybrid System Analysis.},
booktitle = {VERIFY'07 at CADE, Bremen, Germany},
longbooktitle = {4th International Verification Workshop
VERIFY'07, at CADE-21, Bremen, Germany, July
15-16, 2007},
year = {2007},
pages = {164-178},
editor = {['Bernhard Beckert']},
volume = {259},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
issn = {1613-0073},
pdf = {http://ceur-ws.org/Vol-259/paper14.pdf},
eprint = {https://ceur-ws.org/Vol-259/paper14.pdf},
keywords = {modular prover combination, analytic
tableaux, verification of hybrid systems,
dynamic logic},
abstract = {
We show how theorem proving and methods for handling
real algebraic constraints can be combined for hybrid
system verification. In particular, we highlight the
interaction of deductive and algebraic reasoning that
is used for handling the joint discrete and continuous
behaviour of hybrid systems. We illustrate proof tasks
that occur when verifying scenarios with cooperative
traffic agents. From the experience with these
examples, we analyse proof strategies for dealing with
the practical challenges for integrated algebraic and
deductive verification of hybrid systems, and we
propose an iterative background closure strategy.}
}