Alexandre David
Associate Professor

Department of Computer Science
Aalborg University
Selma Lagerløfs Vej 300
DK-9220 Aalborg Øst
Denmark

Office:	1.2.05
Phone:	(+45) 9940 7226
Fax:	(+45) 9940 9798
E-mail:

My research interests include formal verification methods, model-checking of real-time systems, hierarchical modeling and verification, code generation, tool development, and timed games. I am working in the Distributed and Embedded Systems group in Aalborg. I am also collaborating with the UPPAAL research group in Uppsala.

Publications

2013

Optimizing Control Strategy using Statistical Model Checking (pdf). Alexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay, and Marius Mikucionis. To appear at NFM 2013.

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 . Alexandre David, Dehui Du, Kim G. Larsen, Marius Mikucionis, and Arne Skou. Science China Journal, to appear. 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. To appear. 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. To appear in Proceedings of Formal Methods for Components and Objects, Lecture Notes in Computer Science, 2011, Volume 6957/2011. 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.