1999-2025 Publications

• 2025
  • A. Duret‑Lutz, D. Poitrenaud, Y. Thierry‑Mieg : “Simplifying LTL Model Checking Given Prior Knowledge”, Application and Theory of Petri Nets and Concurrency, vol. 15714, Lecture Notes in Computer Science, Paris, France, pp. 433-456, (Springer Nature Switzerland), (ISBN: 978-3-031-94634-9) (2025)
• 2022
  • E. Paviot‑Adet, D. Poitrenaud, E. Renault, Y. Thierry‑Mieg : “LTL under reductions with weaker conditions than stutter-invariance”, Lecture Notes in Computer Science (LNCS), vol. 13273, Formal Techniques for Distributed Objects, Components, and Systems, Lucca, Italy, pp. 170–187, (Springer Cham), (ISBN: 978-3-031-08679-3) (2022)
• 2019
  • D. Poitrenaud, E. Renault : “Combining Parallel Emptiness Checks with Partial Order Reductions”, ICFEM 2019 - 21^st International Conference on Formal Engineering Methods, vol. 11852, Lecture Notes in Computer Science, Shenzhen, China, pp. 370-386, (Springer) (2019)
• 2017
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata”, International Journal on Software Tools for Technology Transfer, vol. 19 (6), pp. 653-673, (Springer Verlag) (2017)
• 2016
  • A. Duret‑Lutz, F. Kordon, D. Poitrenaud, E. Renault : “Heuristics for Checking Liveness Properties with Partial Order Reductions”, Automated Technology for Verification and Analysis, vol. 9938, Lecture Notes in Computer Science, Chiba, Japan, pp. 340-356, (Springer) (2016)
• 2015
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Parallel Explicit Model Checking for Generalized Büchi Automata”, 21^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, vol. 9035, Lecture Notes in Computer Science, London, United Kingdom, pp. 613-627, (Springer) (2015)
• 2013
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Three SCC-based Emptiness Checks for Generalized Büchi Automata”, Proceedings of the 19^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), vol. 8312, Lecture Notes in Computer Science, Stellenbosch, South Africa, pp. 668-682, (Springer) (2013)
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking”, Proceedings of the 19^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), vol. 7795, Lecture Notes in Computer Science, Rome, Italy, pp. 580-593, (Springer) (2013)
  • J.‑M. Couvreur, D. Poitrenaud, P. Weil : “Branching processes of general Petri nets”, Fundamenta Informaticae, vol. 122 (1-2), pp. 31-58, (IOS Press) (2013)
• 2012
  • K. Barkaoui, B. Monsuez, D. Poitrenaud : “Special Issue on Verification and Evaluation of Computer and Communication Systems - Part II”, International Journal of Critical Computer-Based Systems, vol. 3, (Inderscience) (2012)
• 2011
  • A. Duret‑Lutz, K. Klai, D. Poitrenaud, Y. Thierry‑Mieg : “Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking”, 9^th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), vol. 6996, Lecture Notes in Computer Science, Taipei, Taiwan, Province of China, pp. 336-350, (Springer) (2011)
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
  • J.‑M. Couvreur, D. Poitrenaud, P. Weil : “Branching Processes of General Petri Nets”, Petri Nets 2011 - 32^nd International Conference on Petri Nets and Other Models of Concurrency, vol. 6709, Lecture Notes in Computer Science, Newcastle, United Kingdom, pp. 129-148, (Springer) (2011)
  • K. Barkaoui, B. Monsuez, D. Poitrenaud : “Special Issue on Verification and Evaluation of Computer and Communication Systems - Part I”, International Journal of Critical Computer-Based Systems, vol. 2, (Inderscience) (2011)
  • S. Demri, D. Poitrenaud : “Verification of Infinite-State Systems”, chapter in Models and Analysis in Distributed Systems, pp. 221-269, (Wiley), (ISBN: 9781848213142) (2011)
• 2010
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1^st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
• 2009
  • Y. Thierry‑Mieg, D. Poitrenaud, A. Hamez, F. Kordon : “Hierarchical Set Decision Diagrams and Regular Models”, 15^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 5505, Lecture Notes in Computer Science, York, United Kingdom, pp. 1-15, (Springer) (2009)
  • A. Duret‑Lutz, D. Poitrenaud, J.‑M. Couvreur : “On-the-fly Emptiness Check of Transition-Based Streett Automata”, 7^th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, vol. 5799, Lecture Notes in Computer Science, Macao, China, pp. 213-227, (Springer) (2009)
  • S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24^th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
  • J.‑M. Couvreur, D. Poitrenaud : “Petri Net Unfoldings -- Properties”, chapitre de Petri Nets. Fundamental Models, Verification and Applications, pp. 415-434, (Wiley) (2009)
• 2008
  • K. Klai, D. Poitrenaud : “MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs”, 29^th International Conference on Application and Theory of Petri Nets (ICATPN'08), vol. 5062, Lecture Notes in Computer Science, Xian, China, pp. 288-306, (Springer-Verlag) (2008)
• 2007
  • S. Haddad, D. Poitrenaud : “Recursive Petri nets - Theory and application to discrete event systems”, Acta Informatica, vol. 44 (7-8), pp. 463-508, (Springer Verlag) (2007)
• 2006
  • F. Peschanski, D. Poitrenaud : “Vérification de systèmes infinis”, chapitre de Méthodes formelles pour les systèmes répartis et coopératifs, IC2 Series, pp. 213-250, (Hermès Lavoisier), (ISBN: 2-7462-1447-4) (2006)
• 2005
  • J.‑M. Couvreur, A. Duret‑Lutz, D. Poitrenaud : “On-the-Fly Emptiness Checks for Generalized Büchi Automata”, 12^th International SPIN Workshop on Model Checking of Software, vol. 3639, Lecture Notes in Computer Science, San Francisco, United States, pp. 169-184, (Springer-Verlag) (2005)
• 2004
  • F. Gilliers, F. Bréant, D. Poitrenaud, F. Kordon : “Model Checking of Highlevelobject Oriented Specifications : The LfP Experience”, 3^rd Workshop on Modelling of Objects, Components, and Agents (MOCA '04), Aarhus, Denmark, pp. 149-168 (2004)
  • A. Duret‑Lutz, D. Poitrenaud : “SPOT: an Extensible Model Checking Library using Transition-based Generalized Büchi Automata”, 12^th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Volendam, Netherlands, pp. 76-83, (IEEE Computer Society Press) (2004)
  • Y. Thierry‑Mieg, J.‑M. Ilié, D. Poitrenaud : “A Symbolic Symbolic State Space Representation”, 24^th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE '04), vol. 3235, Lecture Notes in Computer Science, Madrid, Spain, pp. 276-291, (Springer-Verlag) (2004)
  • F. Bréant, J.‑M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot‑Adet, D. Poitrenaud, D. Regep, G. Sutre : “Modeling and Verifying Behavioral Aspects”, chapter in Formal Methods for Embedded Distributed Systems - How to master the complexity, pp. 171-211, (Kluwer Academic Publishers), (ISBN: 1-4020-7996-6) (2004)
• 2003
  • J.‑M. Couvreur, D. Poitrenaud : “Dépliages pour la vérification de propriétés temporelles”, chapitre de Vérification et mise en oeuvre des réseaux de Petri, pp. 127-162, (Hermes Science Publications), (ISBN: 2-7462-0445-2) (2003)
  • C. Dutheillet, J.‑M. Ilié, D. Poitrenaud, I. Vernier‑Mounier : “State-Space-Based Methods and Model Checking”, chapter in Petri nets for Systems Engineering : A Guide to Modeling, Verification, and Applications, pp. 201-275, (Springer-Verlag), (ISBN: 3-540-41217-4) (2003)
• 2002
  • J.‑M. Couvreur, E. Encrenaz, E. Paviot‑Adet, D. Poitrenaud, P.‑A. Wacrenier : “Data Decision Diagrams for Petri Net analysis”, 23^th International Conference on Application and Theory of Petri Nets, vol. 2360, Lecture Notes in Computer Science, Adelaide, Australia, pp. 101-120, (Springer-Verlag) (2002)
• 2001
  • S. Haddad, D. Poitrenaud : “Checking Linear Temporal Formulas on Sequential Recursive Petri Nets”, 8^th International Symposium on Temporal Representation and Reasonning (TIME-01), Cividale del Friuli, Italy, pp. 198-205, (IEEE) (2001)
  • J.‑M. Couvreur, S. Grivet, D. Poitrenaud : “Unfolding of Products of Symmetrical Petri Nets”, 22^th International Conference on Applications and Theory of Petri Nets, vol. 2075, Lecture Notes in Computer Science, Newcastle upon Tyne, United Kingdom, pp. 121-143, (Springer-Verlag) (2001)
  • L. Arantes, D. Poitrenaud, P. Sens, B. Folliot : “The Barrier-Lock Clock: A Scalable Synchronisation-oriented Logical Clock”, Parallel Processing Letters, vol. 11 (1), pp. 65-76, (World Scientific Publishing) (2001)
• 2000
  • S. Haddad, D. Poitrenaud : “A model checking decision procedure for sequential recursive Petri nets”, (2000)
  • S. Haddad, D. Poitrenaud : “Modelling and Analyzing Systems with Recursive Petri Nets”, 5^th Workshop on Discrete Event Systems (WODES '2000), vol. 569, The Springer International Series in Engineering and Computer Science, Ghent, Belgium, pp. 449-458, (Kluwer Academic Publishers) (2000)
  • J.‑M. Couvreur, S. Grivet, D. Poitrenaud : “Designing a LTL Model-Checker based on Unfolding Graphs”, 21^th International Conference on Applications and Theory of Petri Nets, vol. 1825, Lecture Notes in Computer Science, Aarhus, Denmark, pp. 123-145, (Springer) (2000)
  • D. Poitrenaud, J.‑F. Pradat‑Peyre : “Pre and post-agglomerations for LTL model checking”, 21^th International Conference on Applications and Theory of Petri Nets, vol. 1825, Lecture Notes in Computer Science, Aarhus, Denmark, pp. 387-408, (Springer) (2000)
• 1999
  • S. Haddad, D. Poitrenaud : “Decidability and Undecidability Results for Recursive Petri Nets”, (1999)
  • J.‑M. Couvreur, D. Poitrenaud : “Detection of Illegal Behaviours Based on Unfoldings”, 20^th International Conference on Application and Theory of Petri Nets, vol. 1639, Lecture Notes in Computer Science, Williamsburg, Virginia, United States, pp. 364-383, (Springer-Verlag) (1999)
  • S. Haddad, D. Poitrenaud : “Theoretical Aspects of Recursive Petri Nets”, 20^th International Conference on Application and Theory of Petri Nets, vol. 1639, Lecture Notes in Computer Science, Williamsburg, Virginia, United States, pp. 228-247, (Springer-Verlag) (1999)