Thomas A. Henzinger

Institute of Science and Technology Austria

	2013
j63		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5): 640-657 (2013)
c258		Andreas Haas, Michael Lippautz, Thomas A. Henzinger, Hannes Payer, Ana Sokolova, Christoph M. Kirsch, Ali Sezgin: Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation. Conf. Computing Frontiers 2013: 17
c257		Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna: Quantitative abstraction refinement. POPL 2013: 115-128
c256		Thomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, Ali Sezgin, Ana Sokolova: Quantitative relaxation of concurrent data structures. POPL 2013: 317-328
e7		Antonín Kucera, Thomas A. Henzinger, Jaroslav Nesetril, Tomás Vojnar, David Antos (Eds.): Mathematical and Engineering Methods in Computer Science, 8th International Doctoral Workshop, MEMICS 2012, Znojmo, Czech Republic, October 25-28, 2012, Revised Selected Papers. Lecture Notes in Computer Science 7721, Springer 2013, isbn 978-3-642-36044-2
	2012
j62		Moshe Y. Vardi, Thomas A. Henzinger, Rajeev Alur, Marta Z. Kwiatkowska: 2011 CAV award announcement. Formal Methods in System Design 41(1): 1-2 (2012)
j61		Krishnendu Chatterjee, Thomas A. Henzinger: A survey of stochastic ω-regular games. J. Comput. Syst. Sci. 78(2): 394-413 (2012)
j60		Arkadeb Ghosal, Daniel T. Iercan, Christoph M. Kirsch, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli: Separate compilation of hierarchical real-time programs into linear-bounded Embedded Machine code. Sci. Comput. Program. 77(2): 96-112 (2012)
j59		Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna: Simulation distances. Theor. Comput. Sci. 413(1): 21-35 (2012)
j58		Jérôme Feret, Thomas A. Henzinger, Heinz Koeppl, Tatjana Petrov: Lumpability abstractions of rule-based systems. Theor. Comput. Sci. 431: 137-164 (2012)
c255		Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin: Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. CAV 2012: 294-309
c254		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Finite automata with time-delay blocks. EMSOFT 2012: 43-52
c253		Pavol Cerný, Sivakanth Gopi, Thomas A. Henzinger, Arjun Radhakrishna, Nishant Totla: Synthesis from incompatible specifications. EMSOFT 2012: 53-62
c252		Benoît Delahaye, Uli Fahrenberg, Thomas A. Henzinger, Axel Legay, Dejan Nickovic: Synchronous Interface Theories and Time Triggered Scheduling. FMOODS/FORTE 2012: 203-218
c251		Udi Boker, Thomas A. Henzinger: Approximate Determinization of Quantitative Automata. FSTTCS 2012: 362-373
c250		Thomas A. Henzinger: Quantitative Reactive Models. MoDELS 2012: 1-2
c249		Thomas A. Henzinger, Dejan Nickovic: Independent Implementability of Viewpoints. Monterey Workshop 2012: 380-395
c248		Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, Philipp Wendler: Conditional model checking: a technique to pass information between verifiers. SIGSOFT FSE 2012: 57
c247		Damien Zufferey, Thomas Wies, Thomas A. Henzinger: Ideal Abstractions for Well-Structured Transition Systems. VMCAI 2012: 445-460
c246		Thomas A. Henzinger: Keynote on "the propagation approach for computing biochemical reaction networks". Winter Simulation Conference 2012: 320
c245		Pavol Cerný, Martin Chmelik, Thomas A. Henzinger, Arjun Radhakrishna: Interface Simulation Distances. GandALF 2012: 29-42
i29		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy Improvement for Concurrent Reachability and Safety Games. CoRR abs/1201.2834 (2012)
i28		Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Counterexample-guided Planning. CoRR abs/1207.1373 (2012)
i27		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Finite Automata with Time-Delay Blocks (Extended Version). CoRR abs/1207.7019 (2012)
i26		Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Rabinovich, Jean-François Raskin: The Complexity of Multi-Mean-Payoff and Multi-Energy Games. CoRR abs/1209.3234 (2012)
	2011
j57		Jasmin Fisher, David Harel, Thomas A. Henzinger: Biology as reactivity. Commun. ACM 54(10): 72-82 (2011)
j56		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Timed Parity Games: Complexity and Robustness. Logical Methods in Computer Science 7(4) (2011)
j55		Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Verification of STM on relaxed memory models. Formal Methods in System Design 39(3): 297-331 (2011)
j54		Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf: Formalisms for Specifying Markovian Population Models. Int. J. Found. Comput. Sci. 22(4): 823-841 (2011)
j53		Frédéric Didier, Thomas A. Henzinger, Maria Mateescu, Verena Wolf: Approximation of event probabilities in noisy cellular processes. Theor. Comput. Sci. 412(21): 2128-2141 (2011)
j52		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Qualitative concurrent parity games. ACM Trans. Comput. Log. 12(4): 28 (2011)
j51		Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, Edward A. Lee: A Theory of Synchronous Relational Interfaces. ACM Trans. Program. Lang. Syst. 33(4): 14 (2011)
c244		Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh: Quantitative Synthesis for Concurrent Programs. CAV 2011: 243-259
c243		Thomas A. Henzinger, Maria Mateescu: Propagation models for computing biochemical reaction networks. CMSB 2011: 1-3
c242		Jasmin Fisher, Thomas A. Henzinger, Dejan Nickovic, Nir Piterman, Anmol V. Singh, Moshe Y. Vardi: Dynamic Reactive Modules. CONCUR 2011: 404-418
c241		Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger: The Complexity of Quantitative Information Flow Problems. CSF 2011: 205-217
c240		Udi Boker, Thomas A. Henzinger: Determinizing Discounted-Sum Automata. CSL 2011: 82-96
c239		Pavol Cerný, Thomas A. Henzinger: From boolean to quantitative synthesis. EMSOFT 2011: 149-154
c238		Thomas A. Henzinger, Vasu Singh, Thomas Wies, Damien Zufferey: Scheduling large jobs by abstraction refinement. EuroSys 2011: 329-342
c237		Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn: The Complexity of Request-Response Games. LATA 2011: 227-237
c236		Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman: Temporal Specifications with Accumulative Values. LICS 2011: 43-52
c235		Raluca Halalai, Thomas A. Henzinger, Vasu Singh: Quantitative Evaluation of BFT Protocols. QEST 2011: 255-264
c234		Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann: Specification-centered robustness. SIES 2011: 176-185
c233		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: QUASY: Quantitative Synthesis Tool. TACAS 2011: 267-271
i25		Krishnendu Chatterjee, Thomas A. Henzinger, Mathieu Tracol: The Decidability Frontier for Probabilistic Automata on Infinite Words. CoRR abs/1104.0127 (2011)
i24		Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh: Quantitative Synthesis for Concurrent Programs. CoRR abs/1104.4306 (2011)
i23		Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, Philipp Wendler: Conditional Model Checking. CoRR abs/1109.6926 (2011)
	2010
j50		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Expressiveness and Closure Properties for Quantitative Languages. Logical Methods in Computer Science 6(3) (2010)
j49		Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Model checking transactional memories. Distributed Computing 22(3): 129-145 (2010)
j48		Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Strategy logic. Inf. Comput. 208(6): 677-693 (2010)
j47		Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger: Strategy construction for parity games with imperfect information. Inf. Comput. 208(10): 1206-1220 (2010)
j46		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Quantitative languages. ACM Trans. Comput. Log. 11(4) (2010)
c232		Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey: FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. IEEE CLOUD 2010: 83-90
c231		Laurent Doyen, Thomas A. Henzinger, Axel Legay, Dejan Nickovic: Robustness of Sequential Circuits. ACSD 2010: 77-84
c230		Krishnendu Chatterjee, Thomas A. Henzinger: Probabilistic Automata on Infinite Words: Decidability and Undecidability Results. ATVA 2010: 1-16
c229		Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna: Quantitative Simulation Games. Essays in Memory of Amir Pnueli 2010: 42-60
c228		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: Measuring and Synthesizing Systems in Probabilistic Environments. CAV 2010: 380-395
c227		Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann: Robustness in the Presence of Liveness. CAV 2010: 410-424
c226		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna: Gist: A Solver for Probabilistic Games. CAV 2010: 665-669
c225		Thomas A. Henzinger, Linar Mikeev, Maria Mateescu, Verena Wolf: Hybrid numerical solution of the chemical master equation. CMSB 2010: 55-65
c224		Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna: Simulation Distances. CONCUR 2010: 253-268
c223		Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, Philippe Rannou: Mean-Payoff Automaton Expressions. CONCUR 2010: 269-283
c222		Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey: A marketplace for cloud resources. EMSOFT 2010: 1-8
c221		Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz, Damien Zufferey: Shape Refinement through Explicit Heap Analysis. FASE 2010: 263-277
c220		Thomas Wies, Damien Zufferey, Thomas A. Henzinger: Forward Analysis of Depth-Bounded Processes. FOSSACS 2010: 94-108
c219		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Generalized Mean-payoff and Energy Games. FSTTCS 2010: 505-516
c218		Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács: ABC: Algebraic Bound Computation for Loops. LPAR (Dakar) 2010: 103-118
c217		Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko: Aligators for Arrays (Tool Paper). LPAR (Yogyakarta) 2010: 348-356
c216		Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert, Thomas A. Henzinger: Randomness for Free. MFCS 2010: 246-257
c215		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Qualitative Analysis of Partially-Observable Markov Decision Processes. MFCS 2010: 258-269
c214		Thomas A. Henzinger: From Boolean to quantitative notions of correctness. POPL 2010: 157-158
c213		Frédéric Didier, Thomas A. Henzinger, Maria Mateescu, Verena Wolf: SABRE: A Tool for Stochastic Analysis of Biochemical Reaction Networks. QEST 2010: 193-194
c212		Rachid Guerraoui, Thomas A. Henzinger, Michal Kapalka, Vasu Singh: Transactions in the jungle. SPAA 2010: 263-272
c211		Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov: Invariant and Type Inference for Matrices. VMCAI 2010: 163-179
c210		Jérôme Feret, Thomas A. Henzinger, Heinz Koeppl, Tatjana Petrov: Lumpability Abstractions of Rule-based Systems. MeCBIC 2010: 142-161
e6		Krishnendu Chatterjee, Thomas A. Henzinger (Eds.): Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings. Lecture Notes in Computer Science 6246, Springer 2010, isbn 978-3-642-15296-2
i22		Yashdeep Godhal, Krishnendu Chatterjee, Thomas A. Henzinger: Synthesis of AMBA AHB from Formal Specification. CoRR abs/1001.2811 (2010)
i21		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: Measuring and Synthesizing Systems in Probabilistic Environments. CoRR abs/1004.0739 (2010)
i20		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna: GIST: A Solver for Probabilistic Games. CoRR abs/1004.2367 (2010)
i19		Thomas A. Henzinger, Maria Mateescu, Linar Mikeev, Verena Wolf: Hybrid Numerical Solution of the Chemical Master Equation. CoRR abs/1005.0747 (2010)
i18		Frédéric Didier, Thomas A. Henzinger, Maria Mateescu, Verena Wolf: SABRE: A Tool for Stochastic Analysis of Biochemical Reaction Networks. CoRR abs/1005.2819 (2010)
i17		Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert, Thomas A. Henzinger: Randomness for Free. CoRR abs/1006.0673 (2010)
i16		Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, Philippe Rannou: Mean-payoff Automaton Expressions. CoRR abs/1006.1492 (2010)
i15		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Generalized Mean-payoff and Energy Games. CoRR abs/1007.1669 (2010)
	2009
j45		Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi: The 2008 CAV Award citation. Formal Methods in System Design 35(1): 4-5 (2009)
j44		Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn: Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1) (2009)
c209		Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Better Quality in Synthesis through Quantitative Objectives. CAV 2009: 140-156
c208		Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Software Transactional Memory on Relaxed Memory Models. CAV 2009: 321-336
c207		Thomas A. Henzinger, Maria Mateescu, Verena Wolf: Sliding Window Abstraction for Infinite Markov Chains. CAV 2009: 337-352
c206		Frédéric Didier, Thomas A. Henzinger, Maria Mateescu, Verena Wolf: Approximation of Event Probabilities in Noisy Cellular Processes. CMSB 2009: 173-188
c205		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Probabilistic Weighted Automata. CONCUR 2009: 244-258
c204		Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, Edward A. Lee: On relational interfaces. EMSOFT 2009: 67-76
c203		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Alternating Weighted Automata. FCT 2009: 3-13
c202		Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann: Synthesizing robust systems. FMCAD 2009: 85-92
c201		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: A Survey of Stochastic Games with Limsup and Liminf Objectives. ICALP (2) 2009: 1-15
c200		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Expressiveness and Closure Properties for Quantitative Languages. LICS 2009: 199-208
c199		Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn: Stochastic Games with Finitary Objectives. MFCS 2009: 34-54
c198		Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf: Formalisms for Specifying Markovian Population Models. RP 2009: 3-23
c197		Thomas A. Henzinger, Christoph M. Kirsch, Eduardo R. B. Marques, Ana Sokolova: Distributed, Modular HTL. RTSS 2009: 171-180
c196		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Termination criteria for solving concurrent safety and reachability games. SODA 2009: 197-206
c195		Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger: Alpaga: A Tool for Solving Parity Games with Imperfect Information. TACAS 2009: 58-61
i14		Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger: Alpaga: A Tool for Solving Parity Games with Imperfect Information. CoRR abs/0901.4728 (2009)
i13		Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Better Quality in Synthesis through Quantitative Objectives. CoRR abs/0904.2638 (2009)
i12		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Expressiveness and Closure Properties for Quantitative Languages. CoRR abs/0905.2195 (2009)
i11		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Qualitative Analysis of Partially-observable Markov Decision Processes. CoRR abs/0909.1645 (2009)
i10		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Probabilistic Weighted Automata. CoRR abs/0909.1647 (2009)
	2008
j43		Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Equivalence of Labeled Markov Chains. Int. J. Found. Comput. Sci. 19(3): 549-563 (2008)
j42		Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Stochastic limit-average games are in EXPTIME. Int. J. Game Theory 37(2): 219-234 (2008)
j41		Krishnendu Chatterjee, Thomas A. Henzinger: Reduction of stochastic parity to stochastic mean-payoff games. Inf. Process. Lett. 106(1): 1-7 (2008)
c194		Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Completeness and Nondeterminism in Model Checking Transactional Memories. CONCUR 2008: 21-35
c193		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Environment Assumptions for Synthesis. CONCUR 2008: 147-161
c192		Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Sangram Raje: Strategy Construction for Parity Games with Imperfect Information. CONCUR 2008: 325-339
c191		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Quantitative Languages. CSL 2008: 385-400
c190		Krishnendu Chatterjee, Arkadeb Ghosal, Thomas A. Henzinger, Daniel T. Iercan, Christoph M. Kirsch, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli: Logical Reliability of Interacting Real-Time Tasks. DATE 2008: 909-914
c189		Laurent Doyen, Thomas A. Henzinger, Barbara Jobstmann, Tatjana Petrov: Interface theories with component reuse. EMSOFT 2008: 79-88
c188		Jasmin Fisher, Thomas A. Henzinger, Maria Mateescu, Nir Piterman: Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions. FMSB 2008: 17-32
c187		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Timed Parity Games: Complexity and Robustness. FORMATS 2008: 124-140
c186		Krishnendu Chatterjee, Koushik Sen, Thomas A. Henzinger: Model-Checking omega-Regular Properties of Interval Markov Chains. FoSSaCS 2008: 302-317
c185		Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Controller Synthesis with Budget Constraints. HSCC 2008: 72-86
c184		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Trading Infinite Memory for Uniform Randomness in Timed Games. HSCC 2008: 87-100
c183		Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Program Analysis with Dynamic Precision Adjustment. ASE 2008: 29-38
c182		Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács: Valigator: A Verification Tool with Bound and Invariant Generation. LPAR 2008: 333-342
c181		Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, Vasu Singh: Model checking transactional memories. PLDI 2008: 372-382
c180		Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu: Proving non-termination. POPL 2008: 147-158
c179		Krishnendu Chatterjee, Thomas A. Henzinger: Value Iteration. 25 Years of Model Checking 2008: 107-138
c178		Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Permissiveness in Transactional Memories. DISC 2008: 305-319
i9		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy Improvement for Concurrent Safety Games. CoRR abs/0804.4530 (2008)
i8		Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Algorithms for Büchi Games. CoRR abs/0805.2620 (2008)
i7		Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Stochastic Limit-Average Games are in EXPTIME. CoRR abs/0805.2622 (2008)
i6		Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Environment Assumptions for Synthesis. CoRR abs/0805.4167 (2008)
i5		Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Timed Parity Games: Complexity and Robustness. CoRR abs/0807.1165 (2008)
i4		Krishnendu Chatterjee, Thomas A. Henzinger: Probabilistic Systems with LimSup and LimInf Objectives. CoRR abs/0809.1465 (2008)
i3		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Termination Criteria for Solving Concurrent Safety and Reachability Games. CoRR abs/0809.4017 (2008)
	2007
j40		Thomas A. Henzinger, Joseph Sifakis: The Discipline of Embedded Systems Design. IEEE Computer 40(10): 32-40 (2007)
j39		Jean-François Raskin, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Algorithms for Omega-Regular Games with Imperfect Information. Logical Methods in Computer Science 3(3) (2007)
j38		Jasmin Fisher, Nir Piterman, Alex Hajnal, Thomas A. Henzinger: Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development. PLoS Computational Biology 3(5) (2007)
j37		Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The software model checker Blast. STTT 9(5-6): 505-525 (2007)
j36		Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman: Concurrent reachability games. Theor. Comput. Sci. 386(3): 188-217 (2007)
j35		Thomas A. Henzinger, Christoph M. Kirsch: The embedded machine: Predictable, portable real-time code. ACM Trans. Program. Lang. Syst. 29(6) (2007)
c177		Dirk Beyer, Thomas A. Henzinger, Vasu Singh: Algorithms for Interface Synthesis. CAV 2007: 4-19
c176		Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. CAV 2007: 504-518
c175		Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Strategy Logic. CONCUR 2007: 59-73
c174		Thomas A. Henzinger: Quantitative Generalizations of Languages. Developments in Language Theory 2007: 20-22
c173		Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Generalized Parity Games. FoSSaCS 2007: 153-167
c172		Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, Jean-François Raskin: Minimum-Time Reachability in Timed Games. ICALP 2007: 825-837
c171		Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, Sanjit A. Seshia: An Application ofWeb-Service Interfaces. ICWS 2007: 831-838
c170		Krishnendu Chatterjee, Thomas A. Henzinger: Probabilistic Systems with LimSup and LimInf Objectives. ILC 2007: 32-45
c169		Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Path invariants. PLDI 2007: 300-309
c168		Thomas A. Henzinger: Games, Time, and Probability: Graph Models for System Design and Analysis. SOFSEM (1) 2007: 103-110
c167		Krishnendu Chatterjee, Thomas A. Henzinger: Assume-Guarantee Synthesis. TACAS 2007: 261-275
c166		Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Invariant Synthesis for Combined Theories. VMCAI 2007: 378-394
e5		Jacques Duparc, Thomas A. Henzinger (Eds.): Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science 4646, Springer 2007, isbn 978-3-540-74914-1
i2		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Algorithms for Omega-Regular Games with Imperfect Information. CoRR abs/0706.2619 (2007)
	2006
j34		Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar: On the universal and existential fragments of the mu-calculus. Theor. Comput. Sci. 354(2): 173-186 (2006)
j33		Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with secure equilibria. Theor. Comput. Sci. 365(1-2): 67-82 (2006)
c165		Roman Manevich, John Field, Thomas A. Henzinger, G. Ramalingam, Mooly Sagiv: Abstract Counterexample-Based Refinement for Powerset Domains. Program Analysis and Compilation 2006: 273-292
c164		Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Antichains: A New Algorithm for Checking Universality of Finite Automata. CAV 2006: 17-30
c163		Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Lazy Shape Analysis. CAV 2006: 532-546
c162		Krishnendu Chatterjee, Thomas A. Henzinger: Strategy Improvement for Stochastic Rabin and Streett Games. CONCUR 2006: 375-389
c161		Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Algorithms for Omega-Regular Games with Imperfect Information, . CSL 2006: 287-302
c160		Thomas A. Henzinger, Nir Piterman: Solving Games Without Determinization. CSL 2006: 395-410
c159		Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Lazy Shape Analysis. Software Verification: Infinite-State Model Checking and Static Program Analysis 2006
c158		Arkadeb Ghosal, Alberto L. Sangiovanni-Vincentelli, Christoph M. Kirsch, Thomas A. Henzinger, Daniel T. Iercan: A hierarchical coordination language for interacting real-time tasks. EMSOFT 2006: 132-141
c157		Thomas A. Henzinger, Joseph Sifakis: The Embedded Systems Design Challenge. FM 2006: 1-15
c156		Thomas A. Henzinger, Vinayak S. Prabhu: Timed Alternating-Time Temporal Logic. FORMATS 2006: 1-17
c155		Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: Compositional Quantitative Reasoning. QEST 2006: 179-188
c154		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy Improvement for Concurrent Reachability Games. QEST 2006: 291-300
c153		Thomas A. Henzinger, Slobodan Matic: An Interface Algebra for Real-Time Components. IEEE Real Time Technology and Applications Symposium 2006: 253-266
c152		Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, Sriram K. Rajamani: SYNERGY: a new algorithm for property checking. SIGSOFT FSE 2006: 117-127
c151		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: The complexity of quantitative concurrent parity games. SODA 2006: 678-687
c150		Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Markov Decision Processes with Multiple Objectives. STACS 2006: 325-336
c149		Krishnendu Chatterjee, Thomas A. Henzinger: Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. STACS 2006: 512-523
c148		Krishnendu Chatterjee, Thomas A. Henzinger: Finitary Winning in omega-Regular Games. TACAS 2006: 257-271
c147		Jasmin Fisher, Thomas A. Henzinger: Executable biology. Winter Simulation Conference 2006: 1675-1682
	2005
j32		Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1): 139-170 (2005)
j31		Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin: A classification of symbolic transition systems. ACM Trans. Comput. Log. 6(1): 1-32 (2005)
c146		Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar: Verifying Quantitative Properties Using Bound Functions. CHARME 2005: 50-64
c145		Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Checking Memory Safety with Blast. FASE 2005: 2-18
c144		Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Automatic Rectangular Refinement of Affine Hybrid Systems. FORMATS 2005: 144-161
c143		Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu: Quantifying Similarities Between Timed Systems. FORMATS 2005: 226-241
c142		Krishnendu Chatterjee, Thomas A. Henzinger: Semiperfect-Information Games. FSTTCS 2005: 1-18
c141		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: The Complexity of Stochastic Rabin and Streett Games'. ICALP 2005: 878-890
c140		Thomas A. Henzinger, Christoph M. Kirsch, Slobodan Matic: Composable code generation for distributed giotto. LCTES 2005: 21-30
c139		Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Mean-Payoff Parity Games. LICS 2005: 178-187
c138		Slobodan Matic, Thomas A. Henzinger: Trading End-to-End Latency for Composability. RTSS 2005: 99-110
c137		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Permissive interfaces. ESEC/SIGSOFT FSE 2005: 31-40
c136		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The BLAST Software Verification System. SPIN 2005: 25-26
c135		Thomas A. Henzinger: Games in system design and verification. TARK 2005: 1-4
c134		Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Counterexample-guided Planning. UAI 2005: 104-111
c133		Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger: A programmable microkernel for real-time systems. VEE 2005: 35-45
c132		Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger: Web service interfaces. WWW 2005: 148-159
	2004
j30		Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, Jens Palsberg: Stack size analysis for interrupt-driven programs. Inf. Comput. 194(2): 144-174 (2004)
c131		Thomas A. Henzinger: Embedded Software: Better Models, Better Code. ICATPN 2004: 35-36
c130		Thomas A. Henzinger: Rich Interfaces for Software Modules. ECOOP 2004: 517-518
c129		Thomas A. Henzinger, Christoph M. Kirsch: A typed assembly language for real-time programs. EMSOFT 2004: 104-113
c128		Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with Secure Equilibria. FMCO 2004: 141-161
c127		Arkadeb Ghosal, Thomas A. Henzinger, Christoph M. Kirsch, Marco A. A. Sanvido: Event-Driven Programming with Logical Execution Times. HSCC 2004: 357-371
c126		Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Generating Tests from Counterexamples. ICSE 2004: 326-335
c125		Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: An Eclipse Plug-in for Model Checking. IWPC 2004: 251-255
c124		Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with Secure Equilibria. LICS 2004: 160-169
c123		Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Invited talk: the blast query language for software verification. PEPM 2004: 201-202
c122		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Race checking by context inference. PLDI 2004: 1-13
c121		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
c120		Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Invited talk: the blast query language for software verification. PPDP 2004: 1-2
c119		Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Trading Memory for Randomness. QEST 2004: 206-217
c118		Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The Blast Query Language for Software Verification.. SAS 2004: 2-18
c117		Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger: Quantitative stochastic parity games. SODA 2004: 121-130
c116		Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: Model Checking Discounted Temporal Properties. TACAS 2004: 77-92
	2003
j29		Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer: From Pre-Historic to Post-Modern Symbolic Model Checking. Formal Methods in System Design 23(3): 303-327 (2003)
j28		Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch: Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE 91(1): 84-99 (2003)
c115		Thomas A. Henzinger: Model Checking: From Hardware to Software. APLAS 2003: 176-177
c114		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking. Verification: Theory and Practice 2003: 332-358
c113		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer: Thread-Modular Abstraction Refinement. CAV 2003: 262-274
c112		Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: The Element of Surprise in Timed Games. CONCUR 2003: 142-156
c111		Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger: Simple Stochastic Parity Games. CSL 2003: 100-113
c110		Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Mariëlle Stoelinga: Resource Interfaces. EMSOFT 2003: 117-133
c109		Thomas A. Henzinger, Christoph M. Kirsch, Slobodan Matic: Schedule-Carrying Code. EMSOFT 2003: 241-256
c108		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Counterexample-Guided Control. ICALP 2003: 886-902
c107		Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: Discounting the Future in Systems Theory. ICALP 2003: 1022-1037
c106		Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, Jens Palsberg: Stack Size Analysis for Interrupt-Driven Programs. SAS 2003: 109-126
c105		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre: Software Verification with BLAST. SPIN 2003: 235-239
c104		Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar: On the Universal and Existential Fragments of the µ-Calculus. TACAS 2003: 49-64
c103		Thomas A. Henzinger: Automata for Specifying Component Interfaces. CIAA 2003: 1-2
	2002
j27		Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani: Fair Simulation. Inf. Comput. 173(1): 64-81 (2002)
j26		Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-time temporal logic. J. ACM 49(5): 672-713 (2002)
j25		Pierre-Yves Schobbens, Jean-François Raskin, Thomas A. Henzinger: Axioms for real-time logics. Theor. Comput. Sci. 274(1-2): 151-182 (2002)
j24		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran: An assume-guarantee rule for checking simulation. ACM Trans. Program. Lang. Syst. 24(1): 51-64 (2002)
c102		Thomas A. Henzinger: The Symbolic Approach to Hybrid Systems. CAV 2002: 57
c101		Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Synchronous and Bidirectional Component Interfaces. CAV 2002: 414-427
c100		Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang: Interface Compatibility Checking for Software Modules. CAV 2002: 428-441
c99		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer: Temporal-Safety Proofs for Systems Code. CAV 2002: 526-538
c98		Marcin Jurdzinski, Orna Kupferman, Thomas A. Henzinger: Trading Probability for Fairness. CSL 2002: 292-305
c97		Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger, Wolfgang Pree: A Giotto-Based Helicopter Control System. EMSOFT 2002: 46-60
c96		Thomas A. Henzinger, Christoph M. Kirsch, Rupak Majumdar, Slobodan Matic: Time-Safety Checking for Embedded Programs. EMSOFT 2002: 76-92
c95		Luca de Alfaro, Thomas A. Henzinger, Mariëlle Stoelinga: Timed Interfaces. EMSOFT 2002: 108-122
c94		Thomas A. Henzinger: From Models to Code: The Missing Link in Embedded Software. HSCC 2002: 5-6
c93		Franck Cassez, Thomas A. Henzinger, Jean-François Raskin: A Comparison of Control Problems for Timed and Hybrid Systems. HSCC 2002: 134-148
c92		Thomas A. Henzinger, Sriram C. Krishnan, Orna Kupferman, Freddy Y. C. Mang: Synthesis of Uninitialized Systems. ICALP 2002: 644-656
c91		Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli: Convertibility verification and converter synthesis: two faces of the same coin. ICCAD 2002: 132-139
c90		Thomas A. Henzinger, Christoph M. Kirsch: The Embedded Machine: Predictable, Portable Real-Time Code. PLDI 2002: 315-326
c89		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre: Lazy abstraction. POPL 2002: 58-70
	2001
j23		Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Partial-Order Reduction in Symbolic State-Space Exploration. Formal Methods in System Design 18(2): 97-116 (2001)
j22		Rajeev Alur, Thomas A. Henzinger: Introduction. Inf. Comput. 164(2): 233 (2001)
c88		Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala: Compositional Methods for Probabilistic Systems. CONCUR 2001: 351-365
c87		Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: Symbolic Algorithms for Infinite-State Games. CONCUR 2001: 536-550
c86		Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: The Control of Synchronous Systems, Part II. CONCUR 2001: 566-582
c85		Luca de Alfaro, Thomas A. Henzinger: Interface Theories for Component-Based Design. EMSOFT 2001: 148-165
c84		Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch: Giotto: A Time-Triggered Language for Embedded Programming. EMSOFT 2001: 166-184
c83		Alberto L. Sangiovanni-Vincentelli, Thomas A. Henzinger, Bruce H. Krogh, Oded Maler, Manfred Morari, Costas C. Pantelides, George J. Pappas, Tunc Simsec, Janos Sztipanovits, Stavros Tripakis: Hybrid Systems Applications: An Oxymoron? HSCC 2001: 5-6
c82		Thomas A. Henzinger, Marius Minea, Vinayak S. Prabhu: Assume-Guarantee Reasoning for Hierarchical Hybrid Systems. HSCC 2001: 275-290
c81		Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, Bow-Yaw Wang: JMOCHA: A Model Checking Tool that Exploits Design Structure. ICSE 2001: 835-836
c80		Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch: Embedded Control Systems Development with Giotto. LCTES/OM 2001: 64-72
c79		Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: From Verification to Control: Dynamic Programs for Omega-Regular Objectives. LICS 2001: 279-290
c78		Luca de Alfaro, Thomas A. Henzinger: Interface automata. ESEC / SIGSOFT FSE 2001: 109-120
c77		Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: MCWEB: A Model-Checking Tool for Web Site Debugging. WWW Posters 2001
e4		Thomas A. Henzinger, Christoph M. Kirsch (Eds.): Embedded Software, First International Workshop, EMSOFT 2001, Tahoe City, CA, USA, October, 8-10, 2001, Proceedings. Lecture Notes in Computer Science 2211, Springer 2001, isbn 3-540-42673-6
i1		Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin: A Classification of Symbolic Transition Systems. CoRR cs.LO/0101013 (2001)
	2000
j21		Thomas A. Henzinger: Exploiting Design Structure in Model Checking. Electr. Notes Theor. Comput. Sci. 39(3): 322 (2000)
j20		Thomas A. Henzinger: New directions in computer-aided verification. ACM SIGSOFT Software Engineering Notes 25(1): 56-57 (2000)
c76		Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Detecting Errors Before Reaching Them. CAV 2000: 186-201
c75		Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: The Control of Synchronous Systems. CONCUR 2000: 458-473
c74		Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, Howard Wong-Toi: Beyond HYTECH: Hybrid Systems Analysis Using Interval Numerical Methods. HSCC 2000: 130-144
c73		Thomas A. Henzinger, Jean-François Raskin: Robust Undecidability of Timed and Hybrid Systems. HSCC 2000: 145-159
c72		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. ICCAD 2000: 245-252
c71		Thomas A. Henzinger: Masaccio: A Formal Model for Embedded Components. IFIP TCS 2000: 549-563
c70		Luca de Alfaro, Thomas A. Henzinger: Concurrent Omega-Regular Games. LICS 2000: 141-154
c69		Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, Jean-François Raskin: Abstract Interpretation of Game Properties. SAS 2000: 220-239
c68		Thomas A. Henzinger, Rupak Majumdar: A Classification of Symbolic Transition Systems. STACS 2000: 13-34
c67		Thomas A. Henzinger, Rupak Majumdar: Symbolic Model Checking for Rectangular Hybrid Systems. TACAS 2000: 142-156
c66		Thomas A. Henzinger, Sriram K. Rajamani: Fair Bisimulation. TACAS 2000: 299-314
	1999
j19		Rajeev Alur, Thomas A. Henzinger: Introduction. Formal Methods in System Design 14(3): 235 (1999)
j18		Rajeev Alur, Thomas A. Henzinger: Introduction. Formal Methods in System Design 15(1): 5 (1999)
j17		Rajeev Alur, Thomas A. Henzinger: Reactive Modules. Formal Methods in System Design 15(1): 7-48 (1999)
j16		Rajeev Alur, Limor Fix, Thomas A. Henzinger: Event-Clock Automata: A Determinizable Class of Timed Automata. Theor. Comput. Sci. 211(1-2): 253-273 (1999)
j15		Thomas A. Henzinger, Peter W. Kopke: Discrete-Time Control for Rectangular Hybrid Automata. Theor. Comput. Sci. 221(1-2): 369-392 (1999)
c65		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Assume-Guarantee Refinement Between Different Time Scales. CAV 1999: 208-221
c64		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. CAV 1999: 301-315
c63		Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Automating Modular Verification. CONCUR 1999: 82-97
c62		Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar: Rectangular Hybrid Games. CONCUR 1999: 320-335
c61		Thomas A. Henzinger, Xiaojun Liu, Shaz Qadeer, Sriram K. Rajamani: Formal specification and verification of a dataflow processor array. ICCAD 1999: 494-499
	1998
j14		Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaiya: What's Decidable about Hybrid Automata? J. Comput. Syst. Sci. 57(1): 94-124 (1998)
j13		Rajeev Alur, Thomas A. Henzinger: Finitary Fairness. ACM Trans. Program. Lang. Syst. 20(6): 1171-1194 (1998)
c60		Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer: From Pre-historic to Post-modern Symbolic Model Checking. CAV 1998: 195-206
c59		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: You Assume, We Guarantee: Methodology and Case Studies. CAV 1998: 440-451
c58		Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran: MOCHA: Modularity in Model Checking. CAV 1998: 521-525
c57		Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi: Alternating Refinement Relations. CONCUR 1998: 163-178
c56		Jean-François Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger: Axioms for Real-Time Logics. CONCUR 1998: 219-236
c55		Thomas A. Henzinger: It's About Time: Real-Time Logics Reviewed. CONCUR 1998: 439-454
c54		Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran: An Assume-Guarantee Rule for Checking Simulation. FMCAD 1998: 421-432
c53		Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman: Concurrent Reachability Games. FOCS 1998: 564-575
c52		Jörg Preußig, Stefan Kowalewski, Howard Wong-Toi, Thomas A. Henzinger: An Algorithm for the Approximative Analysis of Rectangular Automata. FTRTFT 1998: 228-240
c51		Thomas A. Henzinger, Vlad Rusu: Reachability Verification for Hybrid Automata. HSCC 1998: 190-204
c50		Thomas A. Henzinger: Model Checking Game Properties of Multi-agent Systems (Abstract). ICALP 1998: 543
c49		Thomas A. Henzinger, Jean-François Raskin, Pierre-Yves Schobbens: The Regular Real-Time Languages. ICALP 1998: 580-591
c48		Thomas A. Henzinger: Computer-aided Verification of Embedded Systems. IFIP Congress: Fundamentals - Foundations of Computer Science 1998: 89-92
c47		Rajeev Alur, Thomas A. Henzinger, Sriram K. Rajamani: Symbolic Exploration of transition Hierarchies. TACAS 1998: 330-344
e3		Thomas A. Henzinger, Shankar Sastry (Eds.): Hybrid Systems: Computation and Control, First International Workshop, HSCC'98, Berkeley, California, USA, April 13-15, 1998, Proceedings. Lecture Notes in Computer Science 1386, Springer 1998, isbn 3-540-64358-3
	1997
j12		Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: Computing Accumulated Delays in Real-time Systems. Formal Methods in System Design 11(2): 137-155 (1997)
j11		Rajeev Alur, Thomas A. Henzinger: Real-Time System = Discrete System + Clock Variables. STTT 1(1-2): 86-109 (1997)
j10		Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HYTECH: A Model Checker for Hybrid Systems. STTT 1(1-2): 110-122 (1997)
c46		Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Partial-Order Reduction in Symbolic State Space Exploration. CAV 1997: 340-351
c45		Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HYTECH: A Model Checker for Hybrid Systems. CAV 1997: 460-463
c44		Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-Time Temporal Logic. COMPOS 1997: 23-60
c43		Rajeev Alur, Thomas A. Henzinger: Modularity for Timed and Hybrid Systems. CONCUR 1997: 74-88
c42		Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani: Fair Simulation. CONCUR 1997: 273-287
c41		Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-time Temporal Logic. FOCS 1997: 100-109
c40		Thomas A. Henzinger, Orna Kupferman: From Quantity to Quality. HART 1997: 48-62
c39		Vineet Gupta, Thomas A. Henzinger, Radha Jagadeesan: Robust Timed Automata. HART 1997: 331-345
c38		Thomas A. Henzinger, Peter W. Kopke: Discrete-Time Control for Rectangular Hybrid Automata. ICALP 1997: 582-593
	1996
j9		Thomas A. Henzinger: Some Myths About Formal Verification. ACM Comput. Surv. 28(4es): 119 (1996)
j8		Rajeev Alur, Tomás Feder, Thomas A. Henzinger: The Benefits of Relaxing Punctuality. J. ACM 43(1): 116-146 (1996)
j7		Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho: Automatic Symbolic Verification of Embedded Systems. IEEE Trans. Software Eng. 22(3): 181-201 (1996)
c37		Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi: A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. CONCUR 1996: 514-529
c36		Thomas A. Henzinger, Peter W. Kopke: State Equivalences for Rectangular Hybrid Automata. CONCUR 1996: 530-545
c35		Rajeev Alur, Thomas A. Henzinger: Reactive Modules. LICS 1996: 207-218
c34		Thomas A. Henzinger: The Theory of Hybrid Automata. LICS 1996: 278-292
e2		Rajeev Alur, Thomas A. Henzinger (Eds.): Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings. Lecture Notes in Computer Science 1102, Springer 1996, isbn 3-540-61474-5
e1		Rajeev Alur, Thomas A. Henzinger, Eduardo D. Sontag (Eds.): Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA. Lecture Notes in Computer Science 1066, Springer 1996, isbn 3-540-61155-X
	1995
j6		Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine: The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. 138(1): 3-34 (1995)
c33		Rajeev Alur, Thomas A. Henzinger: Local Liveness for Compositional Modeling of Fair Reactive Systems. CAV 1995: 166-179
c32		Thomas A. Henzinger, Pei-Hsin Ho: Algorithmic Analysis of Nonlinear Hybrid Systems. CAV 1995: 225-238
c31		Thomas A. Henzinger, Howard Wong-Toi: Using HyTech to Synthesize Control Parameters for a Steam Boiler. Formal Methods for Industrial Applications 1995: 265-282
c30		Monika Rauch Henzinger, Thomas A. Henzinger, Peter W. Kopke: Computing Simulations on Finite and Infinite Graphs. FOCS 1995: 453-462
c29		Thomas A. Henzinger, Howard Wong-Toi: Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems. Hybrid Systems 1995: 377-388
c28		Thomas A. Henzinger: Hybrid Automata with Finite Bisimulatioins. ICALP 1995: 324-335
c27		Thomas A. Henzinger, Peter W. Kopke, Howard Wong-Toi: The Expressive Power of Clocks. ICALP 1995: 417-428
c26		Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HyTech: The Next Generation. RTSS 1995: 56-65
c25		Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaiya: What's decidable about hybrid automata? STOC 1995: 373-382
c24		Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: A User Guide to HyTech. TACAS 1995: 41-71
	1994
j5		Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine: Symbolic Model Checking for Real-Time Systems. Inf. Comput. 111(2): 193-244 (1994)
j4		Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Timed Transition Systems. Inf. Comput. 112(2): 273-337 (1994)
j3		Rajeev Alur, Thomas A. Henzinger: A Really Temporal Logic. J. ACM 41(1): 181-204 (1994)
c23		Rajeev Alur, Limor Fix, Thomas A. Henzinger: A Determinizable Class of Timed Automata. CAV 1994: 1-13
c22		Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: The Observational Power of Clocks. CONCUR 1994: 162-177
c21		Thomas A. Henzinger, Peter W. Kopke: Verification Methods for the Divergent Runs of Clock Systems. FTRTFT 1994: 351-372
c20		Arjun Kapur, Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Prooving Safety Properties of Hybrid Systems. FTRTFT 1994: 431-454
c19		Thomas A. Henzinger, Pei-Hsin Ho: A Note on Abstract Interpretation Strategies for Hybrid Automata. Hybrid Systems 1994: 252-264
c18		Thomas A. Henzinger, Pei-Hsin Ho: HYTECH: The Cornell HYbrid TECHnology Tool. Hybrid Systems 1994: 265-293
c17		Rajeev Alur, Thomas A. Henzinger: Finitary Fairness. LICS 1994: 52-61
	1993
j2		Rajeev Alur, Thomas A. Henzinger: Real-Time Logics: Complexity and Expressiveness. Inf. Comput. 104(1): 35-77 (1993)
c16		Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: Computing Accumulated Delays in Real-time Systems. CAV 1993: 181-193
c15		Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho: Automatic Symbolic Verification of Embedded Systems. RTSS 1993: 2-11
c14		Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601
	1992
j1		Thomas A. Henzinger: Sooner is Safer Than Later. Inf. Process. Lett. 43(3): 135-141 (1992)
c13		Rajeev Alur, Thomas A. Henzinger: Back to the Future: Towards a Theory of Timed Regular Languages. FOCS 1992: 177-186
c12		Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Towards Refining Temporal Specifications into Hybrid Systems. Hybrid Systems 1992: 60-76
c11		Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, Pei-Hsin Ho: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Hybrid Systems 1992: 209-229
c10		Thomas A. Henzinger, Zohar Manna, Amir Pnueli: What Good Are Digital Clocks? ICALP 1992: 545-558
c9		Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine: Symbolic Model Checking for Real-time Systems. LICS 1992: 394-406
	1991
c8		Rajeev Alur, Tomás Feder, Thomas A. Henzinger: The Benefits of Relaxing Punctuality. PODC 1991: 139-152
c7		Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Real-time Systems. POPL 1991: 353-366
c6		Rajeev Alur, Thomas A. Henzinger: Logics and Models of Real Time: A Survey. REX Workshop 1991: 74-106
c5		Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Timed Transition Systems. REX Workshop 1991: 226-251
	1990
c4		Rajeev Alur, Thomas A. Henzinger: Real-time Logics: Complexity and Expressiveness. LICS 1990: 390-401
c3		Thomas A. Henzinger: Half-Order Modal Logic: How to Prove Real-Time Properties. PODC 1990: 281-296
	1989
c2		Rajeev Alur, Thomas A. Henzinger: A Really Temporal Logic. FOCS 1989: 164-169
	1985
c1		Thomas A. Henzinger, Hubert Hofbauer: PROOF-PAD: An Interactive Proof Generating System Using Natural Deduction. ÖGAI 1985: 173-184