ACM Transactions on Computational Logic

• Thomas A. Henzinger, Rupak Majumdar, and Jean-Francois Raskin. A classification of symbolic transition systems. ACM Transactions on Computational Logic 6:1-32, 2005.

ACM Transactions on Programming Languages and Systems

• Thomas A. Henzinger and Christoph M. Kirsch. The Embedded Machine: Predictable, portable real-time code. ACM Transactions on Programming Languages and Systems 29(6), 2007.

• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems 24:51-64, 2002.

• Rajeev Alur and Thomas A. Henzinger. Finitary fairness. ACM Transactions on Programming Languages and Systems 20:1171-1194, 1998.

BMC Systems Biology

• Marc A. Schaub, Thomas A. Henzinger, and Jasmin Fisher. Qualitative networks: A symbolic approach to analyze biological signaling networks. BMC Systems Biology 1:4, 2007.

Formal Methods in System Design

• Thomas A. Henzinger, Orna Kupferman, and Shaz Qadeer. From prehistoric to postmodern symbolic model checking. Formal Methods in System Design 23:303-327, 2003.

• Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design 18:97-116, 2001.

• Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods in System Design 15:7-48, 1999.

• Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. Computing accumulated delays in real-time systems. Formal Methods in System Design 11:137-156, 1997.

IEEE Computer

• Thomas A. Henzinger and Joseph Sifakis. The discipline of embedded systems design. IEEE Computer 40(10):36-44, 2007.

IEEE Control Systems Magazine

• Thomas A. Henzinger, Christoph M. Kirsch, Marco A.A. Sanvido, and Wolfgang Pree. From control models to real-time code using Giotto. IEEE Control Systems Magazine 23(1):50-64, 2003.

IEEE Transactions on Automatic Control

• Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43:540-554, 1998.

IEEE Transactions on Software Engineering

• Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22:181-201, 1996.

Information and Computation

• Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, and Jens Palsberg. Stack size analysis for interrupt-driven programs. Information and Computation 194:144-174, 2004.

• Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. Information and Computation 173:64-81, 2002.

• Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Temporal proof methodologies for timed transition systems. Information and Computation 112:273-337, 1994.

• Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation 111:193-244, 1994.

• Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation 104:35-77, 1993.

Information Processing Letters

• Krishnendu Chatterjee and Thomas A. Henzinger. Reduction of stochastic parity to stochastic mean-payoff games. Information Processing Letters 106:1-7, 2008.

• Thomas A. Henzinger. Sooner is safer than later. Information Processing Letters 43:135-141, 1992.

International Journal of Foundations of Computer Science

• Laurent Doyen, Thomas A. Henzinger, and Jean-Francois Raskin. Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science 19:549-563, 2008.

International Journal of Game Theory

• Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger. Stochastic limit-average games are in EXPTIME. International Journal of Game Theory 37:219-234, 2008.

Journal of the ACM

• Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM 49:672-713, 2002.

• Rajeev Alur, Tomas Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM 43:116-146, 1996.

• Rajeev Alur and Thomas A. Henzinger. A really temporal logic. Journal of the ACM 41:181-204, 1994.

Journal of Computer and System Sciences

• Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic omega-regular games. Journal of Computer and System Sciences, to appear.

• Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata? Journal of Computer and System Sciences 57:94-124, 1998.

Logical Methods in Computer Science

• Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-Francois Raskin. Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(3), 2007.

Nature Biotechnology

• Jasmin Fisher and Thomas A. Henzinger. Executable cell biology. Nature Biotechnology 25:1239-1249, 2007.

Philosophical Transactions of the Royal Society

• Thomas A. Henzinger. Two challenges in embedded systems design: Predictability and robustness. Philosophical Transactions of the Royal Society A 366:3727-3736, 2008.

PLoS Computational Biology

• Jasmin Fisher, Nir Piterman, Alex Hajnal, and Thomas A. Henzinger. Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Computational Biology 3(5):e92, 2007.

Proceedings of the IEEE

• Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE 91:84-99, 2003.

• Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE 88:971-984, 2000.

Software Tools for Technology Transfer

• Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker Blast: Applications to software engineering. Software Tools for Technology Transfer 9:505-526, 2007.

• Rajeev Alur and Thomas A. Henzinger. Real-time system = discrete system + clock variables. Software Tools for Technology Transfer 1:86-109, 1997.

• Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer 1:110-122, 1997.

Theoretical Computer Science

• Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. Theoretical Computer Science 386:188-217, 2007.

• Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Games with secure equilibria. Theoretical Computer Science 365:67-82, 2006.

• Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science 354:173-186, 2006.

• Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Marielle Stoelinga. Model checking discounted temporal properties. Theoretical Computer Science 345:139-170, 2005.

• Jean-Francois Raskin, Pierre-Yves Schobbens, and Thomas A. Henzinger. Axioms for real-time logics. Theoretical Computer Science 274:151-182, 2002.

• Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theoretical Computer Science 211:253-273, 1999.

• Thomas A. Henzinger and Peter W. Kopke. Discrete-time control for rectangular hybrid automata. Theoretical Computer Science 221:369-392, 1999.

• Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science 138:3-34, 1995.