Thomas A. Henzinger
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
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.
- NSF Career Development Award
- ONR Young Investigator Award
- Member: Field of Applied Mathematics; Field of Cognitive Studies
- 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
- Journal Referee: Formal Aspects of Computing; IEEE
Transactions on Computers; Information and Computation
- Conference Referee: 25th International Conference on Parallel
- 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
- Consultant: AT&T Bell Laboratories; GrammaTech
- 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
- 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.
- 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
- 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
- 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).
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