2009 | ||
---|---|---|
251 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Termination criteria for solving concurrent safety and reachability games. SODA 2009: 197-206 |
250 | EE | 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 |
249 | EE | 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) |
248 | EE | Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Better Quality in Synthesis through Quantitative Objectives CoRR abs/0904.2638: (2009) |
2008 | ||
247 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Value Iteration. 25 Years of Model Checking 2008: 107-138 |
246 | EE | Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Program Analysis with Dynamic Precision Adjustment. ASE 2008: 29-38 |
245 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Environment Assumptions for Synthesis. CONCUR 2008: 147-161 |
244 | EE | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Completeness and Nondeterminism in Model Checking Transactional Memories. CONCUR 2008: 21-35 |
243 | EE | Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Sangram Raje: Strategy Construction for Parity Games with Imperfect Information. CONCUR 2008: 325-339 |
242 | EE | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger: Quantitative Languages. CSL 2008: 385-400 |
241 | EE | 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 |
240 | EE | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Permissiveness in Transactional Memories. DISC 2008: 305-319 |
239 | EE | Laurent Doyen, Thomas A. Henzinger, Barbara Jobstmann, Tatjana Petrov: Interface theories with component reuse. EMSOFT 2008: 79-88 |
238 | EE | Jasmin Fisher, Thomas A. Henzinger, Maria Mateescu, Nir Piterman: Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions. FMSB 2008: 17-32 |
237 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Timed Parity Games: Complexity and Robustness. FORMATS 2008: 124-140 |
236 | EE | Krishnendu Chatterjee, Koushik Sen, Thomas A. Henzinger: Model-Checking omega-Regular Properties of Interval Markov Chains. FoSSaCS 2008: 302-317 |
235 | EE | Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Controller Synthesis with Budget Constraints. HSCC 2008: 72-86 |
234 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Trading Infinite Memory for Uniform Randomness in Timed Games. HSCC 2008: 87-100 |
233 | EE | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács: Valigator: A Verification Tool with Bound and Invariant Generation. LPAR 2008: 333-342 |
232 | EE | Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, Vasu Singh: Model checking transactional memories. PLDI 2008: 372-382 |
231 | EE | Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu: Proving non-termination. POPL 2008: 147-158 |
230 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy Improvement for Concurrent Safety Games CoRR abs/0804.4530: (2008) |
229 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Algorithms for Büchi Games CoRR abs/0805.2620: (2008) |
228 | EE | Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Stochastic Limit-Average Games are in EXPTIME CoRR abs/0805.2622: (2008) |
227 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Environment Assumptions for Synthesis CoRR abs/0805.4167: (2008) |
226 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu: Timed Parity Games: Complexity and Robustness CoRR abs/0807.1165: (2008) |
225 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Probabilistic Systems with LimSup and LimInf Objectives CoRR abs/0809.1465: (2008) |
224 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Termination Criteria for Solving Concurrent Safety and Reachability Games CoRR abs/0809.4017: (2008) |
223 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Reduction of stochastic parity to stochastic mean-payoff games. Inf. Process. Lett. 106(1): 1-7 (2008) |
222 | EE | Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Equivalence of Labeled Markov Chains. Int. J. Found. Comput. Sci. 19(3): 549-563 (2008) |
2007 | ||
221 | Jacques Duparc, Thomas A. Henzinger: Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings Springer 2007 | |
220 | EE | Dirk Beyer, Thomas A. Henzinger, Vasu Singh: Algorithms for Interface Synthesis. CAV 2007: 4-19 |
219 | EE | 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 |
218 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Strategy Logic. CONCUR 2007: 59-73 |
217 | EE | Thomas A. Henzinger: Quantitative Generalizations of Languages. Developments in Language Theory 2007: 20-22 |
216 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman: Generalized Parity Games. FoSSaCS 2007: 153-167 |
215 | EE | Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, Jean-François Raskin: Minimum-Time Reachability in Timed Games. ICALP 2007: 825-837 |
214 | EE | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, Sanjit A. Seshia: An Application ofWeb-Service Interfaces. ICWS 2007: 831-838 |
213 | EE | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Path invariants. PLDI 2007: 300-309 |
212 | EE | Thomas A. Henzinger: Games, Time, and Probability: Graph Models for System Design and Analysis. SOFSEM (1) 2007: 103-110 |
211 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Assume-Guarantee Synthesis. TACAS 2007: 261-275 |
210 | EE | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Invariant Synthesis for Combined Theories. VMCAI 2007: 378-394 |
209 | EE | Thomas A. Henzinger, Christoph M. Kirsch: The embedded machine: Predictable, portable real-time code. ACM Trans. Program. Lang. Syst. 29(6): (2007) |
208 | EE | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Algorithms for Omega-Regular Games with Imperfect Information CoRR abs/0706.2619: (2007) |
207 | EE | Thomas A. Henzinger, Joseph Sifakis: The Discipline of Embedded Systems Design. IEEE Computer 40(10): 32-40 (2007) |
206 | EE | 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) |
205 | EE | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The software model checker Blast. STTT 9(5-6): 505-525 (2007) |
204 | EE | Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman: Concurrent reachability games. Theor. Comput. Sci. 386(3): 188-217 (2007) |
2006 | ||
203 | EE | 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 |
202 | EE | Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Lazy Shape Analysis. CAV 2006: 532-546 |
201 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Strategy Improvement for Stochastic Rabin and Streett Games. CONCUR 2006: 375-389 |
200 | EE | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Algorithms for Omega-Regular Games with Imperfect Information, . CSL 2006: 287-302 |
199 | EE | Thomas A. Henzinger, Nir Piterman: Solving Games Without Determinization. CSL 2006: 395-410 |
198 | EE | 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 |
197 | EE | Thomas A. Henzinger, Joseph Sifakis: The Embedded Systems Design Challenge. FM 2006: 1-15 |
196 | EE | Thomas A. Henzinger, Vinayak S. Prabhu: Timed Alternating-Time Temporal Logic. FORMATS 2006: 1-17 |
195 | EE | Thomas A. Henzinger, Slobodan Matic: An Interface Algebra for Real-Time Components. IEEE Real Time Technology and Applications Symposium 2006: 253-266 |
194 | EE | 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 |
193 | EE | Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: Compositional Quantitative Reasoning. QEST 2006: 179-188 |
192 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Strategy Improvement for Concurrent Reachability Games. QEST 2006: 291-300 |
191 | EE | 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 |
190 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: The complexity of quantitative concurrent parity games. SODA 2006: 678-687 |
189 | EE | Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger: Markov Decision Processes with Multiple Objectives. STACS 2006: 325-336 |
188 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. STACS 2006: 512-523 |
187 | EE | Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Lazy Shape Analysis. Software Verification: Infinite-State Model Checking and Static Program Analysis 2006 |
186 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Finitary Winning in omega-Regular Games. TACAS 2006: 257-271 |
185 | EE | Jasmin Fisher, Thomas A. Henzinger: Executable biology. Winter Simulation Conference 2006: 1675-1682 |
184 | EE | 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) |
183 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with secure equilibria. Theor. Comput. Sci. 365(1-2): 67-82 (2006) |
2005 | ||
182 | EE | Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar: Verifying Quantitative Properties Using Bound Functions. CHARME 2005: 50-64 |
181 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Permissive interfaces. ESEC/SIGSOFT FSE 2005: 31-40 |
180 | EE | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Checking Memory Safety with Blast. FASE 2005: 2-18 |
179 | EE | Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Automatic Rectangular Refinement of Affine Hybrid Systems. FORMATS 2005: 144-161 |
178 | EE | Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu: Quantifying Similarities Between Timed Systems. FORMATS 2005: 226-241 |
177 | EE | Krishnendu Chatterjee, Thomas A. Henzinger: Semiperfect-Information Games. FSTTCS 2005: 1-18 |
176 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: The Complexity of Stochastic Rabin and Streett Games'. ICALP 2005: 878-890 |
175 | EE | Thomas A. Henzinger, Christoph M. Kirsch, Slobodan Matic: Composable code generation for distributed giotto. LCTES 2005: 21-30 |
174 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Mean-Payoff Parity Games. LICS 2005: 178-187 |
173 | EE | Slobodan Matic, Thomas A. Henzinger: Trading End-to-End Latency for Composability. RTSS 2005: 99-110 |
172 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The BLAST Software Verification System. SPIN 2005: 25-26 |
171 | EE | Thomas A. Henzinger: Games in system design and verification. TARK 2005: 1-4 |
170 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Counterexample-guided Planning. UAI 2005: 104-111 |
169 | EE | Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger: A programmable microkernel for real-time systems. VEE 2005: 35-45 |
168 | EE | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger: Web service interfaces. WWW 2005: 148-159 |
167 | EE | Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin: A classification of symbolic transition systems. ACM Trans. Comput. Log. 6(1): 1-32 (2005) |
166 | EE | 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) |
2004 | ||
165 | EE | Thomas A. Henzinger: Rich Interfaces for Software Modules. ECOOP 2004: 517-518 |
164 | EE | Thomas A. Henzinger, Christoph M. Kirsch: A typed assembly language for real-time programs. EMSOFT 2004: 104-113 |
163 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with Secure Equilibria. FMCO 2004: 141-161 |
162 | EE | Arkadeb Ghosal, Thomas A. Henzinger, Christoph M. Kirsch, Marco A. A. Sanvido: Event-Driven Programming with Logical Execution Times. HSCC 2004: 357-371 |
161 | EE | Thomas A. Henzinger: Embedded Software: Better Models, Better Code. ICATPN 2004: 35-36 |
160 | EE | Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Generating Tests from Counterexamples. ICSE 2004: 326-335 |
159 | EE | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: An Eclipse Plug-in for Model Checking. IWPC 2004: 251-255 |
158 | EE | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski: Games with Secure Equilibria. LICS 2004: 160-169 |
157 | EE | Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Invited talk: the blast query language for software verification. PEPM 2004: 201-202 |
156 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Race checking by context inference. PLDI 2004: 1-13 |
155 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244 |
154 | EE | Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Invited talk: the blast query language for software verification. PPDP 2004: 1-2 |
153 | EE | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger: Trading Memory for Randomness. QEST 2004: 206-217 |
152 | EE | Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: The Blast Query Language for Software Verification.. SAS 2004: 2-18 |
151 | EE | Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger: Quantitative stochastic parity games. SODA 2004: 121-130 |
150 | EE | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: Model Checking Discounted Temporal Properties. TACAS 2004: 77-92 |
149 | EE | 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) |
2003 | ||
148 | EE | Thomas A. Henzinger: Model Checking: From Hardware to Software. APLAS 2003: 176-177 |
147 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer: Thread-Modular Abstraction Refinement. CAV 2003: 262-274 |
146 | EE | Thomas A. Henzinger: Automata for Specifying Component Interfaces. CIAA 2003: 1-2 |
145 | EE | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga: The Element of Surprise in Timed Games. CONCUR 2003: 142-156 |
144 | EE | Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger: Simple Stochastic Parity Games. CSL 2003: 100-113 |
143 | EE | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Mariëlle Stoelinga: Resource Interfaces. EMSOFT 2003: 117-133 |
142 | EE | Thomas A. Henzinger, Christoph M. Kirsch, Slobodan Matic: Schedule-Carrying Code. EMSOFT 2003: 241-256 |
141 | EE | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: Discounting the Future in Systems Theory. ICALP 2003: 1022-1037 |
140 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Counterexample-Guided Control. ICALP 2003: 886-902 |
139 | EE | Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, Jens Palsberg: Stack Size Analysis for Interrupt-Driven Programs. SAS 2003: 109-126 |
138 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre: Software Verification with BLAST. SPIN 2003: 235-239 |
137 | EE | Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar: On the Universal and Existential Fragments of the µ-Calculus. TACAS 2003: 49-64 |
136 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking. Verification: Theory and Practice 2003: 332-358 |
135 | EE | 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) |
134 | 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) | |
2002 | ||
133 | EE | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Synchronous and Bidirectional Component Interfaces. CAV 2002: 414-427 |
132 | EE | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang: Interface Compatibility Checking for Software Modules. CAV 2002: 428-441 |
131 | EE | 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 |
130 | EE | Thomas A. Henzinger: The Symbolic Approach to Hybrid Systems. CAV 2002: 57 |
129 | EE | Marcin Jurdzinski, Orna Kupferman, Thomas A. Henzinger: Trading Probability for Fairness. CSL 2002: 292-305 |
128 | EE | Luca de Alfaro, Thomas A. Henzinger, Mariëlle Stoelinga: Timed Interfaces. EMSOFT 2002: 108-122 |
127 | EE | Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger, Wolfgang Pree: A Giotto-Based Helicopter Control System. EMSOFT 2002: 46-60 |
126 | EE | Thomas A. Henzinger, Christoph M. Kirsch, Rupak Majumdar, Slobodan Matic: Time-Safety Checking for Embedded Programs. EMSOFT 2002: 76-92 |
125 | EE | Franck Cassez, Thomas A. Henzinger, Jean-François Raskin: A Comparison of Control Problems for Timed and Hybrid Systems. HSCC 2002: 134-148 |
124 | EE | Thomas A. Henzinger: From Models to Code: The Missing Link in Embedded Software. HSCC 2002: 5-6 |
123 | EE | Thomas A. Henzinger, Sriram C. Krishnan, Orna Kupferman, Freddy Y. C. Mang: Synthesis of Uninitialized Systems. ICALP 2002: 644-656 |
122 | EE | 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 |
121 | EE | Thomas A. Henzinger, Christoph M. Kirsch: The Embedded Machine: Predictable, Portable Real-Time Code. PLDI 2002: 315-326 |
120 | EE | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre: Lazy abstraction. POPL 2002: 58-70 |
119 | EE | 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) |
118 | EE | Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani: Fair Simulation. Inf. Comput. 173(1): 64-81 (2002) |
117 | EE | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-time temporal logic. J. ACM 49(5): 672-713 (2002) |
116 | EE | Pierre-Yves Schobbens, Jean-François Raskin, Thomas A. Henzinger: Axioms for real-time logics. Theor. Comput. Sci. 274(1-2): 151-182 (2002) |
2001 | ||
115 | Thomas A. Henzinger, Christoph M. Kirsch: Embedded Software, First International Workshop, EMSOFT 2001, Tahoe City, CA, USA, October, 8-10, 2001, Proceedings Springer 2001 | |
114 | EE | Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala: Compositional Methods for Probabilistic Systems. CONCUR 2001: 351-365 |
113 | EE | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: Symbolic Algorithms for Infinite-State Games. CONCUR 2001: 536-550 |
112 | EE | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: The Control of Synchronous Systems, Part II. CONCUR 2001: 566-582 |
111 | EE | Luca de Alfaro, Thomas A. Henzinger: Interface Theories for Component-Based Design. EMSOFT 2001: 148-165 |
110 | EE | Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch: Giotto: A Time-Triggered Language for Embedded Programming. EMSOFT 2001: 166-184 |
109 | EE | Luca de Alfaro, Thomas A. Henzinger: Interface automata. ESEC / SIGSOFT FSE 2001: 109-120 |
108 | EE | Thomas A. Henzinger, Marius Minea, Vinayak S. Prabhu: Assume-Guarantee Reasoning for Hierarchical Hybrid Systems. HSCC 2001: 275-290 |
107 | EE | 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 |
106 | 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 | |
105 | Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch: Embedded Control Systems Development with Giotto. LCTES/OM 2001: 64-72 | |
104 | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: From Verification to Control: Dynamic Programs for Omega-Regular Objectives. LICS 2001: 279-290 | |
103 | EE | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: MCWEB: A Model-Checking Tool for Web Site Debugging. WWW Posters 2001 |
102 | EE | Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin: A Classification of Symbolic Transition Systems CoRR cs.LO/0101013: (2001) |
101 | 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) | |
100 | Rajeev Alur, Thomas A. Henzinger: Introduction. Inf. Comput. 164(2): 233 (2001) | |
2000 | ||
99 | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Detecting Errors Before Reaching Them. CAV 2000: 186-201 | |
98 | EE | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: The Control of Synchronous Systems. CONCUR 2000: 458-473 |
97 | EE | Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, Howard Wong-Toi: Beyond HYTECH: Hybrid Systems Analysis Using Interval Numerical Methods. HSCC 2000: 130-144 |
96 | EE | Thomas A. Henzinger, Jean-François Raskin: Robust Undecidability of Timed and Hybrid Systems. HSCC 2000: 145-159 |
95 | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. ICCAD 2000: 245-252 | |
94 | EE | Thomas A. Henzinger: Masaccio: A Formal Model for Embedded Components. IFIP TCS 2000: 549-563 |
93 | EE | Luca de Alfaro, Thomas A. Henzinger: Concurrent Omega-Regular Games. LICS 2000: 141-154 |
92 | Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, Jean-François Raskin: Abstract Interpretation of Game Properties. SAS 2000: 220-239 | |
91 | EE | Thomas A. Henzinger, Rupak Majumdar: A Classification of Symbolic Transition Systems. STACS 2000: 13-34 |
90 | EE | Thomas A. Henzinger, Rupak Majumdar: Symbolic Model Checking for Rectangular Hybrid Systems. TACAS 2000: 142-156 |
89 | EE | Thomas A. Henzinger, Sriram K. Rajamani: Fair Bisimulation. TACAS 2000: 299-314 |
88 | EE | Thomas A. Henzinger: Exploiting Design Structure in Model Checking. Electr. Notes Theor. Comput. Sci. 39(3): (2000) |
1999 | ||
87 | EE | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Assume-Guarantee Refinement Between Different Time Scales. CAV 1999: 208-221 |
86 | EE | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. CAV 1999: 301-315 |
85 | EE | Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar: Rectangular Hybrid Games. CONCUR 1999: 320-335 |
84 | EE | Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang: Automating Modular Verification. CONCUR 1999: 82-97 |
83 | EE | Thomas A. Henzinger, Xiaojun Liu, Shaz Qadeer, Sriram K. Rajamani: Formal specification and verification of a dataflow processor array. ICCAD 1999: 494-499 |
82 | Rajeev Alur, Thomas A. Henzinger: Introduction. Formal Methods in System Design 14(3): 235 (1999) | |
81 | Rajeev Alur, Thomas A. Henzinger: Introduction. Formal Methods in System Design 15(1): 5 (1999) | |
80 | Rajeev Alur, Thomas A. Henzinger: Reactive Modules. Formal Methods in System Design 15(1): 7-48 (1999) | |
79 | EE | 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) |
78 | EE | Thomas A. Henzinger, Peter W. Kopke: Discrete-Time Control for Rectangular Hybrid Automata. Theor. Comput. Sci. 221(1-2): 369-392 (1999) |
1998 | ||
77 | Thomas A. Henzinger, Shankar Sastry: Hybrid Systems: Computation and Control, First International Workshop, HSCC'98, Berkeley, California, USA, April 13-15, 1998, Proceedings Springer 1998 | |
76 | Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer: From Pre-historic to Post-modern Symbolic Model Checking. CAV 1998: 195-206 | |
75 | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani: You Assume, We Guarantee: Methodology and Case Studies. CAV 1998: 440-451 | |
74 | 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 | |
73 | EE | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi: Alternating Refinement Relations. CONCUR 1998: 163-178 |
72 | EE | Jean-François Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger: Axioms for Real-Time Logics. CONCUR 1998: 219-236 |
71 | EE | Thomas A. Henzinger: It's About Time: Real-Time Logics Reviewed. CONCUR 1998: 439-454 |
70 | EE | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran: An Assume-Guarantee Rule for Checking Simulation. FMCAD 1998: 421-432 |
69 | EE | Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman: Concurrent Reachability Games. FOCS 1998: 564-575 |
68 | EE | 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 |
67 | Thomas A. Henzinger, Vlad Rusu: Reachability Verification for Hybrid Automata. HSCC 1998: 190-204 | |
66 | EE | Thomas A. Henzinger: Model Checking Game Properties of Multi-agent Systems (Abstract). ICALP 1998: 543 |
65 | EE | Thomas A. Henzinger, Jean-François Raskin, Pierre-Yves Schobbens: The Regular Real-Time Languages. ICALP 1998: 580-591 |
64 | Thomas A. Henzinger: Computer-aided Verification of Embedded Systems. IFIP Congress: Fundamentals - Foundations of Computer Science 1998: 89-92 | |
63 | EE | Rajeev Alur, Thomas A. Henzinger, Sriram K. Rajamani: Symbolic Exploration of transition Hierarchies. TACAS 1998: 330-344 |
62 | EE | Rajeev Alur, Thomas A. Henzinger: Finitary Fairness. ACM Trans. Program. Lang. Syst. 20(6): 1171-1194 (1998) |
61 | 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) | |
1997 | ||
60 | 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 | |
59 | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HYTECH: A Model Checker for Hybrid Systems. CAV 1997: 460-463 | |
58 | EE | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-Time Temporal Logic. COMPOS 1997: 23-60 |
57 | Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani: Fair Simulation. CONCUR 1997: 273-287 | |
56 | Rajeev Alur, Thomas A. Henzinger: Modularity for Timed and Hybrid Systems. CONCUR 1997: 74-88 | |
55 | EE | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman: Alternating-time Temporal Logic. FOCS 1997: 100-109 |
54 | Vineet Gupta, Thomas A. Henzinger, Radha Jagadeesan: Robust Timed Automata. HART 1997: 331-345 | |
53 | Thomas A. Henzinger, Orna Kupferman: From Quantity to Quality. HART 1997: 48-62 | |
52 | Thomas A. Henzinger, Peter W. Kopke: Discrete-Time Control for Rectangular Hybrid Automata. ICALP 1997: 582-593 | |
51 | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: Computing Accumulated Delays in Real-time Systems. Formal Methods in System Design 11(2): 137-155 (1997) | |
50 | EE | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HYTECH: A Model Checker for Hybrid Systems. STTT 1(1-2): 110-122 (1997) |
49 | EE | Rajeev Alur, Thomas A. Henzinger: Real-Time System = Discrete System + Clock Variables. STTT 1(1-2): 86-109 (1997) |
1996 | ||
48 | Rajeev Alur, Thomas A. Henzinger, Eduardo D. Sontag: Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA Springer 1996 | |
47 | Rajeev Alur, Thomas A. Henzinger: Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings Springer 1996 | |
46 | Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi: A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. CONCUR 1996: 514-529 | |
45 | Thomas A. Henzinger, Peter W. Kopke: State Equivalences for Rectangular Hybrid Automata. CONCUR 1996: 530-545 | |
44 | Rajeev Alur, Thomas A. Henzinger: Reactive Modules. LICS 1996: 207-218 | |
43 | Thomas A. Henzinger: The Theory of Hybrid Automata. LICS 1996: 278-292 | |
42 | Thomas A. Henzinger: Some Myths About Formal Verification. ACM Comput. Surv. 28(4es): 119 (1996) | |
41 | EE | Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho: Automatic Symbolic Verification of Embedded Systems. IEEE Trans. Software Eng. 22(3): 181-201 (1996) |
40 | EE | Rajeev Alur, Tomás Feder, Thomas A. Henzinger: The Benefits of Relaxing Punctuality. J. ACM 43(1): 116-146 (1996) |
1995 | ||
39 | Rajeev Alur, Thomas A. Henzinger: Local Liveness for Compositional Modeling of Fair Reactive Systems. CAV 1995: 166-179 | |
38 | Thomas A. Henzinger, Pei-Hsin Ho: Algorithmic Analysis of Nonlinear Hybrid Systems. CAV 1995: 225-238 | |
37 | Monika Rauch Henzinger, Thomas A. Henzinger, Peter W. Kopke: Computing Simulations on Finite and Infinite Graphs. FOCS 1995: 453-462 | |
36 | Thomas A. Henzinger, Howard Wong-Toi: Using HyTech to Synthesize Control Parameters for a Steam Boiler. Formal Methods for Industrial Applications 1995: 265-282 | |
35 | Thomas A. Henzinger, Howard Wong-Toi: Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems. Hybrid Systems 1995: 377-388 | |
34 | Thomas A. Henzinger: Hybrid Automata with Finite Bisimulatioins. ICALP 1995: 324-335 | |
33 | Thomas A. Henzinger, Peter W. Kopke, Howard Wong-Toi: The Expressive Power of Clocks. ICALP 1995: 417-428 | |
32 | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: HyTech: The Next Generation. IEEE Real-Time Systems Symposium 1995: 56-65 | |
31 | EE | Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaiya: What's decidable about hybrid automata? STOC 1995: 373-382 |
30 | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi: A User Guide to HyTech. TACAS 1995: 41-71 | |
29 | EE | 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) |
1994 | ||
28 | Rajeev Alur, Limor Fix, Thomas A. Henzinger: A Determinizable Class of Timed Automata. CAV 1994: 1-13 | |
27 | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: The Observational Power of Clocks. CONCUR 1994: 162-177 | |
26 | Thomas A. Henzinger, Peter W. Kopke: Verification Methods for the Divergent Runs of Clock Systems. FTRTFT 1994: 351-372 | |
25 | Arjun Kapur, Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Prooving Safety Properties of Hybrid Systems. FTRTFT 1994: 431-454 | |
24 | Thomas A. Henzinger, Pei-Hsin Ho: A Note on Abstract Interpretation Strategies for Hybrid Automata. Hybrid Systems 1994: 252-264 | |
23 | Thomas A. Henzinger, Pei-Hsin Ho: HYTECH: The Cornell HYbrid TECHnology Tool. Hybrid Systems 1994: 265-293 | |
22 | Rajeev Alur, Thomas A. Henzinger: Finitary Fairness LICS 1994: 52-61 | |
21 | Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine: Symbolic Model Checking for Real-Time Systems Inf. Comput. 111(2): 193-244 (1994) | |
20 | Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Timed Transition Systems Inf. Comput. 112(2): 273-337 (1994) | |
19 | EE | Rajeev Alur, Thomas A. Henzinger: A Really Temporal Logic. J. ACM 41(1): 181-204 (1994) |
1993 | ||
18 | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger: Computing Accumulated Delays in Real-time Systems. CAV 1993: 181-193 | |
17 | Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho: Automatic Symbolic Verification of Embedded Systems. IEEE Real-Time Systems Symposium 1993: 2-11 | |
16 | EE | Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601 |
15 | Rajeev Alur, Thomas A. Henzinger: Real-Time Logics: Complexity and Expressiveness Inf. Comput. 104(1): 35-77 (1993) | |
1992 | ||
14 | Rajeev Alur, Thomas A. Henzinger: Back to the Future: Towards a Theory of Timed Regular Languages FOCS 1992: 177-186 | |
13 | 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 | |
12 | Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Towards Refining Temporal Specifications into Hybrid Systems. Hybrid Systems 1992: 60-76 | |
11 | Thomas A. Henzinger, Zohar Manna, Amir Pnueli: What Good Are Digital Clocks? ICALP 1992: 545-558 | |
10 | Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine: Symbolic Model Checking for Real-time Systems LICS 1992: 394-406 | |
9 | Thomas A. Henzinger: Sooner is Safer Than Later. Inf. Process. Lett. 43(3): 135-141 (1992) | |
1991 | ||
8 | Rajeev Alur, Tomás Feder, Thomas A. Henzinger: The Benefits of Relaxing Punctuality. PODC 1991: 139-152 | |
7 | Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Real-time Systems. POPL 1991: 353-366 | |
6 | Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Timed Transition Systems. REX Workshop 1991: 226-251 | |
5 | Rajeev Alur, Thomas A. Henzinger: Logics and Models of Real Time: A Survey. REX Workshop 1991: 74-106 | |
1990 | ||
4 | Rajeev Alur, Thomas A. Henzinger: Real-time Logics: Complexity and Expressiveness LICS 1990: 390-401 | |
3 | EE | Thomas A. Henzinger: Half-Order Modal Logic: How to Prove Real-Time Properties. PODC 1990: 281-296 |
1989 | ||
2 | Rajeev Alur, Thomas A. Henzinger: A Really Temporal Logic FOCS 1989: 164-169 | |
1985 | ||
1 | Thomas A. Henzinger, Hubert Hofbauer: PROOF-PAD: An Interactive Proof Generating System Using Natural Deduction. ÖGAI 1985: 173-184 |