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

• Computer Science Department Faculty Recruiting Committee
• Computer Science Department Colloquium Coordinator
• Cognitive Studies Undergraduate Advisory Committee
• Cognitive Studies Graduate Advisory Committee

Professional Activities

• 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 Theory, 1995
• 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 Science, 1995
• Other Referee: Army Research Office, National Science Foundation, Springer-Verlag Lecture Notes in Computer Science, Weizmann Institute of Science Doctoral Thesis

Awards

• ONR Young Investigator Award, 1995
• NSF Faculty Early Career Development Award (1995-1998)

Lectures

• 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, October 1994.

Publications

• 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 C. Courcoubetis).
• 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. Pnueli).
• 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: www@cs.cornell.edu.

---

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