Thomas A. Henzinger
Assistant Professor
PhD Stanford University, 1991


We are interested in the formal foundations of sequential, concurrent, and real-time computation. 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)automatic tools for testing system prototypes against formal requirement specifications. We have 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

Awards

Lectures

Publications


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

If you have questions or comments please contact: www@cs.cornell.edu.


Last modified: 26 November 1995 by Denise Moore (denise@cs.cornell.edu).