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 |