Thomas A. Henzinger
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.
- Computer Science Department Faculty Recruiting Committee
- Computer Science Department Colloquium Coordinator
- Cognitive Studies Undergraduate Advisory Committee
- Cognitive Studies Graduate Advisory Committee
- Consultant, AT&T Bell Laboratories
- Co-organizer and program co-chair: DIMACS Workshop on Verification
and Control of Hybrid Systems, 1995
- Program Committee: Tenth Annual IEEE Symposium on Logic in Computer
Science, 1995, Seventh International Conference on Computer-aided
Verification, 1995, Sixth International Conference on Concurrency
- Journal Referee: ACM Transactions on Programming Languages and Systems,
Design Automation for Embedded Systems, Formal Aspects of Computing,
IEEE Transactions on Software Engineering, Information and Computation
- Conference Referee: Fourth International Conference on Algebraic
Methodology and Software Technology, 1995, Third International
Conference on the Mathematics of Program Construction, 1995,
14th Annual ACM Symposium on Principles of Distributed Computing,
1995, 36th Annual IEEE Symposium on Foundations of Computer
- Other Referee: Army Research Office, National Science Foundation,
Springer-Verlag Lecture Notes in Computer Science, Weizmann
Institute of Science Doctoral Thesis
- ONR Young Investigator Award, 1995
- NSF Faculty Early Career Development Award (1995-1998)
- Algorithmic analysis of hybrid systems. Third SIAM Conference on
Control and Its Applications, St. Louis, Missouri, April 1995.
- Computer-aided verification of infinite-state systems. University
of California, Berkeley, California, March 1995.
- ___. Stanford University, Stanford, California, March 1995.
- Model-checking and abstract-interpretation strategies for hybrid systems.
Stanford University, Stanford, California, August 1994.
- ___. AFOSR Software and Systems Contractors/Grantees Workshop, Washington,
DC, September 1994.
- ___. Workshop on Hybrid Systems and Autonomous Control, Ithaca, New York,
- Symbolic model checking for real-time systems. Information and
Computation 111 (1994), 193-244 (with X. Nicollin, J. Sifakis,
and S. Yovine).
- Temporal proof methodologies for timed transition systems. Information
and Computation 112 (1994), 273-337 (with Z. Manna and A. Pnueli).
- The algorithmic analysis of hybrid systems. Theoretical Computer Science
138 (1995), 3-34 (with R. Alur, C. Courcoubetis, N. Halbwachs, P.-H.
Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine).
- Finitary fairness. Proceedings of the Ninth Annual Symposium on
Logic in Computer Science, IEEE Computer Society Press (1994),
52-61 (with R. Alur).
- The observational power of clocks. Proceedings of the Fifth International
Conference on Concurrency Theory, Lecture Notes in Computer
Science 836, Springer-Verlag (1994), 162-177 (with R. Alur and
- Real-time system = discrete system + clock variables. Theories and
Experiences for Real-time System Development (T. Rus, C. Rattray,
eds.), AMAST Series in Computing 2, World Scientific (1994), 1-29
(with R. Alur).
- Verification methods for the divergent runs of clock systems. Proceedings
of the Third International Symposium on Formal Techniques in
Real-time and Fault-tolerant Systems, Lecture Notes in Computer
Science 863, Springer-Verlag (1994), 351-372 (with P. Kopke).
- Proving safety properties of hybrid systems. Proceedings of the Third
International Symposium on Formal Techniques in Real-Time and
Fault-Tolerant Systems, Lecture Notes in Computer Science 863,
Springer-Verlag (1994), 431-454 (with A. Kapur, Z. Manna, and A.
- HyTech: the Cornell hybrid technology tool. Proceedings of the First
Workshop on Tools and Algorithms for the Construction and Analysis
of Systems, BRICS Notes Series NS-95-2, University of Aarhus (1995),
29-43 (with P.-H. Ho).
- What's decidable about hybrid automata? Proceedings of the 27th Annual
Symposium on the Theory of Computing, ACM Press (1995), 373-382
(with P. Kopke, A. Puri, and P. Varaiya).
1994-1995 Annual Report Home Page
Departmental Home Page
If you have questions or comments please contact:
Last modified: 26 November 1995 by Denise Moore