Coordonnées

Projets en cours

• Spot : une bibliothèque C++ pour le "model-checking"
• FME3 : un  projet ANR "Sécurité et sûreté informatique"

Publications

[DLKPTM11b]

Alexandre Duret-Lutz, Kaïs Klai, Denis Poitrenaud, and Yann Thierry-Mieg. Self-Loop Aggregation Product - a new hybrid approach to on-the-fly LTL model checking. In 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of Lecture Notes in Computer Science, pages 336-350, Taipei, Taiwan, October 2011. Springer.
[ bib ]

[CPW11]

Jean-Michel Couvreur, Denis Poitrenaud, and Pascal Weil. Branching processes of general Petri nets. In 32nd International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2011), volume 6709 of Lecture Notes in Computer Science, pages 129-148, Newcastle, UK, June 2011. Springer.
[ bib ]

[DP11]

Stéphane Demri and Denis Poitrenaud. Models and Analysis in Distributed Systems - Verification of Infinite-State Systems, chapter 8, pages 221-269. Wiley, 2011.
[ bib ]

[BBE⁺11]

Soheib Baarir, Cécile Braunstein, Emmanuelle Encrenaz, Jean-Michel Ilié, Tun Li, Isabelle Mounier, Denis Poitrenaud, and Sana Younes. Feasibility analysis for robustness quantification by symbolic model checking. Formal Methods in System Design, pages 1-20, 2011.
[ bib ]

[DLKPTM11a]

Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, and Yann Thierry-Mieg. Combining explicit and symbolic approaches for better on-the-fly LTL model checking. Technical Report abs/1106.5700, CoRR, 2011.
[ bib | http ]

[BMP11]

Kamel Barkaoui, Bruno Monsuez, and Denis Poitrenaud, editors. Special Issue on Verification and Evaluation of Computer and Communication Systems -– Part I, volume 2 of International Journal on Critical Computer-Based Systems. Inderscience Enterprises Ltd, 2011.
[ bib ]

[BBE⁺10]

Soheib Baarir, Cécile Braunstein, Emmanuelle Encrenaz, Jean-Michel Ilié, Tun Li, Isabelle Mounier, Denis Poitrenaud, and Sana Younes. Quantifying robustness by symbolic model checking. In Proc. 1st Hardware Verification Workshop (affiliated with CAV'10), Edinburgh, United Kingdom, July 2010.
[ bib ]

[DLPC09]

Alexandre Duret-Lutz, Denis Poitrenaud, and Jean-Michel Couvreur. On-the-fly emptiness check of transition-based Streett automata. In Proc. 7th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, Macao SAR, China, October 2009. Springer.
[ bib ]

[BBC⁺09]

Soheib Baarir, Cécile Braunstein, Renaud Clavel, Emmanuelle Encrenaz, Jean-Michel Ilié, Régis Leveugle, Isabelle Mounier, Laurence Pierre, and Denis Poitrenaud. Complementary formal approaches for dependability analysis. In Proc. 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems. IEEE Computer Society, October 2009.
[ bib ]

[TMPHK09]

Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Hamez, and Fabrice Kordon. Hierarchical set decision diagrams and regular models. In Stefan Kowalewski and Anna Philippou, editors, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of Lecture Notes in Computer Science, pages 1-15. Springer, March 2009.
[ bib | .pdf ]

[CP09]

Jean-Michel Couvreur and Denis Poitrenaud. Petri net unfoldings - properties. In Michel Diaz, editor, Petri Nets: Fundamental Models, Verification and Applications, pages 315-434. Wiley-ISTE, 2009.
[ bib ]

[KP08]

Kais Klai and Denis Poitrenaud. MC-SOG: An LTL model checker based on symbolic observation graphs. In Proceedings of the 29th International Conference on Application and Theory of Petri Nets (ICATPN'08), volume 5062 of Lecture Notes in Computer Science, pages 288–-306, Xi'an, China, June 2008. Springer Verlag.
[ bib | .pdf ]

[HP07]

Serge Haddad and Denis Poitrenaud. Recursive Petri nets - Theory and application to discrete event systems. Acta Informatica, 44(7-8):463-508, December 2007.
[ bib | .pdf ]

[PP06]

Frédéric Peschanski and Denis Poitrenaud. Méthodes Formelles pour les Systèmes Répartis et Coopératifs - Vérification de Systèmes Infinis, chapter 9, pages 213-249. Traité IC2 - Série Informatique et Système. Hermès Science Publications, 2006. ISBN 2-7462-1447-4.
[ bib ]

[CDLP05]

Jean-Michel Couvreur, Alexandre Duret-Lutz, and Denis Poitrenaud. On-the-fly emptiness checks for generalized Büchi automata. In Proceedings of the 12th International SPIN Workshop on Model Checking of Software (SPIN'05), Lecture Notes in Computer Science. Springer, August 2005.
[ bib | .pdf ]

[DLP04]

Alexandre Duret-Lutz and Denis Poitrenaud. Spot: an extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 76-83, Volendam, The Netherlands, October 2004. IEEE Computer Society Press.
[ bib | .pdf ]

[GBPK04]

Frédéric Gilliers, François Bréant, Denis Poitrenaud, and Fabrice Kordon. Model checking of high-level object oriented specifications: the experience. In Proceedings of the 3rd Workshop on Modelling of Objects, Components, and Agents (MOCA’04), pages 149-168, October 2004.
[ bib ]

[TMIP04]

Yann Thierry-Mieg, Jean-Michel Ilié, and Denis Poitrenaud. A symbolic symbolic state space representation. In David de Frutos-Escrig and Manuel Núñez, editors, Proceedings of the 24th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'04), volume 3235 of Lecture Notes in Computer Science, pages 276-291. Springer, September 2004.
[ bib | .pdf ]

[BCG⁺04]

François Bréant, Jean-Michel Couvreur, Frédéric Gilliers, Fabrice Kordon, Isabelle Mounier, Emmanuel Paviot-Adet, Denis Poitrenaud, Dan Regep, and Grégoire Sutre. Formal Methods for Embedded Distributed Systems - How to master the complexity - Modeling and Verifying Behavioral Aspects, pages 171-211. Kluwer Academic Publishers, 2004.
[ bib ]

[CP03]

Jean-Michel Couvreur and Denis Poitrenaud. Vérification et Mise en Oeuvre des Réseaux de Petri - Dépliages pour la Vérification de Propriétés Temporelles, chapter 3, pages 127-162. Hermès Science Publications, 2003. ISBN 2-7462-0445-2.
[ bib ]

[DIPVM02]

Claude Dutheillet, Jean-Michel Ilié, Denis Poitrenaud, and Isabelle Vernier-Mounier. Petri Nets for Systems Engineering, A Guide to Modeling, Verification, and Applications - State-Space-Based Methods and Model Checking, chapter 14, pages 201-276. Springer Verlag, July 2002. ISBN 3-540-41217-4.
[ bib ]

[CEPA⁺02]

Jean-Michel Couvreur, Emmanuelle Encrenaz, Emmanuel Paviot-Adet, Denis Poitrenaud, and Pierre-André Wacrenier. Data decision diagrams for Petri net analysis. In Proceedings of the 23th International Conference on Application and Theory of Petri Nets (ICATPN'02), volume 2360 of Lecture Notes in Computer Science, pages 101-120, Adelaide, Australia, June 2002. Springer Verlag.
[ bib | .pdf ]

[APSF01]

Luciana Bezerra Arantes, Denis Poitrenaud, Pierre Sens, and Bertil Folliot. The barrier-lock clock: A scalable synchronization-oriented logical clock. Parallel Processing Letters, 11(1):65-76, 2001.
[ bib | .ps ]

[CGP01]

Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding of products of symmetrical Petri nets. In José Manuel Colom and Maciej Koutny, editors, Proceedings of the 22th International Conference on Application and Theory of Petri Nets (ICATPN'01), volume 2075 of Lecture Notes in Computer Science, pages 121-143. Springer Verlag, 2001.
[ bib | .ps ]

[HP01]

Serge Haddad and Denis Poitrenaud. Checking linear temporal formulas on sequential recursive Petri nets. In Proceedings of the 8th International Symposium on Temporal Representation and Reasonning (TIME'01), pages 198-205, Cividale del Friuli, Italie, 2001. IEEE Computer Society.
[ bib | .pdf ]

[HP00a]

Serge Haddad and Denis Poitrenaud. A model checking decision procedure for sequential recursive Petri nets. Technical Report 024, LIP6, Paris VI University, Paris, France, September 2000.
[ bib | .ps ]

[HP00b]

Serge Haddad and Denis Poitrenaud. Modelling and analyzing systems with recursive Petri nets. In Proceedings of the 5th Workshop on Discrete Event Systems (WODES'2000), pages 449-458, Ghent, Belgium, August 2000. Kluwer Academic Publishers.
[ bib | .ps ]

[CGP00]

Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Designing a LTL model-checker based on unfolding graphs. In Proceedings of the 21th International Conference on Applications and Theory of Petri Nets (ICATPN'00), Lecture Notes in Computer Science, Aarhus, Denmark, June 2000. Springer-Verlag.
[ bib | .ps ]

[PPP00]

Denis Poitrenaud and Jean-François Pradat-Peyre. Pre and post-agglomerations for LTL model checking. In Proceedings of the 21th International Conference on Applications and Theory of Petri Nets (ICATPN'00), Lecture Notes in Computer Science, Aarhus, Denmark, June 2000. Springer-Verlag.
[ bib | .pdf ]

[HP99a]

Serge Haddad and Denis Poitrenaud. Decidability and undecidability results for recursive Petri nets. Rapport de Recherche LIP6 1999/019, Université Paris 6 - CNRS - Laboratoire d'informatique de Paris 6, Paris, France, September 1999.
[ bib | .ps ]

[CP99]

Jean-Michel Couvreur and Denis Poitrenaud. Detection of illegal behaviours based on unfoldings. In S. Donatelli and J. Kleijn, editors, Proceedings of the 20th International Conference on Application and Theory of Petri Nets (ICATPN'99), volume 1639 of Lecture Notes in Computer Science, pages 364-383, Williamsburg, Virginia, USA, June 1999. Springer Verlag.
[ bib | .pdf ]

[HP99b]

Serge Haddad and Denis Poitrenaud. Theoretical aspects of recursive Petri nets. In S. Donatelli and J. Kleijn, editors, Proceedings of the 20th International Conference on Application and Theory of Petri Nets (ICATPN'99), volume 1639 of Lecture Notes in Computer Science, pages 228-247, Williamsburg, Virginia, USA, June 1999. Springer Verlag.
[ bib | .ps ]

[Poi96]

Denis Poitrenaud. Graphe de Processus Arborescents pour la Vérification de Propriétés. PhD thesis, Université Pierre et Marie Curie, December 1996.
[ bib ]

[CP96]

Jean-Michel Couvreur and Denis Poitrenaud. Model checking based on occurrence net graph. In Proceedings of the 9th International Conference on Formal Description Techniques for Distributed Systems ans Communication Protocols (FORTE'96), pages 380-396, Kaiserslauter, Germany, 1996. Chapman & Hall.
[ bib ]

[IMP95]

Jean-Michel Ilié, Yasmina Maîsi, and Denis Poitrenaud. Towards an efficient simulation based on well formed Petri nets, extended with inhibitor arcs. In Proceedings of the Summer Computer Simulation Conference (SCSC'95), pages 170-175, Ottawa, Canada, June 1995.
[ bib ]

[BP95]

Robert Brgan and Denis Poitrenaud. An efficient algorithm for the computation of stubborn sets of well formed Petri nets. In G. De Michelis and M. Diaz, editors, Proceedings of the 16th International Conference on Application and Theory of Petri Nets (ICATPN'95), volume 935 of Lecture Notes in Computer Science, pages 121-140, Torino, Italy, June 1995. Springer-Verlag.
[ bib ]

Cette page a été mise à jour le 12 octobre 2011