HyTech: The HYbrid TECHnology Tool

HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata with discrete and continuous components, and temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error trace. The standard reference to the HyTech algorithm is [1], and the standard reference to the HyTech tool, [2].

[1] R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering 22:181-201, 1996.
[2] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer 1:110-122, 1997.

The HyTech Team

HyTech was developed by Tom Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.

The HyTech Demo

The HyTech Papers

Introduction, and guide to the literature
The specification formalism of hybrid automata, and its theory
The verification algorithm of polyhedral model checking, and some verification examples
The original tool, and more verification examples
The current tool, and more verification examples
A Unix man page for HyTech (courtesy John A. Murdie, University of York)
Other related papers

The HyTech Files

User guide: a manual with instructions for installation and usage
License agreement: we ask you to submit this before you get the software
hytech.tar.gz: HyTech Version 1.04f source code (Gzip compressed tar file of 679 KB)
hytech.tgz: the same as above (for users of Windows, which has a problem with multiple file extensions)

We have compiled the same sources on Unix, Linux but also under Windows with Cygwin. If you need to use HyTech on another platform, you should be able to compile the sources yourself with little effort (works with gcc 2.9x).
Download binaries :

hytech-v1.04f-Linux_static: Statically compiled under Linux on a Pentium IV (x86)
hytech-v1.04f-win32_cygwin.zip: Windows version compiled under Cygwin (x86)
hytech-v1.04f-Solaris_static.gz: Statically compiled under Solaris (Sparc)

See the user guide for installation instructions.

Two HyTech Case Studies

For questions and comments send mail to hytech-@AT@-epfl.ch

Tom Henzinger: back to my home page
Last updated in April, 2006.