Faculty Publications - Thomas A. Henzinger

Books

• T. A. Henzinger and C. M. Kirsch, Embedded Software: First International Workshop, Lecture Notes in Computer Science; 2211, Berlin; New York: Springer Verlag, 2001. [abstract]
• T. A. Henzinger and S. S. Sastry, Eds., Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, v. 1386, Vol. 1386, Berlin, Germany: Springer-Verlag, 1998. [abstract]
• R. Alur, T. A. Henzinger, and E. D. Sontag, Eds., Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science; No. 1066, Berlin; New York: Springer, 1996.

Book chapters or sections

• K. Chatterjee, K. Sen, and T. A. Henzinger, "Model-checking $omega$-regular properties of interval Markov chains," in Foundations of Software Science and Computational Structures (FoSSaCS 2008): Proc. 11th Intl. Conf., R. M. Amadio, Ed., Lecture Notes in Computer Science, Vol. 4962, Berlin, Germany: Springer-Verlag, 2008, pp. 302-317.
• T. A. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer, "Temporal-safety proofs for systems code," in Computer Aided Verification: Proc. 14th Intl. Conf. (CAV 2002), E. Brinksma and K. G. Larsen, Eds., Lecture Notes in Computer Science, Vol. 2404, Berlin, Germany: Springer-Verlag, 2002, pp. 526-538.
• D. E. Culler, J. Hill, P. Buonadonna, R. Szewczyk, and A. Woo, "A network-centric approach to embedded software for tiny devices," in Proc. 1st Intl. Workshop on Embedded Software (EMSOFT 2001), T. A. Henzinger and C. M. Kirsch, Eds., Lecture Notes in Computer Science, Vol. 2211, London, UK: Springer-Verlag, 2001, pp. 114-130.

Selected Articles in journals or magazines

• T. A. Henzinger, B. Horowitz, and C. M. Kirsch, "Giotto: A time-triggered language for embedded programming," Proc. IEEE, vol. 91, no. 1, pp. 84-99, Jan. 2003.
• T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, "Lazy abstraction," ACM SIGPLAN Notices, vol. 37, no. 1, pp. 58-70, Jan. 2002.
• R. Alur and T. A. Henzinger, "Reactive modules," Formal Methods in System Design, vol. 15, no. 1, pp. 7-48, July 1999.
• T. A. Henzinger, P. Ho, and H. Wong-Toi, "HYTECH: A model checker for hybrid systems," Intl. J. Software Tools for Technology Transfer, vol. 1, no. 1-2, pp. 110-122, Dec. 1997.

Selected Articles in conference proceedings

• K. Chatterjee, A. Ghosal, T. A. Henzinger, D. Iercan, C. M. Kirsch, C. Pinello, and A. L. Sangiovanni-Vincentelli, "Logical reliability of interacting real-time tasks," in Proc. 2008 Design, Automation and Test in Europe (DATE '08), Leuven, Belgium: European Design and Automation Associaton, 2008, pp. 909-914.
• D. Beyer, T. A. Henzinger, A. Chakrabarti, and S. A. Seshia, "An application of Web-service interfaces," in Proc. 2007 IEEE Intl. Conf. on Web Services (ICWS '07), Los Alamitos, CA: IEEE Computer Society, 2007, pp. 831-838.
• A. Ghosal, A. L. Sangiovanni-Vincentelli, C. M. Kirsch, T. A. Henzinger, and D. Iercan, "A hierarchical coordination language for interacting real-time tasks," in Proc. 6th IEEE/ACM Intl. Conf. on Embedded Systems (EMSOFT 2006), New York, NY: The Association for Computing Machinery, Inc., 2006, pp. 132-141.
• T. A. Henzinger, "The theory of hybrid automata," in Proc. 11th Annual IEEE Symp. on Logic in Computer Science, Los Alamitos, CA: IEEE Computer Society Press, 1996, pp. 278-292.
• R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa, "VIS: A system for verification and synthesis," in Lecture Notes in Computer Science: Computer Aided Verification, R. Alur and T. A. Henzinger, Eds., Vol. 1102, London, UK: Springer-Verlag, 1996, pp. 428-432.

Technical Reports

• S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee, "A Theory of Synchronous Relational Interfaces," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-45, April 2010. [abstract]
• S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee, "On Relational Interfaces," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-60, May 2009. [abstract]
• K. Chatterjee, T. A. Henzinger, and V. Prabhu, "Trading Infinite Memory for Uniform Randomness in Timed Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2008-4, Jan. 2008. [abstract]
• K. Chatterjee, T. A. Henzinger, and F. Horn, "Finitary Winning in \omega-Regular Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-120, Oct. 2007. [abstract]
• K. Chatterjee, T. A. Henzinger, and N. Piterman, "Strategy Logic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-78, May 2007. [abstract]
• T. Brihaye, T. A. Henzinger, V. Prabhu, and J. Raskin, "Minimum-Time Reachability in Timed Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-47, April 2007. [abstract]
• K. Chatterjee, T. A. Henzinger, and N. Piterman, "Generalized Parity Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-144, Nov. 2006. [abstract]
• K. Chatterjee, R. Majumdar, and T. A. Henzinger, "Stochastic Limit-Average Games are in EXPTIME," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-143, Nov. 2006. [abstract]
• K. Chatterjee and T. A. Henzinger, "Reduction of Stochastic Parity to Stochastic Mean-payoff Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-140, Nov. 2006. [abstract]
• K. Chatterjee, L. de Alfaro, and T. A. Henzinger, "Memoryless Strategies in Concurrent Games with Reachability Objectives," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-05-1406, Aug. 2005. [abstract]
• K. Chatterjee, R. Majumdar, and T. A. Henzinger, "Stochastic Limit-Average Games are in EXPTIME," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-05-1405, Aug. 2005. [abstract]
• K. Chatterjee and T. A. Henzinger, "Algorithms for Stochastic Parity Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-05-1391, May 2005. [abstract]
• T. A. Henzinger, C. M. Kirsch, and S. Matic, "Distributed Schedule Carrying Code," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1360, 2004. [abstract]
• K. Chatterjee, L. de Alfaro, and T. A. Henzinger, "The Complexity of Stochastic Rabin and Streett Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1355, Nov. 2004. [abstract]
• K. Chatterjee, L. de Alfaro, and T. A. Henzinger, "The Complexity of Quantitative Concurrent Parity Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1354, Nov. 2004. [abstract]
• A. Ghosal, M. A. A. Sanvido, and T. A. Henzinger, "A Preliminary Report on the Embedded Virtual Machine," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1322, May 2004. [abstract]
• K. Chatterjee, M. Jurdzinski, and T. A. Henzinger, "Quantitative Stochastic Parity Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1280, 2003. [abstract]
• M. A. A. Sanvido, A. Ghosal, and T. A. Henzinger, "xGiotto Language Report," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1261, July 2003. [abstract]
• C. M. Kirsch, T. A. Henzinger, and M. A. A. Sanvido, "A Programmable Microkernal for Real-Time Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1250, June 2003. [abstract]
• T. A. Henzinger, C. M. Kirsch, and S. Matic, "Schedule-Carrying Code," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1230, Feb. 2003. [abstract]
• T. A. Henzinger, R. Jhala, and R. Majumdar, "Counterexample Guided Control," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-02-1213, Nov. 2002. [abstract]
• T. A. Henzinger, B. Horowitz, and C. M. Kirsch, "Giotto: a Time-triggered Language for Embedded Programming," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-00-1121, 2000. [abstract]
• T. A. Henzinger, B. Horowitz, and R. Majumdar, "Rectangular Hybrid Games (Extended Abstract)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-99-1044, 1999. [abstract]
• T. A. Henzinger, O. Kupferman, and S. Qadeer, "From Pre-Historic to Post-Modern Symbolic Model Checking," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/56, 1999.
• T. A. Henzinger, S. Qadeer, and S. Rajamani, "Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/55, 1999.
• T. A. Henzinger, X. Liu, S. Qadeer, and S. Rajamani, "Formal Specification and Verification of a Dataflow Processor Array," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/14, 1999.
• T. A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, J. Wang, and E. S. Kuh, "An Assume-Guaranteee Rule for Checking Simulation for Multipoint Moment Matching of Multiport Distributed Interconnect Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/13, 1999.
• J. Preubig, S. Kowalewski, H. Wong-Toi, and T. A. Henzinger, "An Algorithm for the Approximative Analysis of Rectangular Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/12, 1999.
• T. A. Henzinger and R. Majumdar, "A Classification of Symbolic Transition Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-99-1086, Dec. 1999. [abstract]
• P. Schobbens, J. Raskin, T. A. Henzinger, and L. Ferier, "Axioms for Real-Time Logics," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-99-1076, Nov. 1999. [abstract]
• T. A. Henzinger, J. Raskin, and P. Schobbens, "Temporal Logics, Automata, and Classical Theories for Defining Real-Time Languages," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-99-1074, Nov. 1999. [abstract]
• T. A. Henzinger and J. Raskin, "Robust Undecidability of Timed and Hybrid Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-99-1073, Oct. 1999. [abstract]
• T. A. Henzinger and R. Alur, "Reactive Modules," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/41, 1998.
• T. A. Henzinger, "It's About Time: Real-Time Logics Reviewed," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/40, 1998.
• L. de Alfaro, T. A. Henzinger, and O. Kupferman, "Concurrent Reachability Games," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/33, 1998.
• R. Alur, T. A. Henzinger, and H. Wong-Toi, "Symbolic Analysis of Hybrid Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/23, 1998.
• T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, "What's Decidable About Hybrid Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/22, 1998.
• R. Alur, T. A. Henzinger, and S. Rajamani, "Symbolic Exploration of Transition Hierarchies," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/21, 1998.
• R. Alur, T. A. Henzinger, and O. Kupferman, "Alternating-Time Temporal Logic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/20, 1998.
• T. A. Henzinger and V. Rusu, "Reachability Verification for Hybrid Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/19, 1998.
• R. Alur and T. A. Henzinger, "Finitary Fairness," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/18, 1998.
• T. A. Henzinger, P. Ho, and H. Wong-Toi, "HYTECH: A Model Checker for Hybrid Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/79, 1997.
• R. Alur and T. A. Henzinger, "Real-Time System = Discrete System + Clock Variables," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/78, 1997.
• R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, "Partial-Order Reduction in Symbolic State Space Exploration," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/30, 1997.
• T. A. Henzinger, "Discrete-Time Control for Rectangular Hybrid Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/29, 1997.
• R. Alur, L. Fix, and T. A. Henzinger, "Event-Clock Automata: A Determinizable Class of Timed Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/28, 1997.
• R. Alur, C. Courcoubetis, and T. A. Henzinger, "Computing Accumulated Delays in Real-Time Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/19, 1997.
• V. Gupta, T. A. Henzinger, and R. Jagadeesan, "Robust Timed Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/18, 1997.
• T. A. Henzinger and O. Kupferman, "From Quantity to Quality," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/17, 1997.
• T. A. Henzinger, "Using HyTech to Synthesize Control Parameters for a Steam Boiler," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/61, 1996.
• T. A. Henzinger, P. Ho, and H. Wong-Toi, "Algorithmic Analysis of Nonlinear Hybrid Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/60, 1996.
• T. A. Henzinger, "The Theory of Hybrid Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/28, 1996.