●Verificaiton Systems ○Hytech T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer 1:110-122, 1997. ○STeP Nikolaj Bjorner, Zohar Manna, Henny B. Sipma and Tomas E. Uribe. Deductive Verification of Real-time Systems Using STeP. Presented at ARTS 97. ○Uppaal Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Petersson, and Wang Yi. Uppaal -- a tool suite for automatic verification of real-time systems. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Hybrid Systems III, LNCS 1066, pages 232--243, Berlin, 1996. Springer-Verlag. ○KRONOS C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, volume 1066 of Lecture Notes in Computer Science, pages 208--219. Springer-Verlag, 1996. ○PVS N. Shankar. Verification of real-time systems using PVS. In Computer Aided Verification: Fifth International Conference, CAV'93, number 697 in Lecture Notes in Computer Science, pages 280--291, Elounda, Greece, June/July 1993. Springer-Verlag. ●More Basics R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2--34, May 1993. R. Alur and D. L. Dill, "A Theory of Timed Automata", Theoretical Computer Science, Vol. 126, pp. 183-235, 1994. Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994. R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering 22:181-201, 1996. ●Parametric Verification Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric Real-time Reasoning. In Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, pages 592-601, 1993. B. B'erard and L. Fribourg. Automated verification of a parametric real-time program: the ABR conformance protocol. In Proc. 11th Int. Conf. Computer Aided Verification (CAV'99), LNCS 1633, 1999, pp. 96-107. Thomas Hune, Judi Romijn, Marielle Stoelinga, and Frits Vaandrager. Linear parametric model checking of timed automata. Accpeted for Tools and Algorithms for the Construction and Analysis of Systems, 2001. ●Rectangular Automata T. Henzinger and P. Kopke. State equivalences for rectangular hybrid automata. In U. Montanari and V. Sassone, editors, CONCUR 96: Concurrency Theory, Lecture Notes in Computer Science 1119, pages 530--545. Springer-Verlag, 1996. T.A. Henzinger and P.W. Kopke. Discrete-time control for rectangular hybrid automata. Theoretical Computer Science, vol. 221, pp. 369-392, 1999. Thomas A. Henzinger and Rupak Majumdar. Symbolic Model Checking for Rectangular Hybrid Systems. Proceedings of the Sixth International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), Lecture Notes in Computer Science 1785, Springer-Verlag, 142-156, 2000. ●Priced Timed Automata Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, Frits W. Vaandrager: Minimum-Cost Reachability for Priced Timed Automata. HSCC 2001, Lecture Notes in Computer Science, volume 2034, 2001, 147-161. Rajeev Alur, Salvatorre La Torre, and George J. Pappas. Optimal paths in weighted timed automata. HSCC 2001, Lecture Notes in Computer Science, volume 2034, Springer, 2001, 49-62. ●Refinement of Hybrid Systems R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pages 390--402, 2000. Thomas A. Henzinger. Masaccio: a formal model for embedded components. Proceedings of the First IFIP International Conference on Theoretical Computer Science, Lecture Notes in Computer Science 1872, Springer-Verlag, 2000, pp. 549-563.