Thomas A. Henzinger
Assistant Professor
Ph.D. Stanford University, 1991

We are interested in the formal foundations of sequential, concurrent, and real-time com-putation. We use automata theory, logic, and algorithms to analyze and predict the behavior of software and hardware systems.

Recently, our research has focused on the development of formal methods for the analysis of embedded systems. A typical embedded system consists of a digital controller that interacts with an analog environment in real time. Since embedded systems often operate in life-critical situations, an adequate level of safety and reliability can be guaranteed only through the use of computer-aided analysis tools in the development process. Moving one step beyond computer-aided design and simulation, computer-aided verification attempts to provide the development engineer with (semi)auto-matic tools for testing system prototypes against formal requirement specifications. We developed the computer-aided verification tool HyTech, which automatically derives the timing conditions under which an embedded system meets its safety requirements.


University Activities

Professional Activities



Return to:
1995-1996 Annual Report Home Page
Departmental Home Page

If you have questions or comments please contact:

Last modified: 2 November 1996 by Denise Moore (