<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Race checking by context inference </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Programming Language Design and Implementation </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Dirk Beyer , Adam J. Chlipala , Thomas A. Henzinger , Ranjit Jhala , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Generating tests from counterexamples </TI>
<DE> . </DE>
<JN> Proceedings of the 26th Annual International Conference on Software Engineering </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Arkadeb Ghosal , Thomas A. Henzinger , Christoph M. Kirsch , and Marco A. A. Sanvido </AU>
<DE> . </DE>
<TI> Event - driven programming with logical execution times </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> , </DE>
<PP> pp . 357 - 371 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Marco Faella , Thomas A. Henzinger , Rupak Majumdar , and Marielle Stoelinga </AU>
<DE> . </DE>
<TI> Model checking discounted temporal properties </TI>
<DE> . </DE>
<JN> Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> , </DE>
<PP> pp . 77 - 92 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Ken McMillan </AU>
<DE> . </DE>
<TI> Abstractions from proofs </TI>
<DE> . </DE>
<JN> Proceedings of the 31st Annual Symposium on Principles of Programming Languages </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> , </DE>
<PP> pp . 232 - 244 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Marco A. A. Sanvido </AU>
<DE> . </DE>
<TI> Extreme model checking </TI>
<DE> . </DE>
<JN> In Verification : Theory and Practice , Lecture Notes in Computer Science 2772 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2004 </DA>
<DE> , </DE>
<PP> pp . 332 - 358 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Krishnendu Chatterjee , Marcin Jurdzinski , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Quantitative stochastic parity games </TI>
<DE> . </DE>
<JN> Proceedings of the 15th Annual Symposium on Discrete Algorithms </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<DA> 2004 </DA>
<DE> , </DE>
<PP> pp . 114 - 123 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Christoph M. Kirsch , and Slobodan Matic </AU>
<DE> . </DE>
<TI> Schedule carrying code </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Conference on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 241 - 256 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , and Marielle Stoelinga </AU>
<DE> . </DE>
<TI> Resource interfaces </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Conference on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 117 - 133 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Krishnendu Chatterjee , Marcin Jurdzinski , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Simple stochastic parity games </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference for Computer Science Logic </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 100 - 113 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Marco Faella , Thomas A. Henzinger , Rupak Majumdar , and Marielle Stoelinga </AU>
<DE> . </DE>
<TI> The element of surprise in timed games </TI>
<DE> . </DE>
<JN> Proceedings of the 14th International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 144 - 158 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Shaz Qadeer </AU>
<DE> . </DE>
<TI> Thread - modular abstraction refinement </TI>
<DE> . </DE>
<JN> Proceedings of the 15th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 262 - 274 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Counterexample - guided control </TI>
<DE> . </DE>
<JN> Proceedings of the 30th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 886 - 902 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Discounting the future in systems theory </TI>
<DE> . </DE>
<JN> Proceedings of the 30th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 1022 - 1037 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Krishnendu Chatterjee , Di Ma , Rupak Majumdar , Tian Zhao , Thomas A. Henzinger , and Jens Palsberg </AU>
<DE> . </DE>
<TI> Stack size analysis for interrupt - driven programs </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Static Analysis Symposium </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 109 - 126 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Gregoire Sutre </AU>
<DE> . </DE>
<TI> Software verification with Blast </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Workshop on Model Checking of Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 235 - 239 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> Embedded control systems development with Giotto </TI>
<DE> . </DE>
<JN> In Software - Enabled Control : Information Technology for Dynamical Systems </JN>
<DE> ( </DE>
<AU> T. Samad , G. Balas </AU>
<DE> , </DE>
<NG> eds </NG>
<DE> . </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Press and Wiley - Interscience </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 123 - 146 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> Giotto : A time - triggered language for embedded programming </TI>
<DE> . </DE>
<JN> Proceedings of the IEEE </JN>
<VO> 91 </VO>
<DE> : </DE>
<PP> 84 - 99 </PP>
<DE> , </DE>
<DA> 2003 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Christoph M. Kirsch , Marco A. A. Sanvido , and Wolfgang Pree </AU>
<DE> . </DE>
<TI> From control models to real - time code using Giotto </TI>
<DE> . </DE>
<JN> IEEE Control Systems Magazine </JN>
<VO> 23 ( 1 </VO>
<DE> ) </DE>
<DE> : </DE>
<PP> 50 - 64 </PP>
<DE> , </DE>
<DA> 2003 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> On the universal and existential fragments of the mu - calculus </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2003 </DA>
<DE> , </DE>
<PP> pp . 49 - 64 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Shaz Qadeer </AU>
<DE> . </DE>
<TI> From pre historic to post modern symbolic model checking </TI>
<DE> . </DE>
<JN> Formal Methods in System Design </JN>
<VO> 23 </VO>
<DE> : </DE>
<PP> 303 - 327 </PP>
<DE> , </DE>
<DA> 2003 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Orna Kupferman </AU>
<DE> . </DE>
<TI> Alternating - time temporal logic </TI>
<DE> . </DE>
<JN> Journal of the ACM </JN>
<VO> 49 </VO>
<DE> : </DE>
<PP> 672 - 713 </PP>
<DE> , </DE>
<DA> 2002 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Franck Cassez , Thomas A. Henzinger , and J. - F. Raskin </AU>
<DE> . </DE>
<TI> A comparison of control problems for timed and hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Fifth International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 134 - 148 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , Marcin Jurdzinski , and Freddy Y. C. Mang </AU>
<DE> . </DE>
<TI> Interface compatibility checking for software modules </TI>
<DE> . </DE>
<JN> Proceedings of the 14th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 428 - 441 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , and Freddy Y. C. Mang </AU>
<DE> . </DE>
<TI> Synchronous and bidirectional component interfaces </TI>
<DE> . </DE>
<JN> Proceedings of the 14th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 414 - 427 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Marielle Stoelinga </AU>
<DE> . </DE>
<TI> Timed interfaces </TI>
<DE> . </DE>
<JN> Proceedings of the Second International Workshop on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 108 - 122 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Gregoire Sutre , and Westley Weimer </AU>
<DE> . </DE>
<TI> Temporal safety proofs for systems code </TI>
<DE> . </DE>
<JN> Proceedings of the 14th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 526 - 538 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Gregoire Sutre </AU>
<DE> . </DE>
<TI> Lazy abstraction </TI>
<DE> . </DE>
<JN> Proceedings of the 29th Annual Symposium on Principles of Programming Languages </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 58 - 70 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> The Embedded Machine : Predictable , portable real - time code </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Programming Language Design and Implementation </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 315 - 326 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Christoph M. Kirsch , Rupak Majumdar , and Slobodan Matic </AU>
<DE> . </DE>
<TI> Time - safety checking for embedded programs </TI>
<DE> . </DE>
<JN> Proceedings of the Second International Workshop on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 76 - 92 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Sriram C. Krishnan , Orna Kupferman , and Freddy Y. C. Mang </AU>
<DE> . </DE>
<TI> Synthesis of uninitialized systems </TI>
<DE> . </DE>
<JN> Proceedings of the 29th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 644 - 656 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Fair simulation </TI>
<DE> . </DE>
<JN> Information and Computation </JN>
<VO> 173 </VO>
<DE> : </DE>
<PP> 64 - 81 </PP>
<DE> , </DE>
<DA> 2002 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani , and Serdar Tasiran </AU>
<DE> . </DE>
<TI> An assume - guarantee rule for checking simulation </TI>
<DE> . </DE>
<JN> ACM Transactions on Programming Languages and Systems </JN>
<VO> 24 </VO>
<DE> : </DE>
<PP> 51 - 64 </PP>
<DE> , </DE>
<DA> 2002 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Benjamin Horowitz , Judith Liebman , Cedric Ma , T. John Koo , Thomas A. Henzinger , Alberto Sangiovanni - Vincentelli , and Shankar Sastry </AU>
<DE> . </DE>
<TI> Embedded software design and system integration for rotorcraft UAV using platforms </TI>
<DE> . </DE>
<JN> Proceedings of the 15th IFAC World Congress on Automatic Control </JN>
<DE> , </DE>
<PU> Elsevier </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Marcin Jurdzinski , Orna Kupferman , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Trading probability for fairness </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference for Computer Science Logic </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 292 - 305 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Christoph M. Kirsch , Marco A. A. Sanvido , Thomas A. Henzinger , and Wolfgang Pree </AU>
<DE> . </DE>
<TI> A Giotto - based helicopter control system </TI>
<DE> . </DE>
<JN> Proceedings of the Second International Workshop on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 46 - 60 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Roberto Passerone , Luca de Alfaro , Thomas A. Henzinger , and Alberto Sangiovanni - Vincentelli </AU>
<DE> . </DE>
<TI> Convertibility verification and converter synthesis : Two faces of the same coin </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Computer - Aided Design </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2002 </DA>
<DE> , </DE>
<PP> pp . 132 - 139 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> J. - F. Raskin , P. - Y. Schobbens , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Axioms for real - time logics </TI>
<DE> . </DE>
<JN> Theoretical Computer Science </JN>
<VO> 274 </VO>
<DE> : </DE>
<PP> 151 - 182 </PP>
<DE> , </DE>
<DA> 2002 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Robert K. Brayton , Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Partial - order reduction in symbolic state - space exploration </TI>
<DE> . </DE>
<JN> Formal Methods in System Design </JN>
<VO> 18 </VO>
<DE> : </DE>
<PP> 97 - 116 </PP>
<DE> , </DE>
<DA> 2001 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Luca de Alfaro , Radu Grosu , Thomas A. Henzinger , Minsu Kang , Christoph M. Kirsch , Rupak Majumdar , F. Y. C. Mang , Bow - Yaw Wang </AU>
<DE> . </DE>
<TI> jMocha : A model - checking tool that exploits design structure </TI>
<DE> . </DE>
<JN> Proceedings of the 23rd Annual International Conference on Software Engineering </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 835 - 836 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Timothy Brown , Alessandro Pasetti , Wolfgang Pree , Thomas A. Henzinger , and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> A reusable and platform - independent framework for distributed control systems </TI>
<DE> . </DE>
<JN> Proceedings of the 20th Annual Digital Avionics Systems Conference </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<VO> vol . 2 </VO>
<DE> , </DE>
<PU> IEEE Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 1 - 11 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Interface automata </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 109 - 120 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Interface theories for component - based design </TI>
<DE> . </DE>
<JN> Proceedings of the First International Workshop on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 148 - 165 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Ranjit Jhala </AU>
<DE> . </DE>
<TI> Compositional methods for probabilistic systems </TI>
<DE> . </DE>
<JN> Proceedings of the 12th International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 351 - 365 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> From verification to control : Dynamic programs for omega - regular objectives </TI>
<DE> . </DE>
<JN> Proceedings of the 16th Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 279 - 290 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Symbolic algorithms for infinite - state games </TI>
<DE> . </DE>
<JN> Proceedings of the 12th International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 536 - 550 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and F. Y. C. Mang </AU>
<DE> . </DE>
<TI> The control of synchronous systems , part II </TI>
<DE> . </DE>
<JN> Proceedings of the 12th International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 566 - 580 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and F. Y. C. Mang </AU>
<DE> . </DE>
<TI> McWeb : A model - checking tool for web - site debugging </TI>
<DE> . </DE>
<JN> Poster Proceedings of the Tenth International Word - Wide Web Conference </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 86 - 87 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> Giotto : A time - triggered language for embedded programming </TI>
<DE> . </DE>
<JN> Proceedings of the First International Workshop on Embedded Software </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 166 - 184 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , and Christoph M. Kirsch </AU>
<DE> . </DE>
<TI> Embedded control systems development with Giotto </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Languages , Compilers , and Tools for Embedded Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 64 - 72 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Marius Minea , and Vinayak Prabhu </AU>
<DE> . </DE>
<TI> Assume - guarantee reasoning for hierarchical hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Fourth International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 275 - 290 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Joerg Preussig , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Some lessons from the HyTech experience </TI>
<DE> . </DE>
<JN> Proceedings of the 40th Annual Conference on Decision and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Press </PU>
<DE> , </DE>
<DA> 2001 </DA>
<DE> , </DE>
<PP> pp . 2887 - 2892 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , Gerardo Lafferriere , and George J. Pappas </AU>
<DE> . </DE>
<TI> Discrete abstractions of hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the IEEE </JN>
<VO> 88 </VO>
<DE> : </DE>
<PP> 971 - 984 </PP>
<DE> , </DE>
<DA> 2000 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Concurrent omega - regular games </TI>
<DE> . </DE>
<JN> Proceedings of the 15th Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 141 - 154 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and F. Y. C. Mang </AU>
<DE> . </DE>
<TI> Detecting errors before reaching them </TI>
<DE> . </DE>
<JN> Proceedings of the 12th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 186 - 201 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and F. Y. C. Mang </AU>
<DE> . </DE>
<TI> The control of synchronous systems </TI>
<DE> . </DE>
<JN> Proceedings of the 11th International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 458 - 473 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Masaccio : A formal model for embedded components </TI>
<DE> . </DE>
<JN> Proceedings of the First IFIP International Conference on Theoretical Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 549 - 563 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The theory of hybrid automata </TI>
<DE> . </DE>
<JN> In Verification of Digital and Hybrid Systems </JN>
<DE> ( </DE>
<AU> M. K. Inan , R. P. Kurshan </AU>
<DE> , </DE>
<NG> eds </NG>
<DE> . </DE>
<DE> ) </DE>
<DE> , </DE>
<JN> NATO ASI Series F : Computer and Systems Sciences </JN>
<DE> , </DE>
<VO> Vol . 170 </VO>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 265 - 292 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , Rupak Majumdar , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Beyond HyTech : Hybrid systems analysis using interval numerical methods </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 130 - 144 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Rupak Majumdar </AU>
<DE> . </DE>
<TI> A classification of symbolic transition systems </TI>
<DE> . </DE>
<JN> Proceedings of the 17th International Conference on Theoretical Aspects of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 13 - 34 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Symbolic model checking for rectangular hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 142 - 156 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Rupak Majumdar , F. Y. C. Mang , and J. - F. Raskin </AU>
<DE> . </DE>
<TI> Abstract interpretation of game properties </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Static Analysis Symposium </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 220 - 239 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Decomposing refinement proofs using assume - guarantee reasoning </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Computer - Aided Design </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 245 - 252 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Fair bisimulation </TI>
<DE> . </DE>
<JN> Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 299 - 314 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and J. - F. Raskin </AU>
<DE> . </DE>
<TI> Robust undecidability of timed and hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 2000 </DA>
<DE> , </DE>
<PP> pp . 145 - 159 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Reactive modules </TI>
<DE> . </DE>
<JN> Formal Methods in System Design </JN>
<VO> 15 </VO>
<DE> : </DE>
<PP> 7 - 48 </PP>
<DE> , </DE>
<DA> 1999 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Luca de Alfaro , Thomas A. Henzinger , and F. Y. C. Mang </AU>
<DE> . </DE>
<TI> Automating modular verification </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1999 </DA>
<DE> , </DE>
<PP> pp . 82 - 97 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Limor Fix , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Event - clock automata : A determinizable class of timed automata </TI>
<DE> . </DE>
<JN> Theoretical Computer Science </JN>
<VO> 211 </VO>
<DE> : </DE>
<PP> 253 - 273 </PP>
<DE> , </DE>
<DA> 1999 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Benjamin Horowitz , and Rupak Majumdar </AU>
<DE> . </DE>
<TI> Rectangular hybrid games </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1999 </DA>
<DE> , </DE>
<PP> pp . 320 - 335 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Peter W. Kopke </AU>
<DE> . </DE>
<TI> Discrete - time control for rectangular hybrid automata </TI>
<DE> . </DE>
<JN> Theoretical Computer Science </JN>
<VO> 221 </VO>
<DE> : </DE>
<PP> 369 - 392 </PP>
<DE> , </DE>
<DA> 1999 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Xiaojun Liu , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Formal specification and verification of a dataflow processor array </TI>
<DE> . </DE>
<JN> Proceedings of the International Conference on Computer - Aided Design </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1999 </DA>
<DE> , </DE>
<PP> pp . 494 - 499 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Assume - guarantee refinement between different time scales </TI>
<DE> . </DE>
<JN> Proceedings of the 11th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1999 </DA>
<DE> , </DE>
<PP> pp . 208 - 221 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Verifying sequential consistency for multiprocessor memory protocols </TI>
<DE> . </DE>
<JN> Proceedings of the 11th International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1999 </DA>
<DE> , </DE>
<PP> pp . 301 - 315 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Finitary fairness </TI>
<DE> . </DE>
<JN> ACM Transactions on Programming Languages and Systems </JN>
<VO> 20 </VO>
<DE> : </DE>
<PP> 1171 - 1194 </PP>
<DE> , </DE>
<DA> 1998 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Orna Kupferman </AU>
<DE> . </DE>
<TI> Alternating - time temporal logic </TI>
<DE> . </DE>
<JN> In Compositionality : The Significant Difference </JN>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 23 - 60 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , Orna Kupferman , and Moshe Y. Vardi </AU>
<DE> . </DE>
<TI> Alternating refinement relations </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 163 - 178 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , F. Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , and Serdar Tasiran </AU>
<DE> . </DE>
<TI> Mocha : Modularity in model checking </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 521 - 525 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Symbolic exploration of transition hierarchies </TI>
<DE> . </DE>
<JN> Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 330 - 344 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Luca de Alfaro , Thomas A. Henzinger , and Orna Kupferman </AU>
<DE> . </DE>
<TI> Concurrent reachability games </TI>
<DE> . </DE>
<JN> Proceedings of the 39th Annual Symposium on Foundations of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 564 - 575 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> It 's about time : Real - time logics reviewed </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 439 - 454 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Pei - Hsin Ho , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Algorithmic analysis of nonlinear hybrid systems </TI>
<DE> . </DE>
<JN> IEEE Transactions on Automatic Control </JN>
<VO> 43 </VO>
<DE> : </DE>
<PP> 540 - 554 </PP>
<DE> , </DE>
<DA> 1998 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , and Pravin Varaiya </AU>
<DE> . </DE>
<TI> What 's decidable about hybrid automata </TI>
<DE> ? </DE>
<JN> Journal of Computer and System Sciences </JN>
<VO> 57 </VO>
<DE> : </DE>
<PP> 94 - - 124 </PP>
<DE> , </DE>
<DA> 1998 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Shaz Qadeer </AU>
<DE> . </DE>
<TI> From pre historic to post modern symbolic model checking </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 195 - 206 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> You assume , we guarantee : Methodology and case studies </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 440 - 451 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani , and Serdar Tasiran </AU>
<DE> . </DE>
<TI> An assume - guarantee rule for checking simulation </TI>
<DE> . </DE>
<JN> Proceedings of the Second International Conference on Formal Methods in Computer - Aided Design </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 421 - 432 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , J. - F. Raskin , and P. - Y. Schobbens </AU>
<DE> . </DE>
<TI> The regular real - time languages </TI>
<DE> . </DE>
<JN> Proceedings of the 25th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 580 - 591 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Vlad Rusu </AU>
<DE> . </DE>
<TI> Reachability verification for hybrid automata </TI>
<DE> . </DE>
<JN> Proceedings of the First International Workshop on Hybrid Systems : Computation and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 190 - 204 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Joerg Preussig , Stephan Kowalewski , Howard Wong - Toi , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> An algorithm for the approximative analysis of rectangular automata </TI>
<DE> . </DE>
<JN> Proceedings of the Fifth International Symposium on Formal Techniques in Real - Time and Fault - Tolerant Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 228 - 240 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> J. - F. Raskin , P. - Y. Schobbens , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Axioms for real - time logics </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1998 </DA>
<DE> , </DE>
<PP> pp . 219 - 236 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Robert K. Brayton , Thomas A. Henzinger , Shaz Qadeer , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Partial - order reduction in symbolic state - space exploration </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 340 - 351 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Computing accumulated delays in real - time systems </TI>
<DE> . </DE>
<JN> Formal Methods in System Design </JN>
<VO> 11 </VO>
<DE> : </DE>
<PP> 137 - 156 </PP>
<DE> , </DE>
<DA> 1997 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Modularity for timed and hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Eighth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 74 - 88 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Real - time system = discrete system + clock variables </TI>
<DE> . </DE>
<JN> Software Tools for Technology Transfer </JN>
<VO> 1 </VO>
<DE> : </DE>
<PP> 86 - 109 </PP>
<DE> , </DE>
<DA> 1997 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Orna Kupferman </AU>
<DE> . </DE>
<TI> Alternating - time temporal logic </TI>
<DE> . </DE>
<JN> Proceedings of the 38th Annual Symposium on Foundations of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 100 - 109 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Symbolic analysis of hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the 36th Annual Conference on Decision and Control </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Press </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 702 - 707 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Vineet Gupta , Thomas A. Henzinger , and Radha Jagadeesan </AU>
<DE> . </DE>
<TI> Robust timed automata </TI>
<DE> . </DE>
<JN> Proceedings of the International Workshop on Hybrid and Real - Time Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 331 - 345 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Pei - Hsin Ho , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> HyTech : A model checker for hybrid systems </TI>
<DE> . </DE>
<JN> Software Tools for Technology Transfer </JN>
<VO> 1 </VO>
<DE> : </DE>
<PP> 110 - 122 </PP>
<DE> , </DE>
<DA> 1997 </DA>
<DE> . </DE>
<JN> A preliminary version appeared in the Proceedings of the Ninth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 460 - 463 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Peter W. Kopke </AU>
<DE> . </DE>
<TI> Discrete - time control for rectangular hybrid automata </TI>
<DE> . </DE>
<JN> Proceedings of the 24th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 582 - 593 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Orna Kupferman </AU>
<DE> . </DE>
<TI> From quantity to quality </TI>
<DE> . </DE>
<JN> Proceedings of the International Workshop on Hybrid and Real - Time Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 48 - 62 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Sriram K. Rajamani </AU>
<DE> . </DE>
<TI> Fair simulation </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1997 </DA>
<DE> , </DE>
<PP> pp . 273 - 287 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Tomas Feder , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The benefits of relaxing punctuality </TI>
<DE> . </DE>
<JN> Journal of the ACM </JN>
<VO> 43 </VO>
<DE> : </DE>
<PP> 116 - 146 </PP>
<DE> , </DE>
<DA> 1996 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Reactive modules </TI>
<DE> . </DE>
<JN> Proceedings of the 11th Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 207 - 218 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> Automatic symbolic verification of embedded systems </TI>
<DE> . </DE>
<JN> IEEE Transactions on Software Engineering </JN>
<VO> 22 </VO>
<DE> : </DE>
<PP> 181 - 201 </PP>
<DE> , </DE>
<DA> 1996 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The theory of hybrid automata </TI>
<DE> . </DE>
<JN> Proceedings of the 11th Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 278 - 292 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Peter W. Kopke </AU>
<DE> . </DE>
<TI> State equivalences for rectangular hybrid automata </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 530 - 545 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Orna Kupferman , and Moshe Y. Vardi </AU>
<DE> . </DE>
<TI> A space - efficient on - the - fly algorithm for real - time model checking </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 514 - 529 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Linear phase - portrait approximations for nonlinear hybrid systems </TI>
<DE> . </DE>
<JN> In Hybrid Systems III , Lecture Notes in Computer Science 1066 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 377 - 388 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> Using HyTech to synthesize control parameters for a steam boiler </TI>
<DE> . </DE>
<JN> In Formal Methods for Industrial Applications : Specifying and Programming the Steam Boiler Control , Lecture Notes in Computer Science 1165 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1996 </DA>
<DE> , </DE>
<PP> pp . 265 - 282 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , Nicolas Halbwachs , Thomas A. Henzinger , Pei - Hsin Ho , Xavier Nicollin , Alfredo Olivero , Joseph Sifakis , and Sergio Yovine </AU>
<DE> . </DE>
<TI> The algorithmic analysis of hybrid systems </TI>
<DE> . </DE>
<JN> Theoretical Computer Science </JN>
<VO> 138 </VO>
<DE> : </DE>
<PP> 3 - 34 </PP>
<DE> , </DE>
<DA> 1995 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Local liveness for compositional modeling of fair reactive systems </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 166 - 179 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Hybrid automata with finite bisimulations </TI>
<DE> . </DE>
<JN> Proceedings of the 22nd International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 324 - 335 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Monika R. Henzinger , Thomas A. Henzinger , and Peter W. Kopke </AU>
<DE> . </DE>
<TI> Computing simulations on finite and infinite graphs </TI>
<DE> . </DE>
<JN> Proceedings of the 36th Annual Symposium on Foundations of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 453 - 462 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> Algorithmic analysis of nonlinear hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 225 - 238 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> A note on abstract - interpretation strategies for hybrid automata </TI>
<DE> . </DE>
<JN> In Hybrid Systems II , Lecture Notes in Computer Science 999 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 252 - 264 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> HyTech : The Cornell Hybrid Technology Tool </TI>
<DE> . </DE>
<JN> In Hybrid Systems II , Lecture Notes in Computer Science 999 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 265 - 294 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Pei - Hsin Ho , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> A user guide to HyTech </TI>
<DE> . </DE>
<JN> Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 41 - 71 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Pei - Hsin Ho , and Howard Wong - Toi </AU>
<DE> , </DE>
<TI> HyTech : The next generation </TI>
<DE> . </DE>
<JN> Proceedings of the 16th Annual Real - Time Systems Symposium </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 56 - 65 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , and Pravin Varaiya </AU>
<DE> . </DE>
<TI> What 's decidable about hybrid automata </TI>
<DE> ? </DE>
<JN> Proceedings of the 27th Annual Symposium on Theory of Computing </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 373 - 382 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Peter W. Kopke , and Howard Wong - Toi </AU>
<DE> . </DE>
<TI> The expressive power of clocks </TI>
<DE> . </DE>
<JN> Proceedings of the 22nd International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1995 </DA>
<DE> , </DE>
<PP> pp . 417 - 428 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The observational power of clocks </TI>
<DE> . </DE>
<JN> Proceedings of the Fifth International Conference on Concurrency Theory </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 162 - 177 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei - Hsin Ho , Xavier Nicollin , Alfredo Olivero , Joseph Sifakis , and Sergio Yovine </AU>
<DE> . </DE>
<TI> The algorithmic analysis of hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the 11th International Conference on Analysis and Optimization of Systems : Discrete - Event Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 331 - 351 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Limor Fix , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> A determinizable class of timed automata </TI>
<DE> . </DE>
<JN> Proceedings of the Sixth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 1 - 13 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> A really temporal logic </TI>
<DE> . </DE>
<JN> Journal of the ACM </JN>
<VO> 41 </VO>
<DE> : </DE>
<PP> 181 - 204 </PP>
<DE> , </DE>
<DA> 1994 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Finitary fairness </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 52 - 61 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Real - time system = discrete system + clock variables </TI>
<DE> . </DE>
<JN> In Theories and Experiences for Real - Time System Development </JN>
<DE> ( </DE>
<AU> T. Rus , C. Rattray </AU>
<DE> , </DE>
<NG> eds </NG>
<DE> . </DE>
<DE> ) </DE>
<DE> , </DE>
<TI> AMAST Series in Computing </TI>
<DE> , </DE>
<VO> Vol . 2 </VO>
<DE> , </DE>
<PU> World Scientific </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 1 - 29 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger and Peter W. Kopke </AU>
<DE> . </DE>
<TI> Verification methods for the divergent runs of clock systems </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Symposium on Formal Techniques in Real - Time and Fault - Tolerant Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 351 - 372 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> Temporal proof methodologies for timed transition systems </TI>
<DE> . </DE>
<JN> Information and Computation </JN>
<VO> 112 </VO>
<DE> : </DE>
<PP> 273 - 337 </PP>
<DE> , </DE>
<DA> 1994 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , and Sergio Yovine </AU>
<DE> . </DE>
<TI> Symbolic model checking for real - time systems </TI>
<DE> . </DE>
<JN> Information and Computation </JN>
<VO> 111 </VO>
<DE> : </DE>
<PP> 193 - 244 </PP>
<DE> , </DE>
<DA> 1994 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Arjun Kapur , Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> Proving safety properties of hybrid systems </TI>
<DE> . </DE>
<JN> Proceedings of the Third International Symposium on Formal Techniques in Real - Time and Fault - Tolerant Systems </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1994 </DA>
<DE> , </DE>
<PP> pp . 431 - 454 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Computing accumulated delays in real - time systems </TI>
<DE> . </DE>
<JN> Proceedings of the Fifth International Conference on Computer - Aided Verification </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1993 </DA>
<DE> , </DE>
<PP> pp . 181 - 193 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> Hybrid automata : An algorithmic approach to the specification and verification of hybrid systems </TI>
<DE> . </DE>
<JN> In Hybrid Systems I , Lecture Notes in Computer Science 736 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1993 </DA>
<DE> , </DE>
<PP> pp . 209 - 229 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Real - time logics : Complexity and expressiveness </TI>
<DE> . </DE>
<JN> Information and Computation </JN>
<VO> 104 </VO>
<DE> : </DE>
<PP> 35 - 77 </PP>
<DE> , </DE>
<DA> 1993 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Pei - Hsin Ho </AU>
<DE> . </DE>
<TI> Automatic symbolic verification of embedded systems </TI>
<DE> . </DE>
<JN> Proceedings of the 14th Annual Real - Time Systems Symposium </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1993 </DA>
<DE> , </DE>
<PP> pp . 2 - 11 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Thomas A. Henzinger , and Moshe Y. Vardi </AU>
<DE> . </DE>
<TI> Parametric real - time reasoning </TI>
<DE> . </DE>
<JN> Proceedings of the 25th Annual Symposium on Theory of Computing </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 1993 </DA>
<DE> , </DE>
<PP> pp . 592 - 601 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> Towards refining temporal specifications into hybrid systems </TI>
<DE> . </DE>
<JN> In Hybrid Systems I , Lecture Notes in Computer Science 736 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1993 </DA>
<DE> , </DE>
<PP> pp . 60 - 76 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Back to the future : Towards a theory of timed regular languages </TI>
<DE> . </DE>
<JN> Proceedings of the 33rd Annual Symposium on Foundations of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1992 </DA>
<DE> , </DE>
<PP> pp . 177 - 186 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Logics and models of real time : A survey </TI>
<DE> . </DE>
<JN> In Real Time : Theory in Practice , Lecture Notes in Computer Science 600 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1992 </DA>
<DE> , </DE>
<PP> pp . 74 - 106 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Sooner is safer than later </TI>
<DE> . </DE>
<JN> Information Processing Letters </JN>
<VO> 43 </VO>
<DE> : </DE>
<PP> 135 - 141 </PP>
<DE> , </DE>
<DA> 1992 </DA>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> Timed transition systems </TI>
<DE> . </DE>
<JN> In Real Time : Theory in Practice , Lecture Notes in Computer Science 600 </JN>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1992 </DA>
<DE> , </DE>
<PP> pp . 226 - 251 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> What good are digital clocks </TI>
<DE> ? </DE>
<JN> Proceedings of the 19th International Colloquium on Automata , Languages , and Programming </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<DE> , </DE>
<PU> Springer - Verlag </PU>
<DE> , </DE>
<DA> 1992 </DA>
<DE> , </DE>
<PP> pp . 545 - 558 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , and Sergio Yovine </AU>
<DE> . </DE>
<TI> Symbolic model checking for real - time systems </TI>
<DE> . </DE>
<JN> Proceedings of the Seventh Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1992 </DA>
<DE> , </DE>
<PP> pp . 394 - 406 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur , Tomas Feder , and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The benefits of relaxing punctuality </TI>
<DE> . </DE>
<JN> Proceedings of the Tenth Annual Symposium on Principles of Distributed Computing </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 1991 </DA>
<DE> , </DE>
<PP> pp . 139 - 152 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> The Temporal Specification and Verification of Real - Time Systems </TI>
<DE> . </DE>
<JN> Ph . D. Thesis , Technical Report STAN - CS - 91 - 1380 </JN>
<DE> , </DE>
<OR> Stanford University </OR>
<DE> , </DE>
<DA> August 1991 </DA>
<DE> , </DE>
<PP> 272 pages </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger , Zohar Manna , and Amir Pnueli </AU>
<DE> . </DE>
<TI> Temporal proof methodologies for real - time systems </TI>
<DE> . </DE>
<JN> Proceedings of the 18th Annual Symposium on Principles of Programming Languages </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 1991 </DA>
<DE> , </DE>
<PP> pp . 353 - 366 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Real - time logics : Complexity and expressiveness </TI>
<DE> . </DE>
<JN> Proceedings of the Fifth Annual Symposium on Logic in Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1990 </DA>
<DE> , </DE>
<PP> pp . 390 - 401 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> Half - order modal logic : How to prove real - time properties </TI>
<DE> . </DE>
<JN> Proceedings of the Ninth Annual Symposium on Principles of Distributed Computing </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> ACM Press </PU>
<DE> , </DE>
<DA> 1990 </DA>
<DE> , </DE>
<PP> pp . 281 - 296 </PP>
<DE> . </DE>
</REC>
<REC>
<AU> Rajeev Alur and Thomas A. Henzinger </AU>
<DE> . </DE>
<TI> A really temporal logic </TI>
<DE> . </DE>
<JN> Proceedings of the 30th Annual Symposium on Foundations of Computer Science </JN>
<DE> ( </DE>
<DE> ) </DE>
<DE> , </DE>
<PU> IEEE Computer Society Press </PU>
<DE> , </DE>
<DA> 1989 </DA>
<DE> , </DE>
<PP> pp . 164 - 169 </PP>
<DE> . </DE>
</REC>
