We are pleased to announce that a new version of HyTech is now publicly available. 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, HyTech generates a diagnostic error trace.
HyTech is available by anonymous ftp and on the WWW:
Tom Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.