Publications

2015

UPPAAL STRATEGO: Verification, Performance Analysis and Optimization of Timed Game Strategies Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis and Jakob H. Taankvist. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Pages 206-211, LNCS 9035, Springer. DOI: 10.1007/978-3-662-46681-0_16. (bibtex).
UPPAAL SMC Tutorial (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøsted Poulsen. International Journal on Software Tools for Technology Transfer, Jan. 2015, pages 1-19, Springer. DOI: 10.1007/s10009-014-0361-y. (bibtex).

2014

Widening the Schedulability of Hierarchical Scheduling Systems. (pdf). A. Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Marius Mikucionis, Ulrik Nyman, and Arne Skou. In Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS 2014). (bibtex).
Adaptive Task Automata with Earliest-Deadline-First Scheduling (pdf). Leo Hatvani, Alexandre David, Cristina Seceleanu, and Paul Pettersson. In Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), volume 70. (bibtex).
On Time with Minimal Expected Cost! . Alexandre David, Peter G. Jensen, Kim G. Larsen, Axel Legay, Didier Lime, Mathias G. Sørensen, Jakob H. Taankvist. In Proceedings of the Automated Technology for Verification and Analysis conference (ATVA), LLNCS volume 8837, pages 129-145, 2014. DOI: 10.1007/978-3-319-11936-6_10. (bibtex).
Verification and Performance Evaluation of Timed Game Strategies (pdf). Alexandre David, Huixing Fang, Kim G. Larsen, and Zhengkui Zhang. In Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS), 2014, volume 8711, pages 100-114. DOI:: 10.1007/978-3-319-10512-3_8. (bibtex).
Degree of Schedulability of Mixed-Criticality Real-time Systems with Probabilistic Sporadic Tasks (pdf). A. Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim G. Larsen, Marius Mikucionis, Ulrik Nyman, and Arne Skou. TASE 2014, pages 126-130. DOI: 10.1109/TASE.2014.27. (bibtex).
Statistical Model Checker for Biological Systems (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, and Sean Sedwards. International Journal on Software Tools for Technology Transfer, to appear. (bibtex).
Formal verification and simulation for platform screen doors and collision avoidance in subway control systems pdf. Huixing Fang, Jianqi Shi, Huibiao Zhu, Jian Guo, Kim Guldstrand Larsen, and Alexandre David. International Journal on Software Tools for Technology Transfer, Volume 16, Number 4, 2014, pages 339-361. DOI: 10.1007/s10009-014-0318-1. bibtex.
Schedulability of Herschel Revisited Using Statistical Model Checking (pdf). Alexandre David, Kim G. Larsen, Axel Legay, and Marius Mikucionis. International Journal on Software Tools for Technology Transfer, Springer, pages 1-13. DOI: 10.1007/s10009-014-0331-4. bibtex.
Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Guanggyuan Li, and Danny Bøgsted Poulsen. ACSD 2014, to appear. bibtex.
Schedulability and Energy Efficiency for Multi-core Hierarchical Scheduling Systems (pdf). A. Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Marius Mikucionis, Ulrik Nyman, and Arne Skou. ERTS 2014, IEEE. bibtex.

2013

Real-Time Specifications (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, and Andrzej Wasowski. International Journal on Software Tools for Technology Transfer, Springer, pages 1-29. bibtex.
Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal (pdf). A. Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Marius Mikucionis, Ulrik Nyman, and Arne Skou. In Proceedings of Formal Aspects of Component Software, LNCS, pages 61-78. DOI: 10.1007/978-3-319-07602-7_6 bibtex.
Statistical Model Checking in Uppaal: Lets Practice (pdf). Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Marius Mikucionis. Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180, 2014. bibtex.
Remote Testing of Timed Specifications (pdf). Alexandre David, Kim G. Larsen, Marius Mikucionis, Omer L. Nguena Timo, and Antoine Rollet. In Proceedings of The 25th IFIP International Conference on Testing Software and Systems (ICTSS'13), LNCS 8254, pages 65-81. bibtex.
Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata (pdf). Alexandre David, Kim G. Larsen, Axel Legay, and Danny Bøgsted Poulsen. In Proceedings of Automated Verification of Critical Systems (AVoCS2013), volume 10. bibtex.
Efficient Controller Synthesis for a Fragment of MTL(0,∞) (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, and Guangyuan Li. In Acta Informatica, Special Issue on Synthesis, DOI: 10.1007/s00236-013-0189-z. bibtex.
Optimizing Control Strategy using Statistical Model Checking (pdf). Alexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay, and Marius Mikucionis. In Proceeding of NASA Formal Methods 2013, pages 352-367, LNCS volume 7871, Springer. DOI: 10.1007/978-3-642-38088-4_24. bibtex.

2012

Testing Real-Time Systems under Uncertainty (pdf). Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Marius Mikucionis, and Brian Nielsen. In FMCO 2010, published 2012, pages 352-371, LNCS volume 6957, Springer. DOI: 10.1007/978-3-642-25271-6_19. bibtex.
An Evaluation Framework for Energy Aware Buildings using Statistical Model Checking (pdf). Alexandre David, Dehui Du, Kim G. Larsen, Marius Mikucionis, and Arne Skou. In SCIENCE CHINA Information Sciences, volume 55, number 12, pages 2694-2707, 2012. bibtex.
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets (pdf). Alexandre David, Lasse Jacobsen, Morten Jacobsen, and Jiri Srba. Systems Software Verification Conference (SSV 2012), pages 125-140, EPTCS volume 102. DOI: 10.4204/EPTCS.102.12. bibtex.
Compositional Verification of Real-Time Systems Using Ecdar (pdf). Alexandre David, Kim. G. Larsen, Axel Legay, Mikael H. Møller, Ulrik Nyman, Anders P. Ravn, Arne Skou, and Andrzej Wasowski. International Journal on Software Tools for Technology Transfer, pages 703-720, volume 6, 2012. DOI: 10.1007/s10009-012-0237-y. bibtex.
Rewrite-Based Statistical Model Checking of WMTL (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyan Li, and Danny Bøgsted Poulsen. Runtime Verification 2012, pages 260-275, LNCS 7687. DOI: 10.1007/978-3-642-35632-2_25. bibtex.
Runtime Verification of Biological Systems (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, and Sean Sedwards. Runtime Verification of Biological Systems, ISOLA 2012, pages 388-404, LNCS volume 7609, Springer. DOI: 10.1007/978-3-642-34026-0_29. bibtex.
Schedulability of Herschel-Planck Revisited Using Statistical Model Checking (pdf). Alexandre David, Kim G. Larsen, Axel Legay, and Marius Mikucionis. Quantitative Modelling and Analysis, ISOLA 2012, pages 293-307, LNCS volume 7610, Springer. DOI: 10.1007/978-3-642-34032-1_28. bibtex.
Statistical Model Checking for Stochastic Hybrid Systems (pdf). Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, and Sean Sedwards. 1st International Workshop on Hybrid Systems and Biology 2012, pages 122-136, EPTCS volume 92, DOI: 10.4204/EPTCS.92.9. bibtex.
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, Marius Mikucionis, Danny Bøgsted Poulsen, Axel Legay, and Zheng Wang. 10th Workshop on Quantitative Aspects of Programming Languages and Systems, EPTCS 85, pages 1-16, DOI: 10.4204/EPTCS.85.1. bibtex.
Controllers with Minimal Observation Power (Application to Timed Systems) (pdf). Peter Bulychev, Franck Cassez, Alexandre David, Kim G. Larsen, Jean-François Raskin, and Pierre-Alain Reynier. 10th International Conference on Automated Technology for Verification and Analysis (ATVA), 2012, pages 223-237, LNCS 7561, Springer. bibtex.
- Extended version available at arxiv.
A Context-Aware User Interface for Wireless Personal-Area Network Assistive Environments (pdf). Bastien Paul, Séverin Marcombes, Alexandre David, Lotte N. S. Andreasen Struijk, and Yannick Le Moullec. In Wireless Personal Communications 2012, DOI: 10.1007/s11277-012-0582-x. bibtex.
State-of-the-art Tools and Techniques for Quantitative Modeling and Analysis of Embedded Systems (pdf). Marius Bozga, Alexandre David, Arnd Hartmanns, Holger Hermanns, Kim G. Larsen, Axel Legay, and Jan Tretmans. In Design, Automation & Test in Europe 2012, pages 370-375, IEEE. bibtex.
Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen, and Amelie Stainer. 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, 2012, pages 168-182, LNCS 7180, Springer. bibtex.
Checking & Distributing Statistical Model Checking (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Danny Bøgsted Poulsen. 4th NASA Formal Methods Symposium, 2012, pages 449-463, LNCS 7226, Springer. bibtex.
mctau: Bridging the Gap between Modest and UPPAAL (pdf). Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, and Holger Hermanns. In Model Checking Software - SPIN 2012, LNCS 7385, pages 227-233, DOI: 10.1007/978-3-642-31759-0_16. bibtex.
Moving from Specifications to Contracts in Component-based Design (pdf). Sebastian S. Bauer, Alexandre David, Rolf Hennicker, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. 15th International Conference on Fundamental Approaches to Software Engineering, 2012, pages 43-58, LNCS 7212, Springer. bibtex.
TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets (pdf). Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, and Jiri Srba. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2012, pages 492-497, LNCS 7214, Springer. bibtex.
Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach (pdf). Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, and Marius Mikucionis. In EPTCS proceedings of the Second International Workshop on Interactions, Games and Protocols, volume 78, pages 1-14, 2012. bibtex.

2011

Optimal Infinite Runs in One-Clock Priced Timed Automata (pdf). Alexandre David, Daniel Ejsing-Duun, Lisa Fontani, Kim G. Larsen, Vasile Popescu, Jacob Haubach Smedegard. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS), 2011. bibtex.
Distributed Parametric and Statistical Model Checking (pdf). Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis. In EPTCS proceedings of PDMC 2011, volume 72, pages 30-42. bibtex.
Statistical Model Checking for Networks of Priced Timed Automata (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bogsted Poulsen, Jonas van Vliet, Zheng Wang. In Proceedings of Formal Modeling and Analysis of Timed Systems, pages 80-96, 2011, LNCS 6919. bibtex.
Application of Model-Checking Technology to Controller Synthesis (pdf). Alexandre David, Jacob Deleuran Grunnet, Jan Jakob Jessen, Kim Guldstrand Larsen, and Jacob Illum Rasmussen. Proceedings of Formal Methods for Components and Objects, Lecture Notes in Computer Science, Volume 6957/2012, pages 336-351. bibtex.
Time for Statistical Model Checking of Real-time Systems (pdf). Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Zheng Wang. Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), 2011, LNCS. bibtex.
New Results on Time Specifications (pdf). Timothy Bourke, Alexandre David, Kim. G. Larsen, Axel Legay, Didier Lime, Ulrik Nyman, and Andrzej Wasowski. Proceedings of the 20th International Workshop on Algebraic Development Techniques in Verification, Model Checking, and Abstraction Interpretation (WADT), Elesten, October 2010, Lecture Notes in Computer Science, Springer Verlag, pages 175-192, LNCS 7137. bibtex.
Developing UPPAAL over 15 years (pdf). Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. Software: Practice and Experience, Volume 41, Issue 2, pages 133-142, February 2011. bibtex.

2010

Scenario-Based Verification of Real-Time Systems Using UPPAAL (pdf). Sandie Balaguer, Alexandre David, Kim G. Larsen, Shuhao Li, Brian Nielsen, and Saulius Pusinskas. Formal Methods in System Design, volume 37, number 2-3, pages 200-264, 2010. bibtex.
ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. Proceedings of Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, 2010, Volume 6252/2010, pages 365-370. bibtex.
An Interface Theory for Timed Systems (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. 20th International Workshop on Algebraic Development Techniques, WADT 2010, July 2010. bibtex.
Methodologies for Specification of Real-Time Systems Using Timed I/O Automata (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. In Proceedings of Formal Methods for Components and Objects, Lecture Notes in Computer Science, 2010, Volume 6286/2010, pages 290-310. bibtex.
Developing UPPAAL over 15 Years. Gerd Behrmann, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi.
- [Extended abstract (pdf)] Workshop on Tool Building in Formal Methods, ABZ 2010, Orford Canada, February 22-25, 2010. bibtex.
- [Journal] Software: Practice and Experience published in January 2011.
Timed I/O automata: a complete specification theory for real-time systems (pdf). Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. In proceedings of HSCC 2010, pages 91-100. bibtex.
Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1 (pdf). Alexandre David, Jacob Illum, Kim G. Larsen, and Arne Skou. In Model-Based Design for Embedded Systems, ed. Gabriela Nicolescu and Pieter J. Mosterman, CRC Press 2010, pages 93-119. bibtex.

2009

Tools for Model-Checking Timed Systems (ps.gz/ pdf). Alexandre David, Gerd Behrmann, Peter Bulychev, Joakim Byg, Thomas Chatain, Kim G. Larsen, Paul Pettersson, Jacob Illum Rasmussen, Jiri Srba, Wang Yi, Kenneth Y. Joergensen, Didier Lime, Morgan Magnin, Olivier H. Roux, and Louis-Marie Traonouez. In Communicating Embedded Systems - Software and Design Roux, Olivier H. and Jard, Claude, pages 165-225, ISTE Publishing / John Wiley, ISBN 9781848211438, 2009. bibtex.
Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation (pdf). Peter Bulychev and Thomas Chatain and Alexandre David and Kim G. Larsen. Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems, 2009, pages 73-87, LNCS 5813, Springer. bibtex.
Playing Games with Timed Games (pdf). Thomas Chatain, Alexandre David, and Kim G. Larsen. 3rd IFAC Conference on Analysis and Design of Hybrid Systems, 2009, pages 238-243, online reference, bibtex.
Timed Testing under Partial Observability (pdf). Alexandre David, Kim G. Larsen, Shuhao Li, and Brian Nielsen. 2nd IEEE International Conference on Software Testing, Verification, and Validation (ICST'09), Denver, Colorado, USA, 1. april 2009 - 4. april 2009. bibtex.

2008

Model-Driven Development of Embedded Real-Time Systems. Alexandre David and Brian Nielsen. ERCIM News, Issue number 75, pages 19-20. bibtex.
Playing Games with Timed Games (homepage,pdf). Th. Chatain, A. David and K. G. Larsen. Research Report LSV-08-34, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2008. 15 pages. bibtex.
Outils de Model-Checking (pdf). Alexandre David, Gerd Behrmann, Kim G. Larsen, Paul Pettersson, Jacob Illum Rasmussen, Wang Yi, Didier Lime, Morgan Magnin, and Olivier H. Roux. In Approches formelles des systèmes embarqués communicant (abstract), Olivier H. Roux and Claude Jard, Hermes Lavoisier, série Informatique et systèmes d'information, ISBN 978-2-7462-1942-7. bibtex.
Cooperative Testing of Uncontrollable Real-Time Systems (pdf). Alexandre David, Kim G. Larsen, Shuhao Li, and Brian Nielsen. 4th workshop of Model-Based Testing (MBT'08), Budapest, Hungary. bibtex.
A Game-Theoretical Approach to Real-Time System Testing (pdf). Alexandre David, Kim G. Larsen, Shuhao Li, and Brian Nielsen. In Proceedings of the 11th International Conference on Design Automation and Test in Europe (DATE'08), Munich, Germany, March 10-14th 2008. bibtex.

2007

Guided Controller Synthesis for Climate Controller Using UPPAAL-TIGA (pdf). Jan Jakob Jessen, Jacob Illum Rasmussen, Kim G. Larsen, and Alexandre David. In Proceedings of the 19th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'07), pages 227-240, LNCS 4763. bibtex.
UPPAAL-TIGA: Time for Playing Games! (pdf). Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), pages 121-125, LNCS 4590. bibtex.
Timed Control with Observation Based and Stuttering Invariant Strategies (pdf). Franck Cassez, Alexandre David, Kim G. Larsen, Didier Lime, and Jean François Raskin. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), pages 192-206, LNCS 4762, October 2007, Tokyo, Japan. bibtex.

2006

UPPAAL-Tiga: Timed Games for Everyone (ps.gz/pdf). Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. In Proceedings of the 18th Nordic Workshop on Programming Theory, October 2006, Reykjavik, Iceland. bibtex.
Model Checking Timed Automata with Priorities using DBM Subtraction (ps.gz/pdf). Alexandre David, John Håkansson, Kim G. Larsen, and Paul Pettersson. In Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), pages 128-142, LNCS 4202. bibtex.
UPPAAL 4.0 (ps.gz/pdf). Gerd Behrmann and Alexandre David and Kim G. Larsen and John Håkansson and Paul Pettersson and Wang Yi and Martijn Hendriks. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST) 2006, pages 125-126, IEEE Computer Society. bibtex.

2005

Merging DBMs Efficiently (extended abstract) (ps.gz/pdf). Alexandre David. In Proceedings of the 17th Nordic Workshop on Programming Theory, October 2005, DIKU Copenhagen. bibtex.
Efficient On-the-fly Algorithms for the Analysis of Timed Games (ps.gz/pdf). Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. In Proceedings of the 16th CONCUR Conference, August 2005, pages 66-80, LNCS 3653. bibtex.

2004

Minimal DBM Substraction (ps.gz/pdf). Alexandre David, John Håkansson, Kim G. Larsen, and Paul Pettersson. In Proceedings of the 16th Nordic Workshop on Programming Theory, October 6-8, 2004, Uppsala Sweden, pages 17-20. Uppsala University IT Technical report 2004-041, issn 1404-3203. bibtex.
A Tutorial on UPPAAL (ps.gz/pdf). Gerd Behrmann, Alexandre David, and Kim G. Larsen. In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04). LNCS number 3185, Springer. bibtex.

2003

Hierarchical Modeling and Analysis of Timed Systems. Ph. D. thesis. (ps.gz/pdf). Alexandre David. Uppsala University, November 2003. bibtex.
A Tool Architecture for the Next Generation of UPPAAL (ps.gz/pdf). Gerd Behrmann, Alexandre David, Kim G. Larsen, and Wang Yi. In Proceedings of the UNU/IIST 10th Anniversary Colloquium, Formal Methods at the Crossroad: From Panacea to Foundational Support. LNCS. bibtex.
Unification and Sharing in Timed Automata Verification (ps.gz/pdf). Gerd Behrmann, Alexandre David, Kim G. Larsen, and Wang Yi. In Proceedings of the Spin Workshop 2003. LNCS 2648, pages 225-229. bibtex.
A Tool Architecture for the Next Generation of UPPAAL (ps.gz/pdf/url). Gerd Behrmann, Alexandre David, Kim G. Larsen, and Wang Yi. Uppsala University Technical Report Series. bibtex.
A Formal Semantics for UML Statecharts (ps.gz/pdf/url). Alexandre David, Johann Deneux, and Julien d'Orso. Uppsala University Technical Report Series. bibtex.
Verification of UML Statecharts with Real-Time Extensions (ps.gz/pdf/url). Alexandre David, M. Oliver Möller, and Wang Yi. Uppsala University Technical Report Series. bibtex.

2002

UPPAAL Implementation Secrets (pdf). 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). LNCS 2469, pages 3-22. bibtex.
New UPPAAL Architecture (ps.gz/pdf). Gerd Behrmann, Alexandre David, Kim G. Larsen, and Wang Yi. In Proceedings of the Workshop on Real-Time Tools (RTTOOLS'02). Uppsala University Technical Report Series. bibtex.
Formal Verification of UML Statecharts with Real-Time Extensions (ps.gz/pdf). Alexandre David, Oliver Möller, and Wang Yi. In Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE'02). LNCS 2306, pages 218-232. bibtex.

2001

UPPAAL - Now, Next, and Future (ps.gz/pdf). Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. d'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, and Wang Yi. In Proceedings of Modelling and Verification of Parallel Processes. LNCS 2067, pages 100-125. bibtex.
UPPAAL - Present and Future (ps.gz). Gerd Behrmann, Alexandre David, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, and Wang Yi. In Proceedings of the 4th IEEE Conference on Decision and Control (CDC'01), IEEE Computer Society Press. bibtex.
Practical Verification of Real-time Systems (ps.gz/pdf/url). Alexandre David. Licentiate thesis. Uppsala Technical Report Series. bibtex.
Tools for Real-Time UML: Formal Verification and Code Synthesis (ps.gz/pdf). Tobias Amnell, Alexandre David, Elena Fersman, M. Oliver Möller, Paul Pettersson, and Wang Yi. In Proceedings of the SIVOES Workshop, part of the ECOOP conference. bibtex.
Formal Verification of UML Statechart with Real-time Extensions (ps.gz/pdf). Alexandre David, Oliver Möller, and Wang Yi. In Proceedings of the Nordic Workshop on Programming Theory. bibtex.
From HUPPAAL to UPPAAL: A Translation from Hierarchical Timed Automata to Flat Timed Automata (ps.gz/url). Alexandre David and Oliver Möller. BRICS Technical Report Series RS-01-11. bibtex.

2000

A Real Time Animator for Hybrid Systems (ps.gz/pdf). Tobias Amnell, Alexandre David, and Wang Yi. In Proceedings of the 6th ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES'2000). bibtex.
Modelling and Analysis of a Commercial Field Bus Protocol (ps.gz/pdf) (updated version with errata). Alexandre David and Wang Yi. In Proceedings of the 12th Euromicro Conference on Real Time Systems. IEEE Computer Society, pages 165-172. bibtex.

1999

Modeling and Analysis of a Field Bus Protocol Using UPPAAL (ps.gz/pdf). Alexandre David, Ulf Hammar, and Wang Yi. In Proceedings of the Nordic Workshop on Programming Theory. bibtex.

1998

UL++: an Object Oriented Language for Hierarchical Modelling and Analysis (ps.gz). Alexandre David, Justin Pearson, and Wang Yi. In Proceedings of the Nordic Workshop on Programming Theory. bibtex.
UL++: an Object Oriented Language for UPPAAL (ps.gz). Alexandre David. MSc thesis. Uppsala University. bibtex.