Combining deduction and algebraic constraints for hybrid system analysis.

@INPROCEEDINGS{DBLP:conf/verify/Platzer07,
	slides = {pub/cdachsa-slides.pdf},

  author    = {Andr{\'e} 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.}
}```