Thomas A. Henzinger

Thomas A. Henzinger
Assistant Professor
tah@cs.cornell.edu
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.

Awards

NSF Career Development Award
ONR Young Investigator Award

University Activities

Member: Field of Applied Mathematics; Field of Cognitive Studies

Professional Activities

Editor: Hybrid Systems III: Verification and Control. LNCS 1066, Springer-Verlag, January 1996.
Organizer and Program Chair: DIMACS Workshop on Verification and Control of Hybrid Systems, 1995; Eighth International Conference on Computer-Aided Verification, 1996 Program Committee Member: Seventh International Conference on Computer-Aided Verification, 1995; Sixth International Conference on Concurrency Theory, 1995; Seventh International Conference on Concurrency Theory, 1996; Fourth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996; Fourth International Hybrid Systems Workshop, 1996
Journal Referee: Formal Aspects of Computing; IEEE Transactions on Computers; Information and Computation
Conference Referee: 25th International Conference on Parallel Processing
Referee: ACM Distinguished Dissertation Award; Army Research Office; Israel Science Foundation; National Science Foundation; Netherlands Computer Science Research Foundation; Springer-Verlag Lecture Notes in Computer Science
Participant: ACM Workshop on Strategic Directions in Computing Research-Working Group on Concurrency and Working Group on Formal Methods
Consultant: AT&T Bell Laboratories; GrammaTech

Lectures

Reactive modules. Oxford Workshop on Automated Formal Methods, Oxford, UK, June 1996.
____. Stanford University, Stanford, CA, May 1996.
HyTech in control applications. DIMACS Workshop on Controllers for Manufacturing and Automation: Specification, Synthesis, and Verification Issues, New Brunswick, NJ, May 1996.
A brief history of real time. Computer Science Colloquium, University of California, Berkeley, CA, April 1996.
New looks at old concepts: Local liveness and finitary fairness. CAD Seminar, University of California, Berkeley, CA, March 1996.
Algorithmic analysis of real-time and hybrid systems. Industrial Liaison Program, University of California, Berkeley, CA, March 1996.
____. ARPA Formal Methods Principal Investigators Meeting, San Diego, CA, January 1996.
Computer-aided verification of infinite-state systems. AT&T-SUNY Specification and Verification Workshop, Stony Brook, NY, November 1995.
Hybrid systems research: Achievements, problems, and goals. DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, NJ, October 1995.
A reactive-module approach to formal design, verification, and synthesis. SRC Annual Contract Review, University of California, Berkeley, CA, October 1995.

Publications

Linear phase-portrait approximations for nonlinear hybrid automata. Hybrid Systems III: Verification and Control, LNCS 1066, Springer-Verlag 1996, 377-388 (with H. Wong-Toi).
Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22, 1996, 181-201 (with R. Alur and P.-H. Ho).
The benefits of relaxing punctuality. Journal of the ACM 43 (1996), 116-146 (with R. Alur and T. Feder).
Algorithmic analysis of nonlinear hybrid systems. Proceedings of the Seventh International Conference on Computer-Aided Verification, LNCS 939, Springer-Verlag 1995, 225-238 (with P.-H. Ho).
Local liveness for the compositional modeling of fair reactive systems. Proceedings of the Seventh International Conference on Computer-Aided Verification, LNCS 939, Springer-Verlag 1995, 166-179 (with R. Alur).
Hybrid automata with finite bisimulations. Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming, LNCS 944, Springer-Verlag 1995, 324-335.
The expressive power of clocks. Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming, LNCS 944, Springer-Verlag 1995, 417-428 (with P.W. Kopke and H. Wong-Toi).
Computing simulations on finite and infinite graphs. Proceedings of the 36th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press, 1995, 453-462 (with M.R. Henzinger and P.W. Kopke).
HyTech: The Cornell hybrid technology tool. Hybrid Systems II, LNCS 999, Springer-Verlag 1995, 265-294 (with P.-H. Ho).
A note on abstract-interpretation strategies for hybrid automata. Hybrid Systems II, LNCS 999, Springer-Verlag 1995, 252-264 (with P.-H. Ho).
HyTech: The next generation. Proceedings 16th Annual IEEE Real-time Systems Symposium, IEEE Computer Society Press, 1995, 56-65 (with P.-H. Ho and H. Wong-Toi).
A user guide to HyTech. Proceedings First Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, Springer-Verlag 1995, 41-71 (with P.-H. Ho and H. Wong-Toi).

Return to:

1995-1996 Annual Report Home Page
Departmental Home Page If you have questions or comments please contact: www@cs.cornell.edu. Last modified: 2 November 1996 by Denise Moore (denise@cs.cornell.edu).