HyTech

HyTech

Description: HyTech (The Hybrid TECHnology Tool) 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.

VO Integration: No

Active: No

Available Benchmarks: No

Website: https://embedded.eecs.berkeley.edu/research/hytech/

Download: Links can be found on the main webpage.

Documentation: N/A

Contact: Tom Henzinger

Excerpt from: https://embedded.eecs.berkeley.edu/research/hytech/