BLAST: Model Checking of Software

- Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovacs.
Valigator: A verification tool with bound and invariant generation.
*Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning*(LPAR), Lecture Notes in Computer Science 5330, Springer, 2008, pp. 333-342. - Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz.
Program analysis with dynamic change of precision.
*Proceedings of the 23rd International Conference on Automated Software Engineering*(ASE), ACM Press, 2008, pp. 29-38. - Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko,
and Ru-Gang Xu.
Proving non-termination.
*Proceedings of the 35th Annual Symposium on Principles of Programming Languages*(POPL), ACM Press, 2008, pp. 147-158. - Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
The software model checker Blast: Applications to software engineering.
*Software Tools for Technology Transfer*9:505-526, 2007. - Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz.
Configurable software verification:
Concretizing the convergence of model checking and program analysis.
*Proceedings of the 19th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 4590, Springer, 2007, pp. 509-523. - Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko.
Path invariants.
*Proceedings of the International Conference on Programming Language Design and Implementation*(PLDI), ACM Press, 2007, pp. 300-309. - Roman Manevich, John Field, Thomas A. Henzinger, Ganesan Ramalingam, and
Mooly Sagiv.
Abstract counterexample-based refinement for powerset domains.
In
*Program Analysis and Compilation: Theory and Practice*, Lecture Notes in Computer Science 4444, Springer, 2007, pp. 273-292. - Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko.
Invariant synthesis for combined theories.
*Proceedings of the Eighth International Conference on Verification, Model Checking, and Abstract Interpretation*(VMCAI), Lecture Notes in Computer Science 4349, Springer, 2007, pp. 378-394. - Bhargav Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya Nori, and
Sriram K. Rajamani.
Synergy: A new algorithm for property checking.
*Proceedings of the 14th Annual Symposium on Foundations of Software Engineering*(FSE), ACM Press, 2006, pp. 117-127. - Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz.
Lazy shape analysis.
*Proceedings of the 18th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 4144, Springer, 2006, pp. 532-546. - Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
Permissive interfaces.
*Proceedings of the 13th Annual Symposium on Foundations of Software Engineering*(FSE), ACM Press, 2005, pp. 31-40. - Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
Checking memory safety with Blast.
*Proceedings of the International Conference on Fundamental Approaches to Software Engineering*(FASE), Lecture Notes in Computer Science 3442, Springer, 2005, pp. 2-18. - Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
Race checking by context inference.
*Proceedings of the International Conference on Programming Language Design and Implementation*(PLDI), ACM Press, 2004, pp. 1-13. - Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and
Rupak Majumdar.
The Blast query language for software verification.
*Proceedings of the 11th International Static Analysis Symposium*(SAS), Lecture Notes in Computer Science 3148, Springer, 2004, pp. 2-18. - Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
An Eclipse plugin for model checking.
*Proceedings of the 12th International Workshop on Program Comprehension*(IWPC), IEEE Computer Society Press, 2004, pp. 251-257. - Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and
Rupak Majumdar.
Generating tests from counterexamples.
*Proceedings of the 26th Annual International Conference on Software Engineering*(ICSE), IEEE Computer Society Press, 2004, pp. 326-335. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan.
Abstractions from proofs.
*Proceedings of the 31st Annual Symposium on Principles of Programming Languages*(POPL), ACM Press, 2004, pp. 232-244. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and
Marco A.A. Sanvido.
Extreme model checking.
In
*Verification: Theory and Practice*, Lecture Notes in Computer Science 2772, Springer, 2004, pp. 332-358. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre.
Software verification with Blast.
*Proceedings of the Tenth International Workshop on Model Checking of Software*(SPIN), Lecture Notes in Computer Science 2648, Springer, 2003, pp. 235-239. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer.
Thread-modular abstraction refinement.
*Proceedings of the 15th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 2725, Springer, 2003, pp. 262-274. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula,
Gregoire Sutre, and Westley Weimer.
Temporal safety proofs for systems code.
*Proceedings of the 14th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 2404, Springer, 2002, pp. 526-538. - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre.
Lazy abstraction.
*Proceedings of the 29th Annual Symposium on Principles of Programming Languages*(POPL), ACM Press, 2002, pp. 58-70.

Computational Modeling in Biology

- Thomas A. Henzinger, Maria Mateescu, and Verena Wolf.
Sliding-window abstraction for infinite Markov chains.
*Proceedings of the 21st International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 5643, Springer, 2009, pp. 337-352. - Jasmin Fisher, Thomas A. Henzinger, Maria Mateescu, and Nir Piterman.
Bounded asynchrony: Concurrency for modeling cell-cell interactions.
*Proceedings of the First International Workshop on Formal Methods in Systems Biology*(FMSB), Lecture Notes in Computer Science 5054, Springer, 2008, pp. 17-32. - Jasmin Fisher and Thomas A. Henzinger.
Executable cell biology.
*Nature Biotechnology*25:1239-1249, 2007. - Jasmin Fisher and Thomas A. Henzinger.
Executable biology.
*Proceedings of the Winter Simulation Conference*(WSC), IEEE Computer Society Press, 2006, pp. 1675-1682. - Jasmin Fisher, Nir Piterman, Alex Hajnal, and Thomas A. Henzinger.
Predictive modeling of signaling crosstalk during C. elegans vulval
development.
*PLoS Computational Biology*3(5):e92, 2007. - Marc A. Schaub, Thomas A. Henzinger, and Jasmin Fisher.
Qualitative networks: A symbolic approach to analyze biological
signaling networks.
*BMC Systems Biology*1:4, 2007.

Games for Verification and Control

- Krishnendu Chatterjee and Thomas A. Henzinger.
A survey of stochastic omega-regular games.
*Journal of Computer and System Sciences*, to appear. - Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger.
A survey of stochastic games with limsup and liminf objectives.
*Proceedings of the 36th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 5556, Part II, Springer, 2009, pp. 1-15. - Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, and
Barbara Jobstmann.
Better quality in synthesis through quantitative objectives.
*Proceedings of the 21st International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 5643, Springer, 2009, pp. 140-156. - Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.
Termination criteria for solving concurrent safety and reachability games.
*Proceedings of the 20th Annual Symposium on Discrete Algorithms*(SODA), ACM Press, 2009, pp. 197-206. - Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen,
and Thomas A. Henzinger.
Alpaga: A tool for solving parity games with imperfect information.
*Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 5505, Springer, 2009, pp. 58-61. - Krishnendu Chatterjee and Thomas A. Henzinger.
Reduction of stochastic parity to stochastic mean-payoff games.
*Information Processing Letters*106:1-7, 2008. - Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger,
and Jean-Francois Raskin.
Algorithms for omega-regular games with imperfect information.
*Logical Methods in Computer Science*3, 2007. - Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman.
Concurrent reachability games.
*Theoretical Computer Science*386:188-217, 2007. - Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen,
Thomas A. Henzinger, and Sangram Raje.
Strategy construction for parity games with imperfect information.
*Proceedings of the 19th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 5201, Springer, 2008, pp. 325-339. - Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann.
Environment assumptions for synthesis.
*Proceedings of the 19th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 5201, Springer, 2008, pp. 147-161. - Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger.
Stochastic limit-average games are in EXPTIME.
*International Journal of Game Theory*37:219-234, 2008. - Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger.
Controller synthesis with budget constraints.
*Proceedings of the 11th International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 4981, Springer, 2008, pp. 72-86. - Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.
Strategy logic.
*Proceedings of the 18th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 4703, Springer, 2007, pp. 59-73. - Krishnendu Chatterjee and Thomas A. Henzinger.
Assume-guarantee synthesis.
*Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 4424, Springer, 2007, pp. 261-275. - Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.
Generalized parity games.
*Proceedings of the Tenth International Conference on Foundations of Software Science and Computation Structures*(FOSSACS), Lecture Notes in Computer Science 4423, Springer, 2007, pp. 153-167. - Thomas A. Henzinger.
Games, time, and probability:
Graph models for system design and analysis.
*Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science*(SOFSEM), Lecture Notes in Computer Science 4362, Springer, 2007, pp. 103-110. - Thomas A. Henzinger and Nir Piterman.
Solving games without determinization.
*Proceedings of the 15th International Conference on Computer Science Logic*(CSL), Lecture Notes in Computer Science 4207, Springer, 2006, pp. 395-410. - Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and
Jean-Francois Raskin.
Algorithms for omega-regular games with imperfect information.
*Logical Methods in Computer Science*3(3), 2007. A preliminary version appeared in the*Proceedings of the 15th International Conference on Computer Science Logic*(CSL), Lecture Notes in Computer Science 4207, Springer, 2006, pp. 287-302. - Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.
Strategy improvement for concurrent reachability games.
*Proceedings of the Third Annual Conference on Quantitative Evaluation of Systems*(QEST), IEEE Computer Society Press, 2006, pp. 291-300. - Krishnendu Chatterjee and Thomas A. Henzinger.
Strategy improvement for stochastic Rabin and Streett games.
*Proceedings of the 17th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 4137, Springer, 2006, pp. 375-389. - Krishnendu Chatterjee and Thomas A. Henzinger.
Finitary winning in omega-regular games.
*Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 3920, Springer, 2006, pp. 257-271. - Krishnendu Chatterjee and Thomas A. Henzinger.
Strategy improvement and randomized subexponential algorithms for stochastic parity games.
*Proceedings of the 23rd International Conference on Theoretical Aspects of Computer Science*(STACS), Lecture Notes in Computer Science 3884, Springer, 2006, pp. 512-523. - Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.
The complexity of quantitative concurrent parity games.
*Proceedings of the 17th Annual Symposium on Discrete Algorithms*(SODA), ACM Press, 2006, pp. 678-687. - Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.
The complexity of stochastic Rabin and Streett games.
*Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 3580, Springer, 2005, pp. 878-890. - Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski.
Mean-payoff parity games.
*Proceedings of the 20th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 2005, pp. 178-187. - Krishnendu Chatterjee and Thomas A. Henzinger.
Semiperfect-information games.
*Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science*(FSTTCS), Lecture Notes in Computer Science 3821, Springer, 2005, pp. 1-18. - Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski.
Games with secure equilibria.
*Theoretical Computer Science*365:67-82, 2006. A preliminary version appeared in the*Proceedings of the 19th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 2004, pp. 160-169. - Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.
Trading memory for randomness.
*Proceedings of the First Annual Conference on Quantitative Evaluation of Systems*(QEST), IEEE Computer Society Press, 2004, pp. 206-217. - Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger.
Quantitative stochastic parity games.
*Proceedings of the 15th Annual Symposium on Discrete Algorithms*(SODA), ACM Press, 2004, pp. 114-123. - Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger.
Simple stochastic parity games.
*Proceedings of the International Conference for Computer Science Logic*(CSL), Lecture Notes in Computer Science 2803, Springer, 2003, pp. 100-113. - Marcin Jurdzinski, Orna Kupferman, and Thomas A. Henzinger.
Trading probability for fairness.
*Proceedings of the International Conference for Computer Science Logic*(CSL), Lecture Notes in Computer Science 2471, Springer, 2002, pp. 292-305. - Thomas A. Henzinger, Sriram C. Krishnan, Orna Kupferman, and
Freddy Y.C. Mang.
Synthesis of uninitialized systems.
*Proceedings of the 29th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 2380, Springer, 2002, pp. 644-656. - Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang.
The control of synchronous systems, part II.
*Proceedings of the 12th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 2154, Springer, 2001, pp. 566-580. - Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang.
The control of synchronous systems.
*Proceedings of the 11th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1877, Springer, 2000, pp. 458-473. - Thomas A. Henzinger, Rupak Majumdar, Freddy Y.C. Mang, and
Jean-Francois Raskin.
Abstract interpretation of game properties.
*Proceedings of the Seventh International Static Analysis Symposium*(SAS), Lecture Notes in Computer Science 1824, Springer, 2000, pp. 220-239. - Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang.
Detecting errors before reaching them.
*Proceedings of the 12th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1855, Springer, 2000, pp. 186-201. - Luca de Alfaro and Thomas A. Henzinger.
Concurrent omega-regular games.
*Proceedings of the 15th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 2000, pp. 141-154. - Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang.
Automating modular verification.
*Proceedings of the Tenth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1664, Springer, 1999, pp. 82-97. - Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi.
Alternating refinement relations.
*Proceedings of the Ninth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1466, Springer, 1998, pp. 163-178. - Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman.
Alternating-time temporal logic.
*Journal of the ACM*49:672-713, 2002. Preliminary versions appeared in the*Proceedings of the 38th Annual Symposium on Foundations of Computer Science*(FOCS), IEEE Computer Society Press, 1997, pp. 100-109, and in*Compositionality: The Significant Difference*, Lecture Notes in Computer Science 1536, Springer, 1998, pp. 23-60. - Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman.
Concurrent reachability games.
*Proceedings of the 39th Annual Symposium on Foundations of Computer Science*(FOCS), IEEE Computer Society Press, 1998, pp. 564-575.

GIOTTO: Embedded Software Design

- Thomas A. Henzinger.
Two challenges in embedded systems design: Predictability and robustness.
*Philosophical Transactions of the Royal Society A*366:3727-3736, 2008. - Krishnendu Chatterjee, Arkadeb Ghosal, Thomas A. Henzinger,
Daniel Iercan, Christoph M. Kirsch, Claudio Pinello, and
Alberto Sangiovanni-Vincentelli.
Logical reliability of interacting real-time tasks.
*Proceedings of the International Conference on Design, Automation, and Test in Europe*(DATE), IEEE Press, 2008, pp. 909-914. - Arkadeb Ghosal, Thomas A. Henzinger, Daniel Iercan, Christoph M. Kirsch,
and Alberto Sangiovanni-Vincentelli.
A hierarchical coordination language for interacting real-time tasks.
*Proceedings of the Sixth Annual Conference on Embedded Software*(EMSOFT), ACM Press, 2006, pp. 132-141. - Thomas A. Henzinger, Christoph M. Kirsch, and Slobodan Matic.
Composable code generation for distributed Giotto.
*Proceedings of the International Conference on Languages, Compilers, and Tools for Embedded Systems*(LCTES), ACM Press, 2005, pp. 21-30. - Slobodan Matic and Thomas A. Henzinger.
Trading end-to-end latency for composability.
*Proceedings of the 26th Annual Real-Time Systems Symposium*(RTSS), IEEE Computer Society Press, 2005, pp. 99-110. - Christoph M. Kirsch, Marco A.A. Sanvido, and Thomas A. Henzinger.
A programmable microkernel for real-time systems.
*Proceedings of the First International Conference on Virtual Execution Environments*(VEE), ACM Press, 2005, pp. 35-45. - Thomas A. Henzinger and Christoph M. Kirsch.
A typed assembly language for real-time programs.
*Proceedings of the Fourth Annual Conference on Embedded Software*(EMSOFT), ACM Press, 2004, pp. 104-113. - Arkadeb Ghosal, Thomas A. Henzinger, Christoph M. Kirsch, and
Marco A.A. Sanvido.
Event-driven programming with logical execution times.
*Proceedings of the Seventh International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 2993, Springer, 2004, pp. 357-371. - Thomas A. Henzinger, Christoph M. Kirsch, and Slobodan Matic.
Schedule carrying code.
*Proceedings of the Third Annual Conference on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2855, Springer, 2003, pp. 241-256. - Thomas A. Henzinger, Christoph M. Kirsch, Marco A.A. Sanvido, and
Wolfgang Pree.
From control models to real-time code using Giotto.
*IEEE Control Systems Magazine*23(1):50-64, 2003. A preliminary report on this work appeared in C.M. Kirsch, M.A.A. Sanvido, T.A. Henzinger, and W. Pree, "A Giotto-based helicopter control system,"*Proceedings of the Second International Workshop on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2491, Springer, 2002, pp. 46-60. - Thomas A. Henzinger and Christoph M. Kirsch.
The Embedded Machine: Predictable, portable real-time code.
*ACM Transactions on Programming Languages and Systems*29(6), 2007. A preliminary version appeared in the*Proceedings of the International Conference on Programming Language Design and Implementation*(PLDI), ACM Press, 2002, pp. 315-326. - Thomas A. Henzinger, Christoph M. Kirsch, Rupak Majumdar, and
Slobodan Matic.
Time-safety checking for embedded programs.
*Proceedings of the Second International Workshop on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2491, Springer, 2002, pp. 76-92. - Benjamin Horowitz, Judith Liebman, Cedric Ma, T. John Koo,
Thomas A. Henzinger, Alberto Sangiovanni-Vincentelli, and Shankar Sastry.
Embedded software design and system integration for rotorcraft UAV using
platforms.
*Proceedings of the 15th IFAC World Congress on Automatic Control*, Elsevier, 2002. - Timothy Brown, Alessandro Pasetti, Wolfgang Pree, Thomas A. Henzinger,
and Christoph M. Kirsch.
A reusable and platform-independent framework for distributed control
systems.
*Proceedings of the 20th Annual Digital Avionics Systems Conference*(DASC), vol. 2, IEEE Press, 2001, pp. 1-11. - Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch.
Giotto: A time-triggered language for embedded programming.
*Proceedings of the IEEE*91:84-99, 2003. A preliminary version appeared in the*Proceedings of the First International Workshop on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2211, Springer, 2001, pp. 166-184. - Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch.
Embedded control systems development with Giotto.
*Proceedings of the International Conference on Languages, Compilers, and Tools for Embedded Systems*(LCTES), ACM Press, 2001, pp. 64-72. An extended version appeared in*Software-Enabled Control: Information Technology for Dynamical Systems*(T. Samad, G. Balas, eds.), IEEE Press and Wiley-Interscience, 2003, pp. 123-146.

HYTECH: Verification of Hybrid Automata

- Laurent Doyen, Thomas A. Henzinger, and Jean-Francois Raskin.
Automatic rectangular refinement of affine hybrid systems.
*Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems*(FORMATS), Lecture Notes in Computer Science 3829, Springer, 2005, pp. 144-161. - Thomas A. Henzinger, Joerg Preussig, and Howard Wong-Toi.
Some lessons from the HyTech experience.
*Proceedings of the 40th Annual Conference on Decision and Control*(CDC), IEEE Press, 2001, pp. 2887-2892. - Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, and
Howard Wong-Toi.
Beyond HyTech:
Hybrid systems analysis using interval numerical methods.
*Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 1790, Springer, 2000, pp. 130-144. - Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J.
Pappas.
Discrete abstractions of hybrid systems.
*Proceedings of the IEEE*88:971-984, 2000. - Thomas A. Henzinger and Rupak Majumdar.
Symbolic model checking for rectangular hybrid systems.
*Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 1785, Springer, 2000, pp. 142-156. - Thomas A. Henzinger, Benjamin Horowitz, and Rupak Majumdar.
Rectangular hybrid games.
*Proceedings of the Tenth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1664, Springer, 1999, pp. 320-335. - Thomas A. Henzinger and Vlad Rusu.
Reachability verification for hybrid automata.
*Proceedings of the First International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 1386, Springer, 1998, pp. 190-204. - Joerg Preussig, Stephan Kowalewski, Howard Wong-Toi, and
Thomas A. Henzinger.
An algorithm for the approximative analysis of rectangular automata.
*Proceedings of the Fifth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems*(FTRTFT), Lecture Notes in Computer Science 1486, Springer, 1998, pp. 228-240. - Thomas A. Henzinger and Peter W. Kopke.
Discrete-time control for rectangular hybrid automata.
*Theoretical Computer Science*221:369-392, 1999. A preliminary version appeared in the*Proceedings of the 24th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 1256, Springer, 1997, pp. 582-593. - Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
HyTech: A model checker for hybrid systems.
*Software Tools for Technology Transfer*1:110-122, 1997. A preliminary version appeared in the*Proceedings of the Ninth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1254, Springer, 1997, pp. 460-463. - Rajeev Alur, Thomas A. Henzinger, and Howard Wong-Toi.
Symbolic analysis of hybrid systems.
*Proceedings of the 36th Annual Conference on Decision and Control*(CDC), IEEE Press, 1997, pp. 702-707. - Thomas A. Henzinger.
The theory of hybrid automata.
*Proceedings of the 11th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 1996, pp. 278-292. An extended version appeared in*Verification of Digital and Hybrid Systems*(M.K. Inan, R.P. Kurshan, eds.), NATO ASI Series F: Computer and Systems Sciences, Vol. 170, Springer, 2000, pp. 265-292. - Thomas A. Henzinger and Peter W. Kopke.
State equivalences for rectangular hybrid automata.
*Proceedings of the Seventh International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1119, Springer, 1996, pp. 530-545. - Thomas A. Henzinger and Howard Wong-Toi.
Using HyTech to synthesize control parameters for a steam boiler.
In
*Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control*, Lecture Notes in Computer Science 1165, Springer, 1996, pp. 265-282. - Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya.
What's decidable about hybrid automata?
*Journal of Computer and System Sciences*57:94-124, 1998. A preliminary version appeared in the*Proceedings of the 27th Annual Symposium on Theory of Computing*(STOC), ACM Press, 1995, pp. 373-382. - Thomas A. Henzinger.
Hybrid automata with finite bisimulations.
*Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 944, Springer, 1995, pp. 324-335. - Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
Algorithmic analysis of nonlinear hybrid systems.
*IEEE Transactions on Automatic Control*43:540-554, 1998. Preliminary reports on this work appeared in T.A. Henzinger and P.-H. Ho, "Algorithmic analysis of nonlinear hybrid systems,"*Proceedings of the Seventh International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 939, Springer, 1995, pp. 225-238, and in T.A. Henzinger and H. Wong-Toi, "Linear phase-portrait approximations for nonlinear hybrid systems," in*Hybrid Systems III*, Lecture Notes in Computer Science 1066, Springer, 1996, pp. 377-388. - Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi,
HyTech: The next generation.
*Proceedings of the 16th Annual Real-Time Systems Symposium*(RTSS), IEEE Computer Society Press, 1995, pp. 56-65. - Thomas A. Henzinger and Pei-Hsin Ho.
A note on abstract-interpretation strategies for hybrid automata.
In
*Hybrid Systems II*, Lecture Notes in Computer Science 999, Springer, 1995, pp. 252-264. - Thomas A. Henzinger and Pei-Hsin Ho.
HyTech: The Cornell Hybrid Technology Tool.
In
*Hybrid Systems II*, Lecture Notes in Computer Science 999, Springer, 1995, pp. 265-294. - Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
A user guide to HyTech.
*Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 1019, Springer, 1995, pp. 41-71. - Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger,
Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and
Sergio Yovine.
The algorithmic analysis of hybrid systems.
*Theoretical Computer Science*138:3-34, 1995. A preliminary version appeared in the*Proceedings of the 11th International Conference on Analysis and Optimization of Systems: Discrete-Event Systems*(ICAOS), Lecture Notes in Control and Information Sciences 199, Springer, 1994, pp. 331-351. - Arjun Kapur, Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
Proving safety properties of hybrid systems.
*Proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems*(FTRTFT), Lecture Notes in Computer Science 863, Springer, 1994, pp. 431-454. - Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho.
Automatic symbolic verification of embedded systems.
*IEEE Transactions on Software Engineering*22:181-201, 1996. A preliminary version appeared in the*Proceedings of the 14th Annual Real-Time Systems Symposium*(RTSS), IEEE Computer Society Press, 1993, pp. 2-11. - Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho.
Hybrid automata: An algorithmic approach to the specification and
verification of hybrid systems.
In
*Hybrid Systems I*, Lecture Notes in Computer Science 736, Springer, 1993, pp. 209-229. - Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
Towards refining temporal specifications into hybrid systems.
In
*Hybrid Systems I*, Lecture Notes in Computer Science 736, Springer, 1993, pp. 60-76.

Interface-based Design

- Laurent Doyen, Thomas A. Henzinger, Barbara Jobstmann, and Tatjana
Petrov.
Interface theories with component reuse.
*Proceedings of the Eighth Annual Conference on Embedded Software*(EMSOFT), ACM Press, 2008, pp. 79-88. - Dirk Beyer, Thomas A. Henzinger, and Vasu Singh.
Algorithms for interface synthesis.
*Proceedings of the 19th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 4590, Springer, 2007, pp. 4-19. - Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, and Sanjit A. Seshia.
An application of web-service interfaces.
*Proceedings of the International Conference on Web Services*(ICWS), IEEE Computer Society Press, 2007, pp. 831-838. - Thomas A. Henzinger and Slobodan Matic.
An interface algebra for real-time components.
*Proceedings of the 12th Annual Real-Time and Embedded Technology and Applications Symposium*(RTAS), IEEE Computer Society Press, 2006, pp. 253-266. - Luca de Alfaro and Thomas A. Henzinger.
Interface-based design.
In
*Engineering Theories of Software-intensive Systems*(M. Broy, J. Gruenbauer, D. Harel, and C.A.R. Hoare, eds.), NATO Science Series: Mathematics, Physics, and Chemistry, Vol. 195, Springer, 2005, pp. 83-104. - Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger.
Web service interfaces.
*Proceedings of the 14th International Word-Wide Web Conference*(WWW), 2005, pp. 148-159. - Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger,
and Marielle Stoelinga.
Resource interfaces.
*Proceedings of the Third Annual Conference on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2855, Springer, 2003, pp. 117-133. - Luca de Alfaro, Thomas A. Henzinger, and Marielle Stoelinga.
Timed interfaces.
*Proceedings of the Second International Workshop on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2491, Springer, 2002, pp. 108-122. - Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger,
Marcin Jurdzinski, and Freddy Y.C. Mang.
Interface compatibility checking for software modules.
*Proceedings of the 14th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 2404, Springer, 2002, pp. 428-441. - Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and
Freddy Y.C. Mang.
Synchronous and bidirectional component interfaces.
*Proceedings of the 14th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 2404, Springer, 2002, pp. 414-427. - Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, and
Alberto Sangiovanni-Vincentelli.
Convertibility verification and converter synthesis:
Two faces of the same coin.
*Proceedings of the International Conference on Computer-Aided Design*(ICCAD), IEEE Computer Society Press, 2002, pp. 132-139. - Luca de Alfaro and Thomas A. Henzinger.
Interface theories for component-based design.
*Proceedings of the First International Workshop on Embedded Software*(EMSOFT), Lecture Notes in Computer Science 2211, Springer, 2001, pp. 148-165. - Luca de Alfaro and Thomas A. Henzinger.
Interface automata.
*Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering*(FSE), ACM Press, 2001, pp. 109-120.

Liveness of Reactive Systems

- Thomas A. Henzinger and Sriram K. Rajamani.
Fair bisimulation.
*Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 1785, Springer, 2000, pp. 299-314. - Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani.
Fair simulation.
*Information and Computation*173:64-81, 2002. A preliminary version appeared in the*Proceedings of the Ninth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1243, Springer, 1997, pp. 273-287. - Rajeev Alur and Thomas A. Henzinger.
Local liveness for compositional modeling of fair reactive systems.
*Proceedings of the Seventh International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 939, Springer, 1995, pp. 166-179. - Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi.
The expressive power of clocks.
*Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 944, Springer, 1995, pp. 417-428. - Rajeev Alur and Thomas A. Henzinger.
Finitary fairness.
*ACM Transactions on Programming Languages and Systems*20:1171-1194, 1998. A preliminary version appeared in the*Proceedings of the Ninth Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 1994, pp. 52-61. - Thomas A. Henzinger.
Sooner is safer than later.
*Information Processing Letters*43:135-141, 1992.

MOCHA: Assume-Guarantee Model Checking

- Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, Minsu Kang,
Christoph M. Kirsch, Rupak Majumdar, Freddy Y.C. Mang, Bow-Yaw Wang.
jMocha: A model-checking tool that exploits design structure.
*Proceedings of the 23rd Annual International Conference on Software Engineering*(ICSE), IEEE Computer Society Press, 2001, pp. 835-836. - Thomas A. Henzinger, Marius Minea, and Vinayak Prabhu.
Assume-guarantee reasoning for hierarchical hybrid systems.
*Proceedings of the Fourth International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 2034, Springer, 2001, pp. 275-290. - Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala.
Compositional methods for probabilistic systems.
*Proceedings of the 12th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 2154, Springer, 2001, pp. 351-365. - Thomas A. Henzinger.
Masaccio: A formal model for embedded components.
*Proceedings of the First IFIP International Conference on Theoretical Computer Science*(TCS), Lecture Notes in Computer Science 1872, Springer, 2000, pp. 549-563. - Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani.
Decomposing refinement proofs using assume-guarantee reasoning.
*Proceedings of the International Conference on Computer-Aided Design*(ICCAD), IEEE Computer Society Press, 2000, pp. 245-252. - Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani.
Verifying sequential consistency for multiprocessor memory protocols.
*Proceedings of the 11th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1633, Springer, 1999, pp. 301-315. - Thomas A. Henzinger, Xiaojun Liu, Shaz Qadeer, and Sriram K. Rajamani.
Formal specification and verification of a dataflow processor array.
*Proceedings of the International Conference on Computer-Aided Design*(ICCAD), IEEE Computer Society Press, 1999, pp. 494-499. - Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani.
Assume-guarantee refinement between different time scales.
*Proceedings of the 11th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1633, Springer, 1999, pp. 208-221. - Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran.
An assume-guarantee rule for checking simulation.
*ACM Transactions on Programming Languages and Systems*24:51-64, 2002. A preliminary version appeared in the*Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design*(FMCAD), Lecture Notes in Computer Science 1522, Springer, 1998, pp. 421-432. - Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani.
You assume, we guarantee: Methodology and case studies.
*Proceedings of the Tenth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1427, Springer, 1998, pp. 440-451. - Rajeev Alur, Thomas A. Henzinger, Freddy Y.C. Mang, Shaz Qadeer,
Sriram K. Rajamani, and Serdar Tasiran.
Mocha: Modularity in model checking.
*Proceedings of the Tenth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1427, Springer, 1998, pp. 521-525. - Rajeev Alur and Thomas A. Henzinger.
Modularity for timed and hybrid systems.
*Proceedings of the Eighth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1243, Springer, 1997, pp. 74-88. - Rajeev Alur and Thomas A. Henzinger.
Reactive modules.
*Formal Methods in System Design*15:7-48, 1999. A preliminary version appeared in the*Proceedings of the 11th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 1996, pp. 207-218.

Real Time: Logics and Automata

- Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak Prabhu.
Timed parity games: Complexity and robustness.
*Proceedings of the Sixth International Conference on Formal Modeling and Analysis of Timed Systems*(FORMATS), Lecture Notes in Computer Science 5215, Springer, 2008, pp. 124-140. - Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu.
Trading infinite memory for uniform randomness in timed games.
*Proceedings of the 11th International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 4981, Springer, 2008, pp. 87-100. - Thomas Brihaye, Thomas A. Henzinger, Vinayak Prabhu, and
Jean-Francois Raskin.
Minimum-time reachability in timed games.
*Proceedings of the 34th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 4596, Springer, 2007, pp. 825-837. - Thomas A. Henzinger and Vinayak Prabhu.
Timed alternating-time temporal logic.
*Proceedings of the Fourth International Conference on Formal Modeling and Analysis of Timed Systems*(FORMATS), Lecture Notes in Computer Science 4202, Springer, 2006, pp. 1-17. - Thomas A. Henzinger, Rupak Majumdar, and Vinayak Prabhu.
Quantifying similarities between timed systems.
*Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems*(FORMATS), Lecture Notes in Computer Science 3829, Springer, 2005, pp. 226-241. - Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar,
and Marielle Stoelinga.
The element of surprise in timed games.
*Proceedings of the 14th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 2761, Springer, 2003, pp. 144-158. - Franck Cassez, Thomas A. Henzinger, and Jean-Francois Raskin.
A comparison of control problems for timed and hybrid systems.
*Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 2289, Springer, 2002, pp. 134-148. - Thomas A. Henzinger and Jean-Francois Raskin.
Robust undecidability of timed and hybrid systems.
*Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control*(HSCC), Lecture Notes in Computer Science 1790, Springer, 2000, pp. 145-159. - Jean-Francois Raskin, Pierre-Yves Schobbens, and Thomas A. Henzinger.
Axioms for real-time logics.
*Theoretical Computer Science*274:151-182, 2002. A preliminary version appeared in the*Proceedings of the Ninth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1466, Springer, 1998, pp. 219-236. - Thomas A. Henzinger.
It's about time: Real-time logics reviewed.
*Proceedings of the Ninth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1466, Springer, 1998, pp. 439-454. - Thomas A. Henzinger, Jean-Francois Raskin, and Pierre-Yves Schobbens.
The regular real-time languages.
*Proceedings of the 25th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 1443, Springer, 1998, pp. 580-591. - Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan.
Robust timed automata.
*Proceedings of the International Workshop on Hybrid and Real-Time Systems*(HART), Lecture Notes in Computer Science 1201, Springer, 1997, pp. 331-345. - Thomas A. Henzinger and Orna Kupferman.
From quantity to quality.
*Proceedings of the International Workshop on Hybrid and Real-Time Systems*(HART), Lecture Notes in Computer Science 1201, Springer, 1997, pp. 48-62. - Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi.
A space-efficient on-the-fly algorithm for real-time model checking.
*Proceedings of the Seventh International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 1119, Springer, 1996, pp. 514-529. - Rajeev Alur, Limor Fix, and Thomas A. Henzinger.
Event-clock automata: A determinizable class of timed automata.
*Theoretical Computer Science*211:253-273, 1999. A preliminary version appeared in the*Proceedings of the Sixth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 818, Springer, 1994, pp. 1-13. - Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger.
The observational power of clocks.
*Proceedings of the Fifth International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 836, Springer, 1994, pp. 162-177. - Thomas A. Henzinger and Peter W. Kopke.
Verification methods for the divergent runs of clock systems.
*Proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems*(FTRTFT), Lecture Notes in Computer Science 863, Springer, 1994, pp. 351-372. - Rajeev Alur and Thomas A. Henzinger.
Real-time system = discrete system + clock variables.
*Software Tools for Technology Transfer*1:86-109, 1997. A preliminary version appeared in*Theories and Experiences for Real-Time System Development*(T. Rus, C. Rattray, eds.), AMAST Series in Computing, Vol. 2, World Scientific, 1994, pp. 1-29. - Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger.
Computing accumulated delays in real-time systems.
*Formal Methods in System Design*11:137-156, 1997. A preliminary version appeared in the*Proceedings of the Fifth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 697, Springer, 1993, pp. 181-193. - Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi.
Parametric real-time reasoning.
*Proceedings of the 25th Annual Symposium on Theory of Computing*(STOC), ACM Press, 1993, pp. 592-601. - Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
Symbolic model checking for real-time systems.
*Information and Computation*111:193-244, 1994. A preliminary version appeared in the*Proceedings of the Seventh Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 1992, pp. 394-406. - Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
What good are digital clocks?
*Proceedings of the 19th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 623, Springer, 1992, pp. 545-558. - Rajeev Alur and Thomas A. Henzinger.
Back to the future: Towards a theory of timed regular languages.
*Proceedings of the 33rd Annual Symposium on Foundations of Computer Science*(FOCS), IEEE Computer Society Press, 1992, pp. 177-186. - Rajeev Alur, Tomas Feder, and Thomas A. Henzinger.
The benefits of relaxing punctuality.
*Journal of the ACM*43:116-146, 1996. A preliminary version appeared in the*Proceedings of the Tenth Annual Symposium on Principles of Distributed Computing*(PODC), ACM Press, 1991, pp. 139-152. - Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
Temporal proof methodologies for timed transition systems.
*Information and Computation*112:273-337, 1994. Preliminary reports on this work appeared in T.A. Henzinger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for real-time systems,"*Proceedings of the 18th Annual Symposium on Principles of Programming Languages*(POPL), ACM Press, 1991, pp. 353-366, and in T.A. Henzinger, Z. Manna, and A. Pnueli, "Timed transition systems," in*Real Time: Theory in Practice*, Lecture Notes in Computer Science 600, Springer, 1992, pp. 226-251. - Rajeev Alur and Thomas A. Henzinger.
Logics and models of real time: A survey.
In
*Real Time: Theory in Practice*, Lecture Notes in Computer Science 600, Springer, 1992, pp. 74-106. - Thomas A. Henzinger.
*The Temporal Specification and Verification of Real-Time Systems.*Ph.D. Thesis, Technical Report STAN-CS-91-1380, Stanford University, August 1991, 272 pages. - Rajeev Alur and Thomas A. Henzinger.
Real-time logics: Complexity and expressiveness.
*Information and Computation*104:35-77, 1993. A preliminary version appeared in the*Proceedings of the Fifth Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 1990, pp. 390-401. - Thomas A. Henzinger.
Half-order modal logic: How to prove real-time properties.
*Proceedings of the Ninth Annual Symposium on Principles of Distributed Computing*(PODC), ACM Press, 1990, pp. 281-296. - Rajeev Alur and Thomas A. Henzinger.
A really temporal logic.
*Journal of the ACM*41:181-204, 1994. A preliminary version appeared in the*Proceedings of the 30th Annual Symposium on Foundations of Computer Science*(FOCS), IEEE Computer Society Press, 1989, pp. 164-169.

Symbolic Algorithms for System Analysis

- Krishnendu Chatterjee and Thomas A. Henzinger.
Value iteration.
In
*25 Years of Model Checking*, Lecture Notes in Computer Science 5000, Springer, 2008, pp. 107-138. - Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and
Jean-Francois Raskin.
Antichains: A New Algorithm for Checking Universality of Finite Automata.
*Proceedings of the 18th International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 4144, Springer, 2006, pp. 17-30. - Krishnendu Chatterjee, Luca de Alfaro, Marco Faella,
Thomas A. Henzinger, Rupak Majumdar, and Marielle Stoelinga.
Compositional quantitative reasoning.
*Proceedings of the Third Annual Conference on Quantitative Evaluation of Systems*(QEST), IEEE Computer Society Press, 2006, pp. 179-188. - Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger,
Orna Kupferman, and Rupak Majumdar.
Verifying quantitative properties using bound functions.
*Proceedings of the 13th International Conference on Correct Hardware Design and Verification Methods*(CHARME), Lecture Notes in Computer Science 3725, Springer, 2005, pp. 50-64. - Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, and
Rupak Majumdar.
Counterexample-guided planning.
*Proceedings of the 21st International Conference on Uncertainty in Artificial Intelligence*(UAI), AUAI Press, 2005, pp. 104-111. - Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar,
and Marielle Stoelinga.
Model checking discounted temporal properties.
*Theoretical Computer Science*345:139-170, 2005. A preliminary version appeared in the*Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 2988, Springer, 2004, pp. 77-92. - Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar.
Discounting the future in systems theory.
*Proceedings of the 30th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 2719, Springer, 2003, pp. 1022-1037. - Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
Counterexample-guided control.
*Proceedings of the 30th International Colloquium on Automata, Languages, and Programming*(ICALP), Lecture Notes in Computer Science 2719, Springer, 2003, pp. 886-902. - Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar.
From verification to control:
Dynamic programs for omega-regular objectives.
*Proceedings of the 16th Annual Symposium on Logic in Computer Science*(LICS), IEEE Computer Society Press, 2001, pp. 279-290. - Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar.
Symbolic algorithms for infinite-state games.
*Proceedings of the 12th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 2154, Springer, 2001, pp. 536-550. - Thomas A. Henzinger, Rupak Majumdar, and Jean-Francois Raskin.
A classification of symbolic transition systems.
*ACM Transactions on Computational Logic*6:1-32, 2005. A preliminary version appeared in the*Proceedings of the 17th International Conference on Theoretical Aspects of Computer Science*(STACS), Lecture Notes in Computer Science 1770, Springer, 2000, pp. 13-34. - Thomas A. Henzinger, Orna Kupferman, and Shaz Qadeer.
From
*pre*historic to*post*modern symbolic model checking.*Formal Methods in System Design*23:303-327, 2003. A preliminary version appeared in the*Proceedings of the Tenth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1427, Springer, 1998, pp. 195-206. - Rajeev Alur, Thomas A. Henzinger, and Sriram K. Rajamani.
Symbolic exploration of transition hierarchies.
*Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 1384, Springer, 1998, pp. 330-344. - Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and
Sriram K. Rajamani.
Partial-order reduction in symbolic state-space exploration.
*Formal Methods in System Design*18:97-116, 2001. A preliminary version appeared in the*Proceedings of the Ninth International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 1254, Springer, 1997, pp. 340-351. - Monika R. Henzinger, Thomas A. Henzinger, and Peter W. Kopke.
Computing simulations on finite and infinite graphs.
*Proceedings of the 36th Annual Symposium on Foundations of Computer Science*(FOCS), IEEE Computer Society Press, 1995, pp. 453-462.

Resource Provisioning in Clouds

- Thomas A. Henzinger, Vasu Singh, Thomas Wies, and Damien Zufferey.
Scheduling large jobs by abstraction refinement.
*EuroSYS*2011. - Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, and Damien Zufferey.
Static scheduling in clouds.
*HotCloud*2011. - Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, and Damien Zufferey.
A Marketplace for cloud resources.
*Proceedings of the Tenth Annual Conference on Embedded Software*(EMSOFT), ACM Press, 2010. - Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, and Damien Zufferey.
FlexPRICE: Flexible provisioning of resources in a cloud
environment.
*IEEE Conference on Cloud Computing*, (IEEE Cloud), 2010.

Transactional Memories

- Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh.
Software transactional memory on relaxed memory models.
*Proceedings of the 21st International Conference on Computer-Aided Verification*(CAV), Lecture Notes in Computer Science 5643, Springer, 2009, pp. 321-336. - Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, and
Vasu Singh.
Model checking transactional memories.
*Proceedings of the International Conference on Programming Language Design and Implementation*(PLDI), ACM Press, 2008, pp. 372-382. - Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh.
Completeness and nondeterminism in model checking transactional
memories.
*Proceedings of the 19th International Conference on Concurrency Theory*(CONCUR), Lecture Notes in Computer Science 5201, Springer, 2008, pp. 21-35. - Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh.
Permissiveness in transactional memories.
*Proceedings of the 22nd International Symposium on Distributed Computing*(DISC), Lecture Notes in Computer Science 5218, Springer, 2008, pp. 305-319.

Miscellaneous

- Krishnendu Chatterjee, Koushik Sen, and Thomas A. Henzinger.
Model checking omega-regular properties of interval Markov chains.
*Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures*(FOSSACS), Lecture Notes in Computer Science 4962, Springer, 2008, pp. 302-317. - Laurent Doyen, Thomas A. Henzinger, and Jean-Francois Raskin.
Equivalence of labeled Markov chains.
*International Journal of Foundations of Computer Science*19:549-563, 2008. - Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger.
Quantitative languages.
*Proceedings of the 17th International Conference on Computer Science Logic*(CSL), Lecture Notes in Computer Science 5213, Springer, 2008, pp. 385-400. - Thomas A. Henzinger.
Quantitative generalizations of languages.
*Proceedings of the 11th International Conference on Developments in Language Theory*(DLT), Lecture Notes in Computer Science 4588, Springer, 2007, pp. 20-22. - Thomas A. Henzinger and Joseph Sifakis.
The discipline of embedded systems design.
*IEEE Computer*40(10):36-44, 2007. - Thomas A. Henzinger and Joseph Sifakis.
The embedded systems design challenge.
*Proceedings of the 14th International Symposium on Formal Methods*(FM), Lecture Notes in Computer Science 4085, Springer, 2006, pp. 1-15. - Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger.
Markov decision processes with multiple objectives.
*Proceedings of the 23rd International Conference on Theoretical Aspects of Computer Science*(STACS), Lecture Notes in Computer Science 3884, Springer, 2006, pp. 325-336. - Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar.
On the universal and existential fragments of the mu-calculus.
*Theoretical Computer Science*354:173-186, 2006. A preliminary version appeared in the*Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems*(TACAS), Lecture Notes in Computer Science 2619, Springer, 2003, pp. 49-64. - Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao,
Thomas A. Henzinger, and Jens Palsberg.
Stack size analysis for interrupt-driven programs.
*Information and Computation*194:144-174, 2004. A preliminary version appeared in the*Proceedings of the Tenth International Static Analysis Symposium*(SAS), Lecture Notes in Computer Science 2694, Springer, 2003, pp. 109-126. - Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang.
McWeb: A model-checking tool for web-site debugging.
*Poster Proceedings of the Tenth International Word-Wide Web Conference*(WWW), 2001, pp. 86-87.

*Last updated in November 2009*