Bengtson, Wang: Timed Automata: Semantics, Algorithms and Tools
Joost-Pieter Katoen: Concepts, Algorithms, and Tools for Model Checking (Especially Chapter 4)
Rajeev Alur: Timed Automata (survey) NATO-ASI 1998 Summer School on Verification of Digital and Hybrid Systems.
Larsen, Pettersson, Yi: Uppaal in a Nutshell. In Springer International Journal of Software Tools for Technology Transfer, volume 1, issue 1+2, pages 134-152, 1997.
Alexandre David: UPPAAL2k: Small Tutorial
Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco, California, USA, 3-5 December 1997.
Efficient Timed Reachability Analysis Using Clock Difference Diagrams. Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. In the proceedings of CAV99, 11th International Conference on Computer-Aided Verification, July 7-10, 1999, Trento, Italy. Lecture Notes in Computer Science Volume 1633, Springer-Verlag, 1999.
Clock Difference Diagrams. Kim G. Larsen, Carsten Weise, Wang Yi and Justin Pearson. Nordic Journal of Computing, 1999.
Gerd Behrmann, Thomas Hune, Frits Vaandrager: Disitributing Timed Model Checking -- How the Search Order Matters`, In Proceedings of CAV'2000, Chicago.
UPPAAL - Present and Future. Gerd Behrmann, Alexandre David, Kim G. Larsen, Oliver Muller, Paul Pettersson, and Wang Yi. In Proceedings of the 40th IEEE Conference on Decision and Control (CDC'2001). Orlando, Florida, USA, December 4 to 7, 2001.
UPPAAL Implementation Secrets: Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), 2002.
Gerd Behrmann, Kim G. Larsen, Radek Pelanek: To Store or Not to Store, Computer Aided Verification 2003.
Gerd Behrmann, Patricia Bouyer, Emmanuel Fluery, Kim G Larsen: Static Guard Analysis in Timed Automata Analysis, TACAS 2003.
Exact Acceleration of Real-Time Model Checking. M. Hendriks and K. G. Larsen. In E. Asarin, O. Maler and S. Yovine, editors, ENTCS, volume 65 issue 6. Elsevier Science Publishers, April 2002.
Guided Synthesis of Control Programs Using UPPAAL. Thomas Hune, Kim G. Larsen and Paul Pettersson. In Proceedings of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation ( DSVV'2000), pages E15-E22, Ten H. Lai (Ed.). Taipei, Taiwan, April 10-13, 2000.
Minimum-Cost Reachability for Priced Timed Automata. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. In Proceedings of the 4th International Workwhop on Hybrid Systems: Computation and Control (HSCC'01). Rome, Italy, March 28 to 30, 2001. LNCS 2034, pages 147-161, Maria Domenica Di Benedetto and Alberto Sangiovanni-Vincentelli (Eds.)
Efficient Guiding Towards Cost-Optimality in UPPAAL. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01). Genova, Italy, April 2 to 6, 2001. LNCS 2031, pages 174-188, T. Margaria and W. Yi (Eds.).
As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. Kim G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. In Procceedings of the 13th Conference on Computer Aided Verification, (CAV'01). 2001. LNCS 2102, pages 493-505, G. Berry, H. Comon, A. Finkel (Eds.). Paris, France, July 18 to 23, 2001.
Guided Synthesis of Control Programs Using UPPAAL. Thomas Hune, Kim G. Larsen, and Paul Pettersson. In Nordic Journal of Computing (NJC), volume 8, number 1, 2001, pages 43-64
Franck Cassez, Kim Guldstrand Larsen: The Impressive Power of Stopwatches. CONCUR 2000: 138-152
From Timed Automata to Logic - And Back. F. Laroussinie, K.G. Larsen, C. Weise. In Proc. of MFCS'95
Compositional Model-Checking of Real Time Systems. F. Laroussinie and K.G. Larsen. In Proc. of CONCUR'95