2010 | |
| • | . Toward a compositional theory of leftist grammars and transformations. In FoSSaCS'10, LNCS 6014, pages 237-251. Springer, 2010. ( PDF | BibTeX + Abstract ) |
2008 | |
| • | . Mixing Lossy and Perfect Fifo Channels. In CONCUR'08, LNCS 5201, pages 340-355. Springer, 2008. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . The Ordinal Recursive Complexity of Lossy Channel Systems. In LICS'08, pages 205-216. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract ) |
| • | . The ω-Regular Post Embedding Problem. In FoSSaCS'08, LNCS 4962, pages 97-111. Springer, 2008. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . On Termination for Faulty Channel Machines. In STACS'08, Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, 2008. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
2007 | |
| • | . Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Transactions on Computational Logic 9(1), 2007. ( Web page | PDF | PS | BibTeX + Abstract ) |
| • | . Post Embedding Problem is not Primitive Recursive, with Applications to Channel Systems. In FSTTCS'07, LNCS 4855, pages 265-276. Springer, 2007. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract ) |
| • | . Model Checking Branching-Time Logics. In TIME'07, page 5. IEEE Computer Society Press, 2007. ( PDF | PS | PS.GZ | Slides | BibTeX ) |
2006 | |
| • | . On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. In LPAR'06, LNAI 4246, pages 347-361. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness. In FORTE'06, LNCS 4229, pages 212-227. Springer, 2006. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. Theoretical Computer Science 358(2-3), pages 315-333, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . A short visit to the STS hierarchy. In EXPRESS'05, ENTCS 154(3), pages 59-69. Elsevier Science Publishers, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . BTL2 and the expressive power of ECTL+. Information and Computation 204(7), pages 1023-1044, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . A Parametric Analysis of the State Explosion Problem in Model Checking. Journal of Computer and System Sciences 72(4), pages 547-575, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Efficient Timed Model Checking for Discrete-Time Systems. Theoretical Computer Science 353(1-3), pages 249-271, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Mu-Calculus Path Checking. Information Processing Letters 97(6), pages 225-230, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . A note on the attractor-property of infinite-state Markov chains. Information Processing Letters 97(2), pages 58-63, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
2005 | |
| • | B. Bouyssonouse and J. Sifakis (eds.). Embedded Systems Design: The ARTIST Roadmap for Research and Development, LNCS 3436. Springer, 2005. ( Web page | BibTeX ) |
| • | . Verification of Probabilistic Systems with Faulty Communication. Information and Computation 202(2), pages 141-165, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Decidable first-order transition logics for PA-processes. Information and Computation 203(1), pages 75-113, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Flat acceleration in symbolic model checking. In ATVA'05, LNCS 3707, pages 474-488. Springer, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
2004 | |
| • | . The Verification of Probabilistic Lossy Channel Systems. In Validation of Stochastic Systems, LNCS 2925, pages 445-465. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Symbolic Model Checking for Simply-Timed Systems. In FORMATS'04/FTRTFT'04, LNCS 3253, pages 102-117. Springer, 2004. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
| • | . TSMV: A Symbolic Model Checker for Quantitative Analysis of Systems. In QEST'04, pages 330-331. IEEE Computer Society Press, 2004. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
| • | . A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. In CONCUR'04, LNCS 3170, pages 372-386. Springer, 2004. ( PDF | BibTeX + Abstract ) |
| • | . Model Checking Timed Automata with One or Two Clocks. In CONCUR'04, LNCS 3170, pages 387-401. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | Ph. Schnoebelen (ed.). Proceedings of the 5th International Workshop on Verification of Infinite State Systems (INFINITY'03), Marseilles, France, September 2003, ENTCS 98. Elsevier Science Publishers, 2004. ( BibTeX ) |
| • | . Verifying Nondeterministic Channel Systems With Probabilistic Message Losses. In AVIS'04. 2004. ( PDF | BibTeX + Abstract ) |
| • | . A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1), pages 3-6, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
2003 | |
| • | . The Complexity of Temporal Logic Model Checking. In AiML'02, pages 393-436. King's College Publication, 2003. Invited paper. ( PDF | PS | PS.GZ | BibTeX ) |
| • | . Model Checking a Path (Preliminary Report). In CONCUR'03, LNCS 2761, pages 251-265. Springer, 2003. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
| • | . Oracle circuits for branching-time model checking. In ICALP'03, LNCS 2719, pages 790-801. Springer, 2003. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Model Checking Lossy Channels Systems Is Probably Decidable. In FoSSaCS'03, LNCS 2620, pages 120-135. Springer, 2003. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . On the Expressivity and Complexity of Quantitative Branching-Time Temporal Logics. Theoretical Computer Science 297(1-3), pages 297-315, 2003. ( PS | PS.GZ | BibTeX + Abstract ) |
2002 | |
| • | . On Solving Temporal Logic Queries. In AMAST'02, LNCS 2422, pages 163-177. Springer, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5), pages 251-261, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . On Verifying Fair Lossy Channel Systems. In MFCS'02, LNCS 2420, pages 543-555. Springer, 2002. ( PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems. Nordic Journal of Computing 9(2), pages 118-144, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Computer Society Press, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
| • | . The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1), pages 84-103, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, LNCS 2303, pages 264-279. Springer, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
| • | . A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract). In STACS'02, LNCS 2285, pages 620-631. Springer, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . The Regular Viewpoint on PA-Processes. Theoretical Computer Science 274(1-2), pages 89-115, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
2001 | |
| • | . Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001. ( Web page | BibTeX ) |
| • | . Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems. In TACS'01, LNCS 2215, pages 385-399. Springer, 2001. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Spécification et vérification des systèmes concurrents. Mémoire d'habilitation, Université Paris 7, Paris, France, October 2001. ( PS | PS.GZ | BibTeX ) |
| • | . Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2), pages 63-92, 2001. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Model checking CTL+ and FCTL is hard. In FoSSaCS'01, LNCS 2030, pages 318-331. Springer, 2001. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract ) |
2000 | |
| • | . Some Decidability Results for Nested Petri Nets. In PSI'99, LNCS 1755, pages 208-220. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Towards the Automatic Verification of PLC Programs Written in Instruction List. In SMC 2000, pages 2449-2454. Argos Press, 2000. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Safe Programming of PLC Using Formal Verification Methods. In ICP 2000, pages 73-78. PLCopen, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Formal modeling of timed function blocks for the automatic verification of Ladder Diagram programs. In ADPM 2000, pages 177-182. Shaker Verlag, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Un cadre pour la vérification automatique de programmes IL. In CIFA 2000, pages 693-698. Union des Chercheurs Ingénieurs et Scientifiques, Villeneuve d'Ascq, France, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Decidable First-Order Transition Logics for PA-Processes. In ICALP 2000, LNCS 1853, pages 342-353. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Bisimulation and the Reduction of Petri Nets. In ICATPN 2000, LNCS 1825, pages 409-423. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Verifying Performance Equivalence for Timed Basic Parallel Processes. In FoSSaCS 2000, LNCS 1784, pages 35-47. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . The State-Explosion Problem from Trace to Bisimulation Equivalence. In FoSSaCS 2000, LNCS 1784, pages 192-207. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| • | . Specification in CTL+Past for verification in CTL. Information and Computation 156(1-2), pages 236-263, 2000. ( PS | PS.GZ | BibTeX ) |
1999 | |
| • | . Boundedness of Reset P/T Nets. In ICALP'99, LNCS 1644, pages 301-310. Springer, 1999. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Vérification de logiciels : techniques et outils du model-checking. Vuibert, 1999. ( Web page | BibTeX ) |
| • | . Decomposable Regular Languages and the Shuffle Operator. EATCS Bulletin 67, pages 283-289, 1999. ( PS | PS.GZ | BibTeX ) |
1998 | |
| • | . Reset Nets between Decidability and Undecidability. In ICALP'98, LNCS 1443, pages 103-115. Springer, 1998. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Fundamental Structures in Well-Structured Infinite Transition Systems. In LATIN'98, LNCS 1380, pages 102-118. Springer, 1998. ( PS | PS.GZ | BibTeX ) |
1997 | |
| • | . A Model for Recursive-Parallel Programs. In INFINITY'96, ENTCS 5, page 30. Elsevier Science Publishers, 1997. ( PS | PS.GZ | BibTeX ) |
| • | . A Formal Framework for the Analysis of Recursive-Parallel Programs. In PaCT'97, LNCS 1277, pages 45-59. Springer, 1997. ( PS | PS.GZ | BibTeX ) |
1996 | |
| • | . Modèles formels pour les programmes récursifs-parallèles. In RENPAR'96, pages 85-88. 1996. ( PS | PS.GZ | BibTeX ) |
1995 | |
| • | . A Hierarchy of Temporal Logics with Past. Theoretical Computer Science 148(2), pages 303-324, 1995. ( PS | PS.GZ | BibTeX ) |
| • | . Translations between Modal Logics of Reactive Systems. Theoretical Computer Science 140(1), pages 53-71, 1995. ( PS | PS.GZ | BibTeX ) |
1994 | |
| • | . Translation Results for Modal Logics of Reactive Systems. In AMAST'93, Workshops in Computing, pages 299-310. Springer-Verlag, 1994. ( BibTeX ) |
| • | . Place Bisimulations for the Reduction of Labeled Petri Nets with Silent Moves. In ICCI'94, pages 230-246. 1994. ( PS | PS.GZ | BibTeX ) |
| • | . Logical Characterizations of Truly Concurrent Bisimulation. Technical Report 114, Laboratoire d'Informatique Fondamentale et d'Intelligence Artificielle, Grenoble, France, March 1994. ( PS | PS.GZ | BibTeX ) |
| • | . A Hierarchy of Temporal Logics with Past. In STACS'94, LNCS 775, pages 47-58. Springer-Verlag, 1994. ( BibTeX ) |
1992 | |
| • | . Place Bisimulations in Petri Nets. In APN'92, LNCS 616, pages 45-61. Springer-Verlag, 1992. ( BibTeX ) |
1991 | |
| • | . τ-Bisimulations and Full Abstraction for Refinement of Actions. Information Processing Letters 40(4), pages 219-222, 1991. ( BibTeX ) |
| • | . Experiments on Processes with Backtracking. In CONCUR'91, LNCS 527, pages 480-494. Springer-Verlag, 1991. ( BibTeX ) |
| • | . Strong Bisimilarity on Nets Revisited. In PARLE'91, LNCS 506, pages 295-312. Springer-Verlag, 1991. ( BibTeX ) |
| • | . A Rewrite-Based Type Discipline for a Subset of Computer Algebra. Journal of Symbolic Computation 11(4), pages 349-368, 1991. ( BibTeX ) |
1990 | |
| • | . A Net-Theoretic Approach to the Efficient Implementation of the FP2 Parallel Language. In APN'90, pages 451-470. 1990. ( BibTeX ) |
| • | . Sémantique du parallélisme et logique temporelle. Application au langage FP2. Thèse de doctorat, Institut National Polytechnique de Grenoble, France, June 1990. ( BibTeX ) |
| • | . On the Weak Adequacy of Branching-Time Temporal Logic. In ESOP'90, LNCS 432, pages 377-388. Springer-Verlag, 1990. ( BibTeX ) |
1989 | |
| • | . Principles of FP2: Term Algebras for Specification of Parallel Machines. In Languages for Parallel Architectures: Design, Semantics, Implementation Models, chapter 5, pages 223-273. John Wiley & Sons, Ltd., 1989. ( BibTeX ) |
1988 | |
| • | . Refined Compilation of Pattern-Matching for Functional Languages. Science of Computer Programming 11(2), pages 133-159, 1988. ( BibTeX ) |
| • | . Refined Compilation of Pattern-Matching for Functional Languages. In ALP'88, LNCS 343, pages 233-243. Springer-Verlag, 1988. ( BibTeX ) |
1987 | |
| • | . Specification of a Pipelined Event-Driven Simulator Using FP2. In PARLE'87, LNCS 258, pages 311-328. Springer-Verlag, 1987. ( BibTeX ) |
| • | . Rewriting Techniques for the Temporal Analysis of Communicating Processes. In PARLE'87, LNCS 259, pages 402-419. Springer-Verlag, 1987. ( BibTeX ) |