Ph.D. Stanford University, 1991
Electrical Engineering and Computer Sciences
University of California at Berkeley
Office hours: on leave
Mail: Berkeley, CA 94720-1770
Email: t a h @eecs.berkeley.edu
Phone: (510) 643-2430
Fax: (510) 642-2739
Assistant (Charlotte Jones): 510 643-2834
Curriculum vitae (PostScript, PDF)
Travel schedule
Weekly schedule
Finger information
A typed assembly language for real-time programs (EMSOFT 2004)
The Blast query language for software verification (SAS 2004)
Games with secure equilibria (LICS 2004)
Race checking by context inference (PLDI 2004)
An Eclipse plugin for model checking (IWPC 2004)
Generating tests from counterexamples (ICSE 2004)
Abstractions from proofs (POPL 2004)
Model checking discounted temporal properties (TACAS 2004)
Event-driven programming with logical execution times (HSCC 2004)
Quantitative stochastic parity games (SODA 2004)
Spring 2003: CS 294-1 / EE 219C (Model Checking)
Fall 2002: CS 170 (Efficient Algorithms and Intractable Problems)
Spring 2001: CS 294-8 (Formal Techniques for Software Reliability)
Spring 2001: EECS 20 (Structure and Interpretation of Signals and Systems)
Spring 2000: EECS 291E (Hybrid Systems)
Modern systems theory: logic, automata, concurrency, hierarchy (e.g., concurrent games)
Chic: A JBuilder plug-in for checking interface compatibility
Giotto: A time-triggered language for real-time programming
HyTech: A symbolic model checker for hybrid automata
Mocha: A formal-verification tool suite for reactive modules
- Games, Time, and Probabilities: Models and Algorithms for System Design and Analysis (Lausanne, Zurich 2003)
- The Symbolic Approach to Hybrid Systems (CAV '02)
- What is an Interface? (Microsoft 2001; Zurich 2002)
- From Models to Code: The Missing Link in Embedded Software (HSCC '02; Munich 2002)
- Design and Verification of Embedded Systems (Minnesota 2001)
- Decomposing Refinement Proofs using Assume-Guarantee Reasoning (ICCAD '00)
Selected courses:
- CS 294-8: Four Lectures on Model Checking (Berkeley 2001)
- EECS 20: Introduction to Modern Systems Theory (Berkeley 2001)
A more recent overview of our research activities (Berkeley 2002)
Archived lectures
- Model checking of software
- Embedded software design
- Interfaces for component-based design
- Games for verification and control
- Probabilistic and hybrid systems
Publications by venue: conferences; journals
Bibtex publication list
DBLP database
Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors. Hybrid Systems III: Verification and Control. Lecture Notes in Computer Science 1066, Springer-Verlag, 1996, 618 pages. ISBN 3-540-61155-X.
Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification: Proceedings of the 8th International Conference, CAV '96. Lecture Notes in Computer Science 1102, Springer-Verlag, 1996, 472 pages. ISBN 3-540-61474-5.
Thomas A. Henzinger and Shankar Sastry, editors. Hybrid Systems-Computation and Control: Proceedings of the First International Workshop, HSCC '98. Lecture Notes in Computer Science 1386, Springer-Verlag, 1998, 415 pages. ISBN 3-540-64358-3.
Thomas A. Henzinger and Christoph M. Kirsch, editors. Embedded Software: Proceedings of the First International Workshop, EMSOFT '01. Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, 504 pages. ISBN 3-540-42673-6.
Founding committee, Hybrid Systems-Computation and Control (HSCC)
Program committee,
Application of Concurrency to System Design
(ACSD), 2004
Program committee,
Hybrid Systems-Computation and Control
(HSCC), 2004
Program committee,
Automata, Languages, and Programming
(ICALP), 2004
Editorial board, Formal Methods in System Design (Kluwer)
Editorial board, Software Tools for Technology Transfer (Springer)
Editorial board, Theoretical Computer Science (Elsevier)
Center for Information Technology Research in the Interest of Society (CITRIS)
Gigascale Silicon Research Center (GSRC)
Model-Based Integration of Embedded Systems
Open Source Quality
Real-Time Fault-Tolerant Network Protocols
Software-Enabled Control
Krishnendu Chatterjee
Arkadeb Ghosal
Ranjit Jhala
Slobodan Matic
Vinayak Prabhu
Peter W. Kopke (Ph.D. Cornell, 1996): The Theory of Rectangular Hybrid Automata
Shaz Qadeer (Ph.D. Berkeley, 1999): Methodology for Scalable Model Checking
Sriram K. Rajamani (Ph.D. Berkeley, 1999): New Directions in Refinement Checking
Freddy Mang (Ph.D. Berkeley, 2002): Games in Open Systems Verification and Synthesis
Benjamin Horowitz (Ph.D. Berkeley, 2003): Giotto: A Time-triggered Language for Embedded Programming
Rupak Majumdar (Ph.D. Berkeley, 2003): Symbolic Algorithms for Verification and Control
Marco Sanvido
Marcin Jurdzinski
Christoph M. Kirsch
Sriram Krishnan
Orna Kupferman
Marius Minea
Jean-Francois Raskin
Gregoire Sutre
Howard Wong-Toi
Defense Advanced Research Projects Agency (DARPA)
Microelectronics Advanced Research Corporation (MARCO)
National Aeronautics and Space Administration (NASA)
National Science Foundation (NSF)
Office of Naval Research (ONR)
Semiconductor Research Corporation (SRC)
University of California MICRO Program
Wind River Systems