---
_id: '4475'
abstract:
- lang: eng
  text: We provide an overview of the current status of HYTECH, and reflect on some
    of the lessons learned from our experiences with the tool. HYTECH is a symbolic
    model checker for mixed discrete-continuous systems that are modeled as automata
    with piecewise-constant polyhedral differential inclusions. The use of a formal
    input language and automated procedures for state-space traversal lay the foundation
    for formally verifying properties of hybrid dynamical systems. We describe some
    recent experiences analyzing three hybrid systems. We point out the successes
    and limitations of the tool. The analysis procedure has been extended in a number
    of ways to address some of the tool's shortcomings. We evaluate these extensions,
    and conclude with some desiderata for verification tools for hybrid systems.
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: Joerg
  full_name: Preussig, Joerg
  last_name: Preussig
- first_name: Howard
  full_name: Wong Toi, Howard
  last_name: Wong Toi
citation:
  ama: 'Henzinger TA, Preussig J, Wong Toi H. Some lessons from the HYTECH experience.
    In: <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>. Vol
    3. IEEE; 2001:2887-2892. doi:<a href="https://doi.org/10.1109/.2001.980714">10.1109/.2001.980714</a>'
  apa: 'Henzinger, T. A., Preussig, J., &#38; Wong Toi, H. (2001). Some lessons from
    the HYTECH experience. In <i>Proceedings of the 40th IEEE Conference on Decision
    and Control</i> (Vol. 3, pp. 2887–2892). Orlando, FL, USA: IEEE. <a href="https://doi.org/10.1109/.2001.980714">https://doi.org/10.1109/.2001.980714</a>'
  chicago: Henzinger, Thomas A, Joerg Preussig, and Howard Wong Toi. “Some Lessons
    from the HYTECH Experience.” In <i>Proceedings of the 40th IEEE Conference on
    Decision and Control</i>, 3:2887–92. IEEE, 2001. <a href="https://doi.org/10.1109/.2001.980714">https://doi.org/10.1109/.2001.980714</a>.
  ieee: T. A. Henzinger, J. Preussig, and H. Wong Toi, “Some lessons from the HYTECH
    experience,” in <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>,
    Orlando, FL, USA, 2001, vol. 3, pp. 2887–2892.
  ista: 'Henzinger TA, Preussig J, Wong Toi H. 2001. Some lessons from the HYTECH
    experience. Proceedings of the 40th IEEE Conference on Decision and Control. CDC:
    Decision and Control vol. 3, 2887–2892.'
  mla: Henzinger, Thomas A., et al. “Some Lessons from the HYTECH Experience.” <i>Proceedings
    of the 40th IEEE Conference on Decision and Control</i>, vol. 3, IEEE, 2001, pp.
    2887–92, doi:<a href="https://doi.org/10.1109/.2001.980714">10.1109/.2001.980714</a>.
  short: T.A. Henzinger, J. Preussig, H. Wong Toi, in:, Proceedings of the 40th IEEE
    Conference on Decision and Control, IEEE, 2001, pp. 2887–2892.
conference:
  end_date: 2001-12-07
  location: Orlando, FL, USA
  name: 'CDC: Decision and Control'
  start_date: 2001-12-04
date_created: 2018-12-11T12:09:02Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-10T09:47:20Z
day: '01'
doi: 10.1109/.2001.980714
extern: '1'
intvolume: '         3'
language:
- iso: eng
month: '05'
oa_version: None
page: 2887 - 2892
publication: Proceedings of the 40th IEEE Conference on Decision and Control
publication_identifier:
  isbn:
  - '0780370619'
publication_status: published
publisher: IEEE
publist_id: '253'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Some lessons from the HYTECH experience
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 3
year: '2001'
...