CAV (Conference on Computer-Aided Verification)

• 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-Verlag, 2003, pp. 262-274.

• 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-Verlag, 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-Verlag, 2002, pp. 414-427.

• 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-Verlag, 2002, pp. 526-538.

• Luca de Alfaro, Thomas A. Henzinger, and F.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-Verlag, 2000, pp. 186-201.

• 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-Verlag, 1999, pp. 208-221.

• 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-Verlag, 1999, pp. 301-315.

• Rajeev Alur, Thomas A. Henzinger, F.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-Verlag, 1998, pp. 521-525.

• Thomas A. Henzinger, Orna Kupferman, and Shaz Qadeer. From prehistoric to postmodern symbolic model checking. Proceedings of the Tenth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 1427, Springer-Verlag, 1998, pp. 195-206.

• 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-Verlag, 1998, pp. 440-451.

• Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-order reduction in symbolic state-space exploration. Proceedings of the Ninth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 1254, Springer-Verlag, 1997, pp. 340-351.

• Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A model checker for hybrid systems. Proceedings of the Ninth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 1254, Springer-Verlag, 1997, pp. 460-463.

• 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-Verlag, 1995, pp. 166-179.

• Thomas A. Henzinger and Pei-Hsin 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-Verlag, 1995, pp. 225-238.

• Rajeev Alur, Limor Fix, and Thomas A. Henzinger. A determinizable class of timed automata. Proceedings of the Sixth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 818, Springer-Verlag, 1994, pp. 1-13.

• Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. Computing accumulated delays in real-time systems. Proceedings of the Fifth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 697, Springer-Verlag, 1993, pp. 181-193.

CDC (IEEE Conference on Decision and Control)

• 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.

• 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.

CONCUR (Conference on Concurrency Theory)

• 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-Verlag, 2003, pp. 144-158.

• 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-Verlag, 2001, pp. 351-365.

• 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-Verlag, 2001, pp. 536-550.

• Luca de Alfaro, Thomas A. Henzinger, and F.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-Verlag, 2001, pp. 566-580.

• Luca de Alfaro, Thomas A. Henzinger, and F.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-Verlag, 2000, pp. 458-473.

• Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, and F.Y.C. Mang. Automating modular verification. Proceedings of the Tenth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1664, Springer-Verlag, 1999, pp. 82-97.

• 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-Verlag, 1999, pp. 320-335.

• 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-Verlag, 1998, pp. 163-178.

• 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-Verlag, 1998, pp. 439-454.

• J.-F. Raskin, P.-Y. Schobbens, and Thomas A. Henzinger. Axioms for real-time logics. Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1466, Springer-Verlag, 1998, pp. 219-236.

• 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-Verlag, 1997, pp. 74-88.

• Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1243, Springer-Verlag, 1997, pp. 273-287.

• 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-Verlag, 1996, pp. 530-545.

• 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-Verlag, 1996, pp. 514-529.

• 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-Verlag, 1994, pp. 162-177.

CSL (Conference for Computer Science Logic)

• 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-Verlag, 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-Verlag, 2002, pp. 292-305.

DASC (IEEE Digital Avionics Systems Conference)

• 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.

EMSOFT (Conference on Embedded Software)

• Thomas A. Henzinger and Christoph M. Kirsch. A typed assembly language for real-time programs. Proceedings of the Fourth International Conference on Embedded Software (EMSOFT), Lecture Notes in Computer Science, Springer-Verlag, 2004.

• Thomas A. Henzinger, Christoph M. Kirsch, and Slobodan Matic. Schedule carrying code. Proceedings of the Third International Conference on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2855, Springer-Verlag, 2003, pp. 241-256.

• Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Marielle Stoelinga. Resource interfaces. Proceedings of the Third International Conference on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2855, Springer-Verlag, 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-Verlag, 2002, pp. 108-122.

• 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-Verlag, 2002, pp. 76-92.

• Christoph M. Kirsch, Marco A.A. Sanvido, Thomas A. Henzinger, and Wolfgang Pree. A Giotto-based helicopter control system. Proceedings of the Second International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2491, Springer-Verlag, 2002, pp. 46-60.

• 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-Verlag, 2001, pp. 148-165.

• Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. Giotto: A time-triggered language for embedded programming. Proceedings of the First International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, pp. 166-184.

FMCAD (Conference on Formal Methods in Computer-Aided Design)

• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. An assume-guarantee rule for checking simulation. Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD), Lecture Notes in Computer Science 1522, Springer-Verlag, 1998, pp. 421-432.

FTRTFT (Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems)

• 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-Verlag, 1998, pp. 228-240.

• 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-Verlag, 1994, pp. 351-372.

• 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-Verlag, 1994, pp. 431-454.

FOCS (IEEE Symposium on Foundations of Computer Science)

• 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.

• Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society Press, 1997, pp. 100-109.

• 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.

• 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 and Thomas A. Henzinger. A really temporal logic. Proceedings of the 30th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society Press, 1989, pp. 164-169.

FSE (ACM Symposium on Foundations of Software Engineering)

• 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.

HSCC (Workshop on Hybrid Systems: Computation and Control)

• 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-Verlag, 2004, pp. 357-371.

• Franck Cassez, Thomas A. Henzinger, and J.-F. 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-Verlag, 2002, pp. 134-148.

• 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-Verlag, 2001, pp. 275-290.

• 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-Verlag, 2000, pp. 130-144.

• Thomas A. Henzinger and J.-F. 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-Verlag, 2000, pp. 145-159.

• 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-Verlag, 1998, pp. 190-204.

• 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-Verlag, 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-Verlag, 1997, pp. 48-62.

• Thomas A. Henzinger and Howard Wong-Toi. Linear phase-portrait approximations for nonlinear hybrid systems. In Hybrid Systems III, Lecture Notes in Computer Science 1066, Springer-Verlag, 1996, pp. 377-388.

• 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-Verlag, 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-Verlag, 1995, pp. 265-294.

• 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-Verlag, 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-Verlag, 1993, pp. 60-76.

ICALP (International Colloquium on Automata, Languages, and Programming)

• 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-Verlag, 2003, pp. 886-902.

• 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-Verlag, 2003, pp. 1022-1037.

• 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-Verlag, 2002, pp. 644-656.

• Thomas A. Henzinger, J.-F. Raskin, and P.-Y. 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-Verlag, 1998, pp. 580-591.

• Thomas A. Henzinger and Peter W. Kopke. Discrete-time control for rectangular hybrid automata. Proceedings of the 24th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 1256, Springer-Verlag, 1997, pp. 582-593.

• 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-Verlag, 1995, pp. 324-335.

• 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-Verlag, 1995, pp. 417-428.

• 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-Verlag, 1992, pp. 545-558.

ICAOS (International Conference on Analysis and Optimization of Systems)

• Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The algorithmic analysis of hybrid systems. 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-Verlag, 1994, pp. 331-351.

ICCAD (ACM/IEEE International Conference on Computer-Aided Design)

• 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.

• 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, 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.

ICSE (ACM/IEEE International Conference on Software Engineering)

• 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.

• Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, Minsu Kang, Christoph M. Kirsch, Rupak Majumdar, F.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.

IFAC (IFAC World Congress on Automatic Control)

• 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.

IWPC (IEEE International Workshop on Program Comprehension)

• 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.

LCTES (ACM Conference on Languages, Compilers, and Tools for Embedded Systems)

• 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.

LICS (IEEE Symposium on Logic in Computer Science)

• Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski, Games with secure equilibria. Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 2004.

• 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 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 and Thomas A. Henzinger. Reactive modules. Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1996, pp. 207-218.

• 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.

• Rajeev Alur and Thomas A. Henzinger. Finitary fairness. Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1994, pp. 52-61.

• Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1992, pp. 394-406.

• Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1990, pp. 390-401.

PLDI (ACM Conference on Programming Language Design and Implementation)

• 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.

• Thomas A. Henzinger and Christoph M. Kirsch. The Embedded Machine: Predictable, portable real-time code. Proceedings of the International Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2002, pp. 315-326.

PODC (ACM Symposium on Principles of Distributed Computing)

• Rajeev Alur, Tomas Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. Proceedings of the Tenth Annual Symposium on Principles of Distributed Computing (PODC), ACM Press, 1991, pp. 139-152.

• 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.

POPL (ACM Symposium on Principles of Programming Languages)

• Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Ken 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 Gregoire Sutre. Lazy abstraction. Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, 2002, pp. 58-70.

• Thomas A. Henzinger, Zohar Manna, and Amir 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.

QEST (IEEE Conference on Quantitative Evaluation of Systems)

• Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. Trading memory for randomness. Proceedings of the First International Conference on Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press, 2004.

REX (Workshop on Research and Education in Concurrent Systems)

• Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In Compositionality: The Significant Difference, Lecture Notes in Computer Science 1536, Springer-Verlag, 1998, pp. 23-60.

• 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-Verlag, 1992, pp. 74-106.

• Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Timed transition systems. In Real Time: Theory in Practice, Lecture Notes in Computer Science 600, Springer-Verlag, 1992, pp. 226-251.

RTSS (IEEE Real-Time Systems Symposium)

• 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.

• Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. Proceedings of the 14th Annual Real-Time Systems Symposium (RTSS), IEEE Computer Society Press, 1993, pp. 2-11.

SAS (Static-Analysis Symposium)

• 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, Springer-Verlag, 2004.

• Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, and Jens Palsberg. Stack size analysis for interrupt-driven programs. Proceedings of the Tenth International Static Analysis Symposium (SAS), Lecture Notes in Computer Science 2694, Springer-Verlag, 2003, pp. 109-126.

• Thomas A. Henzinger, Rupak Majumdar, F.Y.C. Mang, and J.-F. Raskin. Abstract interpretation of game properties. Proceedings of the Seventh International Static Analysis Symposium (SAS), Lecture Notes in Computer Science 1824, Springer-Verlag, 2000, pp. 220-239.

SODA (ACM/SIAM Symposium on Discrete Algorithms)

• Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger. Quantitative stochastic parity games. Proceedings of the 15th Annual Symposium on Discrete Algorithms (SODA), SIAM, 2004, pp. 114-123.

SPIN (Workshop on Model Checking of Software)

• 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-Verlag, 2003, pp. 235-239.

STACS (Conference on Theoretical Aspects of Computer Science)

• Thomas A. Henzinger and Rupak Majumdar. A classification of symbolic transition systems. Proceedings of the 17th International Conference on Theoretical Aspects of Computer Science (STACS), Lecture Notes in Computer Science 1770, Springer-Verlag, 2000, pp. 13-34.

STOC (ACM Symposium on Theory of Computing)

• Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata? Proceedings of the 27th Annual Symposium on Theory of Computing (STOC), ACM Press, 1995, pp. 373-382.

• 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.

TACAS (Conference on Tools and Algorithms for the Construction and Analysis of Systems)

• Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Marielle Stoelinga. Model checking discounted temporal properties. 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-Verlag, 2004, pp. 77-92.

• Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. On the universal and existential fragments of the mu-calculus. 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-Verlag, 2003, pp. 49-64.

• 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-Verlag, 2000, pp. 142-156.

• 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-Verlag, 2000, pp. 299-314.

• 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-Verlag, 1998, pp. 330-344.

• 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-Verlag, 1995, pp. 41-71.

TCS (IFIP Conference on Theoretical Computer Science)

• 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-Verlag, 2000, pp. 549-563.

WWW (World-Wide Web Conference)

• Luca de Alfaro, Thomas A. Henzinger, and F.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.

Other Collections

• 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-Verlag, 2004, pp. 332-358.

• Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. Embedded control systems development with Giotto. In Software-Enabled Control: Information Technology for Dynamical Systems (T. Samad, G. Balas, eds.), IEEE Press and Wiley-Interscience, 2003, pp. 123-146.

• Thomas A. Henzinger. The theory of hybrid automata. 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-Verlag, 2000, pp. 265-292.

• 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-Verlag, 1996, pp. 265-282.

• Rajeev Alur and Thomas A. Henzinger. Real-time system = discrete system + clock variables. 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.