---
_id: '4429'
abstract:
- lang: eng
  text: We study the reachability problem for hybrid automata. Automatic approaches,
    which attempt to construct the reachable region by symbolic execution, often do
    not terminate. In these cases, we require the user to guess the reachable region,
    and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata
    according to the theory in which their reachable region can be defined finitely.
    This is the theory in which the prover needs to operate in order to verify the
    guess. The approach is interesting, because an appropriate guess can often be
    deduced by extrapolating from the first few steps of symbolic execution.
acknowledgement: "This research was supported in part by the ONR YIP award N00014-95-1-0520,
  by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
  contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
  grant NAG2-892, and by the SRC contract 95-DC-324.036.\r\nSupported by Lavoisier
  grant of the French Foreign Affairs Ministry and by SRI."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Vlad
  full_name: Rusu, Vlad
  last_name: Rusu
citation:
  ama: 'Henzinger TA, Rusu V. Reachability verification for hybrid automata. In: <i>Proceedings
    of the 1st International Workshop on Hybrid Systems: Computation and Control</i>.
    Vol 1386. Springer; 1998:190-204. doi:<a href="https://doi.org/10.1007/3-540-64358-3_40">10.1007/3-540-64358-3_40</a>'
  apa: 'Henzinger, T. A., &#38; Rusu, V. (1998). Reachability verification for hybrid
    automata. In <i>Proceedings of the 1st International Workshop on Hybrid Systems:
    Computation and Control</i> (Vol. 1386, pp. 190–204). Berkely, CA, United States
    of America: Springer. <a href="https://doi.org/10.1007/3-540-64358-3_40">https://doi.org/10.1007/3-540-64358-3_40</a>'
  chicago: 'Henzinger, Thomas A, and Vlad Rusu. “Reachability Verification for Hybrid
    Automata.” In <i>Proceedings of the 1st International Workshop on Hybrid Systems:
    Computation and Control</i>, 1386:190–204. Springer, 1998. <a href="https://doi.org/10.1007/3-540-64358-3_40">https://doi.org/10.1007/3-540-64358-3_40</a>.'
  ieee: 'T. A. Henzinger and V. Rusu, “Reachability verification for hybrid automata,”
    in <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation
    and Control</i>, Berkely, CA, United States of America, 1998, vol. 1386, pp. 190–204.'
  ista: 'Henzinger TA, Rusu V. 1998. Reachability verification for hybrid automata.
    Proceedings of the 1st International Workshop on Hybrid Systems: Computation and
    Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1386, 190–204.'
  mla: 'Henzinger, Thomas A., and Vlad Rusu. “Reachability Verification for Hybrid
    Automata.” <i>Proceedings of the 1st International Workshop on Hybrid Systems:
    Computation and Control</i>, vol. 1386, Springer, 1998, pp. 190–204, doi:<a href="https://doi.org/10.1007/3-540-64358-3_40">10.1007/3-540-64358-3_40</a>.'
  short: 'T.A. Henzinger, V. Rusu, in:, Proceedings of the 1st International Workshop
    on Hybrid Systems: Computation and Control, Springer, 1998, pp. 190–204.'
conference:
  end_date: 1998-04-15
  location: Berkely, CA, United States of America
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 1998-04-13
date_created: 2018-12-11T12:08:48Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T11:29:14Z
day: '01'
doi: 10.1007/3-540-64358-3_40
extern: '1'
intvolume: '      1386'
language:
- iso: eng
month: '01'
oa_version: None
page: 190 - 204
publication: 'Proceedings of the 1st International Workshop on Hybrid Systems: Computation
  and Control'
publication_identifier:
  isbn:
  - '9783540643586'
publication_status: published
publisher: Springer
publist_id: '299'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachability verification for hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1386
year: '1998'
...