Pierre-Alain Reynier

Professeur, Université d'Aix-Marseille, Département Informatique et Interactions

Chercheur au LIS

Responsable de l'équipe Modélisation et Vérification (MoVe) du LIS

Responsable du Parcours Informatique et Mathématiques Discrètes du Master Informatique.

Co-responsable (avec Nathalie Bertrand) du groupe de travail Vérification du GDR-IM du CNRS


Contact :

Laboratoire d’Informatique et Systèmes
Parc Scientifique de Luminy
163 avenue de Luminy - Case 901
F-13288 Marseille Cedex 9, France


Office : A208 (bibilothèque universitaire, 2ème étage)
Phone : +33 (0)4 86 09 06 73
Fax : +33 (0)4 86 09 ?? ??

E-mail : prénom.nom@lis-lab.fr (Nouveau !)



Livres/Chapitres de livres

  1. Reachability Problems - 12th International Conference, RP 2018, Marseille, France, September 24-26, 2018, Proceedings. Igor Potapov and Pierre-Alain Reynier.
    Springer. 2018.
    ISBN: 978-3-030-00249-7

  2. MSR 2017 - 11th National Colloquium on Modelization of Reactive Systems. Isabel Demongodin and Pierre-Alain Reynier.
    November 15-17, 2017. Marseille, France


  3. MOVEP 2012 - 10th International Winter School on Modelization and Verification of Parallel Processes. Pierre-Alain Reynier.
    December 3-7, 2012. Marseille, France


  4. An Introduction to Automatic Synthesis of Discrete and Timed Controllers. Franck Cassez, Kim Larsen, Jean-François Raskin et Pierre-Alain Reynier.
    In Quantitative Model-Based Analysis of Real-Time Embedded Systems. Springer. 2012.
    ISBN: 978-94-007-1368-0

  5. Timed Controller Synthesis: An Industrial Case Study. Franck Cassez, Kim Larsen, Jean-François Raskin et Pierre-Alain Reynier.
    In Quantitative Model-Based Analysis of Real-Time Embedded Systems. Springer. 2012.
    ISBN: 978-94-007-1368-0

  6. Verification of Timed Systems. Pierre-Alain Reynier.
    In Models and Analysis in Distributed Systems, pages 271–306. Wiley. 2011.
    ISBN: 978-18-482-1314-2

Journaux

  1. Optimal controller synthesis for timed systems. Damien Busatto-Gaston, Benjamin Monmege et Pierre-Alain Reynier.
    In Logical Methods in Computer Science. 2022. To appear (accepted with minor revision)


  2. Computability of Data-Word Transductions over Different Data Domains. Léo Exibard, Emmanuel Filiot, Nathan Lhote et Pierre-Alain Reynier.
    In Logical Methods in Computer Science. 2022. To appear (accepted with minor revision)


  3. Synthesis of Data Word Transducers. Léo Exibard, Emmanuel Filiot et Pierre-Alain Reynier.
    In Logical Methods in Computer Science, volume 17 (1), . 2021.
    DOI: 10.23638/LMCS-17(1:22)2021

  4. Optimal and robust controller synthesis using energy timed automata with uncertainty. Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey et Pierre-Alain Reynier.
    In Formal Aspects Comput., volume 33 (1), pages 3–25. 2021.
    DOI: 10.1007/s00165-020-00521-4

  5. Copyful Streaming String Transducers. Emmanuel Filiot et Pierre-Alain Reynier.
    In Fundam. Informaticae, volume 178 (1-2), pages 59–76. 2021.
    DOI: 10.3233/FI-2021-1998

  6. From Two-Way Transducers to Regular Function Expressions. Nicolas Baudru et Pierre-Alain Reynier.
    In Int. J. Found. Comput. Sci., volume 31 (6), pages 843–873. 2020.
    DOI: 10.1142/S0129054120410087

  7. Streamability of nested word transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier et Frédéric Servais.
    In Logical Methods in Computer Science, volume 15 (2), . 2019.
    DOI: 10.23638/LMCS-15(2:1)2019

  8. Aperiodic String Transducers. Luc Dartois, Isma\"el Jecker et Pierre-Alain Reynier.
    In International Journal of Foundations of Computer Science, volume 29 (5), pages 801–824. World Scientific. 2018.
    DOI: 10.1142/S0129054118420054

  9. Decision Problems of Tree Transducers with Origin. Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Information and Computation, volume 261, pages 311–335. Elsevier. 2018.
    DOI: 10.1016/j.ic.2018.02.011

  10. Visibly Pushdown Transducers. Emmanuel Filiot, Jean-Francois Raskin, Pierre-Alain Reynier, Frédéric Servais et Jean-Marc Talbot.
    In Journal of Computer and System Sciences. Elsevier. 2018.
    DOI: 10.1016/j.jcss.2018.05.002

  11. Transducers, logic and algebra for functions of finite words. Emmanuel Filiot et Pierre-Alain Reynier.
    In SIGLOG News, volume 3 (3), pages 4–19. 2016.
    DOI: 10.1145/2984450.2984453

  12. Visibly Pushdown Transducers with Well-nested Outputs. Pierre-Alain Reynier et Jean-Marc Talbot.
    In International Journal of Foundations of Computer Science, volume 27 (2), pages 235–258. World Scientific. 2016.
    DOI: 10.1142/S0129054116400086

  13. Robustness of Time Petri Nets under Guard Enlargement. S. Akshay, Loic Hélouet, Claude Jard et Pierre-Alain Reynier.
    In Fundamenta Informaticae, volume 143 (3-4), pages 207–234. IOS Press. 2016.
    DOI: 10.3233/FI-2016-1312

  14. Trimming Visibly Pushdown Automata. Mathieu Caralp, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Theoretical Computer Science, volume 578, pages 13–29. Elsevier. 2015.
    DOI: 10.1016/j.tcs.2015.01.018

  15. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. Pierre-Alain Reynier et Frédéric Servais.
    In Fundamenta Informaticae, volume 122 (1-2), pages 1–30. IOS Press. 2013.
    DOI: 10.3233/FI-2013-781

  16. On Characteristic Formulae for Event-Recording Automata. Omer-Landry Nguena-Timo et Pierre-Alain Reynier.
    In RAIRO - Theoretical Informatics and Applications, volume 47 (1), pages 69–96. EDP Sciences. 2013.
    DOI: 10.1051/ita/2012029

  17. Undecidability Results for Timed Automata with Silent Transitions. Patricia Bouyer, Serge Haddad et Pierre-Alain Reynier.
    In Fundamenta Informaticae, volume 92 (1-2), pages 1–25. IOS Press. 2009.
    DOI: 10.3233/FI-2009-0063

  18. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Patricia Bouyer, Serge Haddad et Pierre-Alain Reynier.
    In Information and Computation, volume 206 (1), pages 73–107. Elsevier. 2008.
    DOI: 10.1016/j.ic.2007.10.004

Conférences internationales

  1. Weighted Automata and Expressions over Pre-Rational Monoids. Nicolas Baudru, Louis-Marie Dando, Benjamin Monmege, Nathan Lhote, Pierre-Alain Reynier et Jean-Marc Talbot.
    In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2022. To appear


  2. Playing Stochastically in Weighted Timed Games to Emulate Memory. Benjamin Monmege, Julie Parreaux et Pierre-Alain Reynier.
    In 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), pages 137:1–137:17, volume 198 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2021.
    DOI: 10.4230/LIPIcs.ICALP.2021.137

  3. Reaching Your Goal Optimally by Playing at Random with No Memory. Benjamin Monmege, Julie Parreaux et Pierre-Alain Reynier.
    In Proc. 31st International Conference on Concurrency Theory (CONCUR 2020), pages 26:1–26:21, volume 171 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2020.
    DOI: 10.4230/LIPIcs.CONCUR.2020.26

  4. On Computability of Data Word Functions Defined by Transducers. Léo Exibard, Emmanuel Filiot et Pierre-Alain Reynier.
    In Proc. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), pages 217–236, volume 12077 of Lecture Notes in Computer Science. Springer. 2020.
    DOI: 10.1007/978-3-030-45231-5\_12

  5. Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach. Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier et Ocan Sankur.
    In Proc. 31st International Conference on Computer Aided Verification (CAV 2019), pages 572–590, volume 11561 of Lecture Notes in Computer Science. Springer. 2019.
    DOI: 10.1007/978-3-030-25540-4\_33

  6. Synthesis of Data Word Transducers. Léo Exibard, Emmanuel Filiot et Pierre-Alain Reynier.
    In Proc. 30th International Conference on Concurrency Theory (CONCUR 2019), pages 24:1–24:15, volume 140 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2019.
    DOI: 10.4230/LIPIcs.CONCUR.2019.24

  7. Sequentiality of String-to-Context Transducers. Pierre-Alain Reynier et Didier Villevalois.
    In Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), pages 128:1–128:14, volume 132 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2019.
    DOI: 10.4230/LIPIcs.ICALP.2019.128

  8. On the Computation of the Minimal Coverability Set of Petri Nets. Pierre-Alain Reynier et Frédéric Servais.
    In Proc. 13th International Conference on Reachability Problems (RP 2019), pages 164–177, volume 11674 of Lecture Notes in Computer Science. Springer. 2019.
    DOI: 10.1007/978-3-030-30806-3\_13

  9. Symbolic approximation of weighted timed games. Damien Busatto-Gaston, Benjamin Monmege et Pierre-Alain Reynier.
    In Proc. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), pages 28:1–28:16 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2018.
    DOI: 10.4230/LIPIcs.FSTTCS.2018.28

  10. From Two-Way Transducers to Regular Function Expressions. Nicolas Baudru et Pierre-Alain Reynier.
    In Proc. 22nd International Conference on Developments in Language Theory (DLT 2018), pages 96–108, volume 11088 of Lecture Notes in Computer Science. Springer. 2018.
    DOI: 10.1007/978-3-319-98654-8\_8

  11. Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty. Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey et Pierre-Alain Reynier.
    In Proc. 22nd International Symposium on Formal Methods, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, pages 203–221, volume 10951 of Lecture Notes in Computer Science. Springer. 2018.
    DOI: 10.1007/978-3-319-95582-7\_12

  12. Copyful Streaming String Transducers. Emmanuel Filiot et Pierre-Alain Reynier.
    In Proc. of 11th International Workshop on Reachability Problems (RP 2017), pages 75–86, volume 10506 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: 10.1007/978-3-319-67089-8_6

  13. Degree of sequentiality of weighted automata. Laure Daviaud, Ismael Jecker, Pierre-Alain Reynier et Didier Villevalois.
    In Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), pages 215–230, volume 10203 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: 10.1007/978-3-662-54458-7_13

  14. Optimal Reachability in Divergent Weighted Timed Games. Damien Busatto-Gaston, Benjamin Monmege et Pierre-Alain Reynier.
    In Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), pages 162–178, volume 10203 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: https://doi.org/10.1007/978-3-662-54458-7_10

  15. Aperiodic String Transducers. Luc Dartois, Ismael Jecker et Pierre-Alain Reynier.
    In Proc. 20th International Conference on Developments in Language Theory (DLT 2016), pages 125–137, volume 9840 of Lecture Notes in Computer Science. Springer. 2016.
    DOI: 10.1007/978-3-662-53132-7_11

  16. Two-Way Visibly Pushdown Automata and Transducers. Luc Dartois, Emmanuel Filiot, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), pages 217–226. ACM. 2016.
    DOI: 10.1145/2933575.2935315

  17. A Generalized Twinning Property for Minimisation of Cost Register Automata. Laure Daviaud, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), pages 857–866. ACM. 2016.
    DOI: 10.1145/2933575.2934549

  18. Decision Problems of Tree Transducers with Origin. Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015), pages 209–221, volume 9135 of Lecture Notes in Computer Science. Springer. 2015.
    DOI: 10.1007/978-3-662-47666-6_17

  19. Probabilistic Robust Timed Games. Youssouf Oualhadj, Pierre-Alain Reynier et Ocan Sankur.
    In Proc. 25th International Conference on Concurrency Theory (CONCUR'14), pages 203–217, volume 8704 of Lecture Notes in Computer Science. Springer. 2014.
    DOI: 10.1007/978-3-662-44584-6_15

  20. Visibly Pushdown Transducers with Well-nested Outputs. Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 18th International Conference on Developments in Language Theory (DLT'14), pages 129–141, volume 8633 of Lecture Notes in Computer Science. Springer. 2014.
    DOI: 10.1007/978-3-319-09698-8_12

  21. Expressiveness of Visibly Pushdown Transducers. Mathieu Caralp, Emmanuel Filiot, Pierre-Alain Reynier, Frédéric Servais et Jean-Marc Talbot.
    In Proc. 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT'13), pages 17–26, volume 134. EPTCS. 2013.
    DOI: 10.4204/EPTCS.134.3

  22. Robust Controller Synthesis in Timed Automata. Ocan Sankur, Patricia Bouyer, Nicolas Markey et Pierre-Alain Reynier.
    In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), pages 546–560, volume 8052 of Lecture Notes in Computer Science. Springer. 2013.
    DOI: 10.1007/978-3-642-40184-8_38

  23. Trimming Visibly Pushdown Automata. Mathieu Caralp, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 18th International Conference on Implementation and Application of Automata (CIAA'13), pages 84–96, volume 7982 of Lecture Notes in Computer Science. Springer. 2013.
    DOI: 10.1007/978-3-642-39274-0_9

  24. From Two-Way to One-Way Finite State Transducers. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier et Frédéric Servais.
    In Proc. 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), pages 468–477. IEEE Computer Society. 2013.
    DOI: 10.1109/LICS.2013.53

  25. Robustness of Time Petri Nets under Guard Enlargement. S. Akshay, Loic Hélouet, Claude Jard et Pierre-Alain Reynier.
    In Proc. 6th International Workshop on Reachability Problems (RP'12), pages 92–106, volume 7550 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-33512-9_9

  26. Controllers with Minimal Observation Power (Application to Timed Systems). Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Jean-Francois Raskin et Pierre-Alain Reynier.
    In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), pages 223–237, volume 7561 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-33386-6_19

  27. Visibly Pushdown Automata with multiplicities: Finiteness and K-Boundedness. Mathieu Caralp, Pierre-Alain Reynier et Jean-Marc Talbot.
    In Proc. 16th International Conference on Developments in Language Theory (DLT'12), pages 226–238, volume 7410 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-31653-1_21

  28. Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier et Frédéric Servais.
    In Proc. 31st Annual International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), pages 312–324, volume 13 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2011.
    DOI: 10.4230/LIPIcs.FSTTCS.2011.312

  29. A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems. Janusz Malinowski, Peter Niebert et Pierre-Alain Reynier.
    In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), pages 198–212, volume 6996 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-24372-1_15

  30. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. Pierre-Alain Reynier et Frédéric Servais.
    In Proc. 32nd International Conference on Application and Theory of Petri Nets and Concurrency (ICATPN'11), pages 69–88, volume 6709 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-21834-7_5

  31. Quantitative Robustness Analysis of Flat Timed Automata. Rémi Jaubert et Pierre-Alain Reynier.
    In Proc. 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), pages 229–244, volume 6604 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-19805-2_16

  32. Properties of Visibly Pushdown Transducers. Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier Reynier, Frédéric Servais et Jean-Marc Talbot.
    In Proc. 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10), pages 355–367, volume 6281 of Lecture Notes in Computer Science. Springer. 2010.
    DOI: 10.1007/978-3-642-15155-2_32

  33. Weak Time Petri Nets strike back!. Pierre-Alain Reynier et Arnaud Sangnier.
    In Proc. 20th International Conference on Concurrency Theory (CONCUR'09), pages 557–571, volume 5710 of Lecture Notes in Computer Science. Springer. 2009.
    DOI: 10.1007/978-3-642-04081-8_37

  34. Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. Franck Cassez, Jan J. Jessen, Kim G. Larsen, Jean-François Raskin et Pierre-Alain Reynier.
    In Proc. 12th International Conference on Hybrid Systems: Computation and Control (HSCC'09), pages 90–104, volume 5469 of Lecture Notes in Computer Science. Springer. 2009.
    DOI: 10.1007/978-3-642-00602-9_7

  35. Robust Analysis of Timed Automata via Channel Machines. Patricia Bouyer, Nicolas Markey et Pierre-Alain Reynier.
    In Proc. 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 157–171, volume 4962 of Lecture Notes in Computer Science. Springer. 2008.
    DOI: 10.1007/978-3-540-78499-9_12

  36. Timed Unfoldings for Networks of Timed Automata. Patricia Bouyer, Serge Haddad et Pierre-Alain Reynier.
    In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), pages 292–306, volume 4218 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11901914_23

  37. Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences. Patricia Bouyer, Serge Haddad et Pierre-Alain Reynier.
    In Proc. 33rd International Colloquium on Automata, Languages and Programming (ICALP'06), pages 420–431, volume 4052 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11787006_36

  38. Extended Timed Automata and Time Petri Nets. Patricia Bouyer, Serge Haddad et Pierre-Alain Reynier.
    In Proc. 6th International Conference on Application of Concurrency to System Design (ACSD'06), pages 91–100. IEEE Computer Society Press. 2006.
    DOI: 10.1109/ACSD.2006.6

  39. Robust Model-Checking of Linear-Time Properties in Timed Automata. Patricia Bouyer, Nicolas Markey et Pierre-Alain Reynier.
    In Proc. 7th Latin American Symposium on Theoretical Informatics (LATIN'06), pages 238–249, volume 3887 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11682462_25

  40. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. Patricia Bouyer, François Laroussinie et Pierre-Alain Reynier.
    In Proc. 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'05), pages 112–126, volume 3829 of Lecture Notes in Computer Science. Springer. 2005.
    DOI: 10.1007/11603009_10

Contributions invitées

  1. Robustness of Timed Systems. Pierre-Alain Reynier.
    In Actes de la 11ème Ecole d'été sur la Modélisation et la Vérification des Systèmes Parallèles (MOVEP'14), pages 64–68. 2014. Invited paper


  2. Implémentabilité des automates temporisés. Karine Altisen, Nicolas Markey, Pierre-Alain Reynier et Stavros Tripakis.
    In Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05), pages 395–406. Hermès. 2005. Invited paper

Conférences internationales sans actes

  1. On Characteristic Formulae for Event-Recording Automata. Omer-Landry Nguena-Timo et Pierre-Alain Reynier.
    In Proc. Workshop on Fixpoints In Computer Science (FICS'09), pages 70–78. 2009.


  2. Forward Analysis of Timed Automata. Pierre-Alain Reynier.
    In Proc. 5th Winter School on Modelling and Verifying Parallel Processes (MOVEP'04), pages 52–57. 2004.

Thèses

  1. Contributions to timed systems and transducers. Pierre-Alain Reynier.
    Habilitation à diriger des recherches. Laboratoire d'informatique fondamentale de Marseille, Aix-Marseille Université, France. 2015.


  2. Vérification de systèmes temporisés et distribués : modèles, algorithmes et implémentabilité. Pierre-Alain Reynier.
    Thèse de doctorat. Laboratoire Spécification et Vérification, ENS Cachan, France. 2007.


  3. Analyse en avant des automates temporisés. Pierre-Alain Reynier.
    Master Thesis. DEA Algorithmique, Paris. 2004.

Autres publications

  1. Diagonal constraints handled efficiently in UppAal. Pierre-Alain Reynier.
    Research Report. Numéro LSV-07-02. Laboratoire Spécification et Vérification, ENS Cachan, France. 2007.