A Theory of Synchronous Relational Interfaces (EECS-2010-45)
Stavros Tripakis, Ben Lickly, Thomas A. Henzinger and Edward A. Lee

On Relational Interfaces (EECS-2009-60)
Stavros Tripakis, Ben Lickly, Thomas A. Henzinger and Edward A. Lee

Trading Infinite Memory for Uniform Randomness in Timed Games (EECS-2008-4)
Krishnendu Chatterjee, Thomas A. Henzinger and Vinayak Prabhu

Finitary Winning in \omega-Regular Games (EECS-2007-120)
Krishnendu Chatterjee, Thomas A. Henzinger and Florian Horn

Strategy Logic (EECS-2007-78)
Krishnendu Chatterjee, Thomas A. Henzinger and Nir Piterman

Minimum-Time Reachability in Timed Games (EECS-2007-47)
Thomas Brihaye, Thomas A. Henzinger, Vinayak Prabhu and Jean-Francois Raskin

Generalized Parity Games (EECS-2006-144)
Krishnendu Chatterjee, Thomas A. Henzinger and Nir Piterman

Stochastic Limit-Average Games are in EXPTIME (EECS-2006-143)
Krishnendu Chatterjee, Rupak Majumdar and Thomas A. Henzinger

Reduction of Stochastic Parity to Stochastic Mean-payoff Games (EECS-2006-140)
Krishnendu Chatterjee and Thomas A. Henzinger

Memoryless Strategies in Concurrent Games with Reachability Objectives (CSD-05-1406)
Krishnendu Chatterjee, Luca de Alfaro and Thomas A. Henzinger

Stochastic Limit-Average Games are in EXPTIME (CSD-05-1405)
Krishnendu Chatterjee, Rupak Majumdar and Thomas A. Henzinger

Algorithms for Stochastic Parity Games (CSD-05-1391)
Krishnendu Chatterjee and Thomas A. Henzinger

Distributed Schedule Carrying Code (CSD-04-1360)
Thomas A. Henzinger, Christoph M. Kirsch and Slobodan Matic

The Complexity of Stochastic Rabin and Streett Games (CSD-04-1355)
Krishnendu Chatterjee, Luca de Alfaro and Thomas A. Henzinger

The Complexity of Quantitative Concurrent Parity Games (CSD-04-1354)
Krishnendu Chatterjee, Luca de Alfaro and Thomas A. Henzinger

A Preliminary Report on the Embedded Virtual Machine (CSD-04-1322)
Arkadeb Ghosal, Marco A. A. Sanvido and Thomas A. Henzinger

Quantitative Stochastic Parity Games (CSD-03-1280)
Krishnendu Chatterjee, Marcin Jurdzinski and Thomas A. Henzinger

xGiotto Language Report (CSD-03-1261)
Marco A. A. Sanvido, Arkadeb Ghosal and Thomas A. Henzinger

A Programmable Microkernal for Real-Time Systems (CSD-03-1250)
Christoph M. Kirsch, Thomas A. Henzinger and Marco A. A. Sanvido

Schedule-Carrying Code (CSD-03-1230)
Thomas A. Henzinger, Christoph M. Kirsch and Slobodan Matic

Counterexample Guided Control (CSD-02-1213)
Thomas A. Henzinger, Ranjit Jhala and Rupak Majumdar

Giotto: a Time-triggered Language for Embedded Programming (CSD-00-1121)
Thomas A. Henzinger, Benjamin Horowitz and Christoph Meyer Kirsch

A Classification of Symbolic Transition Systems (CSD-99-1086)
Thomas A. Henzinger and Rupak Majumdar

Axioms for Real-Time Logics (CSD-99-1076)
Pierre-Yves Schobbens, Jean-Francois Raskin, Thomas A. Henzinger and L. Ferier

Temporal Logics, Automata, and Classical Theories for Defining Real-Time Languages (CSD-99-1074)
Thomas A. Henzinger, Jean-Francois Raskin and Pierre-Yves Schobbens

Robust Undecidability of Timed and Hybrid Systems (CSD-99-1073)
Thomas A. Henzinger and Jean-Francois Raskin

Rectangular Hybrid Games (Extended Abstract) (CSD-99-1044)
Thomas A. Henzinger, Benjamin Horowitz and Rupak Majumdar

From Pre-Historic to Post-Modern Symbolic Model Checking (M99/56)
Thomas A. Henzinger, O. Kupferman and S. Qadeer

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems (M99/55)
Thomas A. Henzinger, S. Qadeer and S.K. Rajamani

Formal Specification and Verification of a Dataflow Processor Array (M99/14)
Thomas A. Henzinger, X. Liu, S. Qadeer and S.K. Rajamani

An Assume-Guaranteee Rule for Checking Simulation for Multipoint Moment Matching of Multiport Distributed Interconnect Networks (M99/13)
Thomas A. Henzinger, S. Qadeer, S.K. Rajamani, S. Tasiran, J.M.L. Wang and Ernest S. Kuh

An Algorithm for the Approximative Analysis of Rectangular Automata (M99/12)
J. Preubig, S. Kowalewski, H. Wong-Toi and Thomas A. Henzinger

Reactive Modules (M98/41)
R. Alur and Thomas A. Henzinger

It's About Time: Real-Time Logics Reviewed (M98/40)
Thomas A. Henzinger

Concurrent Reachability Games (M98/33)
L. de Alfaro, Thomas A. Henzinger and O. Kupferman

Symbolic Analysis of Hybrid Systems (M98/23)
R. Alur, Thomas A. Henzinger and H. Wong-Toi

What's Decidable About Hybrid Automata (M98/22)
Thomas A. Henzinger, P.W. Kopke, A. Puri and Pravin Varaiya

Symbolic Exploration of Transition Hierarchies (M98/21)
R. Alur, Thomas A. Henzinger and S.K. Rajamani

Alternating-Time Temporal Logic (M98/20)
R. Alur, Thomas A. Henzinger and O. Kupferman

Reachability Verification for Hybrid Automata (M98/19)
Thomas A. Henzinger and V. Rusu

Finitary Fairness (M98/18)
R. Alur and Thomas A. Henzinger

HYTECH: A Model Checker for Hybrid Systems (M97/79)
Thomas A. Henzinger, P-H. Ho and H. Wong-Toi

Real-Time System = Discrete System + Clock Variables (M97/78)
R. Alur and Thomas A. Henzinger

Partial-Order Reduction in Symbolic State Space Exploration (M97/30)
R. Alur, Robert K. Brayton, Thomas A. Henzinger, S. Qadeer and S.K. Rajamani

Discrete-Time Control for Rectangular Hybrid Automata (M97/29)
Thomas A. Henzinger and Peter W. Kopke

Event-Clock Automata: A Determinizable Class of Timed Automata (M97/28)
R. Alur, L. Fix and Thomas A. Henzinger

Computing Accumulated Delays in Real-Time Systems (M97/19)
R. Alur, C. Courcoubetis and Thomas A. Henzinger

Robust Timed Automata (M97/18)
V. Gupta, Thomas A. Henzinger and R. Jagadeesan

From Quantity to Quality (M97/17)
Thomas A. Henzinger and O. Kupferman

Using HyTech to Synthesize Control Parameters for a Steam Boiler (M96/61)
Thomas A. Henzinger and Howard Wong-Toi

Algorithmic Analysis of Nonlinear Hybrid Systems (M96/60)
Thomas A. Henzinger, P-H. Ho and H. Wong-Toi

The Theory of Hybrid Automata (M96/28)
Thomas A. Henzinger