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 prehistoric to postmodern 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