Selected publications at LSV: 2002

Books

S. Demri and E. Orłowska. Incomplete Information: Structure, Inference, Complexity. EATCS Monographs. Springer, 2002. ( Web page | BibTeX )

Chapters in Books

R. Hennicker, H. Hußmann and M. Bidoit. On the Precise Meaning of OCL Constraints. In Object Modeling with the OCL - The Rationale behind the Object Constraint Language, LNCS 2263, pages 69-84. Springer, 2002. ( PS | PS.GZ | BibTeX )

Edited Books

J. Goubault-Larrecq (ed.). Special Issue on Models and Methods for Cryptographic Protocol Verification. Journal of Telecommunications and Information Technology 4/2002, 2002. ( Web page | BibTeX )

J. Goubault-Larrecq (ed.). Actes du 1er Workshop International sur la Sécurité des Communications sur Internet (SECI'02), Tunis, Tunisia, September 2002. INRIA. ( Web page | BibTeX )

Journals

P. Bouyer and A. Petit. A Kleene/Büchi-like Theorem for Clock Languages. Journal of Automata, Languages and Combinatorics 7(2), pages 167-186, 2002. ( PS | PS.GZ | BibTeX + Abstract )

H. Comon and V. Shmatikov. Is it Possible to Decide whether a Cryptographic Protocol is Secure or not? Journal of Telecommunications and Information Technology 4/2002, pages 5-15, 2002. ( PDF | BibTeX )

S. Demri and U. Sattler. Automata-Theoretic Decision Procedures for Information Logics. Fundamenta Informaticae 53(1), pages 1-22, 2002. ( PDF | PS | PS.GZ | BibTeX )

J. Goubault-Larrecq. Sécurité, modélisation et analyse de protocoles cryptographiques. Phœbus, la revue de la sûreté de fonctionnement 20, 2002. ( DOC | BibTeX )

P. Bouyer. A Logical Characterization of Data Languages. Information Processing Letters 84(2), pages 75-85, 2002. ( PS | PS.GZ | BibTeX )

V. Cortier. About the Decision of Reachability for Register Machines. Informatique Théorique et Applications 36(4), pages 341-358, 2002. ( PS | PS.GZ | BibTeX )

E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. D. Mosses, D. Sannella and A. Tarlecki. CASL: The Common Algebraic Specification Language. Theoretical Computer Science 286(2), pages 153-196, 2002. ( PS | PS.GZ | BibTeX )

Ph. Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5), pages 251-261, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )

L. Aceto and F. Laroussinie. Is Your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics. Journal of Logic and Algebraic Programming 52-53, pages 7-51, 2002. ( PS | PS.GZ | BibTeX )

M. Bidoit, D. Sannella and A. Tarlecki. Architectural Specifications in CASL. Formal Aspects of Computing 13(3-5), pages 252-273, 2002. ( PS | PS.GZ | BibTeX )

A. Labroue and Ph. Schnoebelen. 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 )

S. Demri and Ph. Schnoebelen. 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 )

D. Lugiez and Ph. Schnoebelen. The Regular Viewpoint on PA-Processes. Theoretical Computer Science 274(1-2), pages 89-115, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )

Conferences

S. Demri and D. D'Souza. An Automata-Theoretic Approach to Constraint LTL. In FSTTCS'02, LNCS 2556, pages 121-132. Springer, 2002. ( PS | PS.GZ | BibTeX )

A. Finkel and J. Leroux. How To Compose Presburger-Accelerations: Applications to Broadcast Protocols. In FSTTCS'02, LNCS 2556, pages 145-156. Springer, 2002. ( PS | PS.GZ | BibTeX )

L. M. Kristensen, J. Billington, L. Petrucci, Z. H. Qureshi and R. Kiefer. Formal specification and analysis of airborne mission systems. In DASC'02, pages 4.D.4.1-4.D.4.13. IEEE Aerospace and Electronic Systems Society, 2002. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq. Higher-Order Positive Set Constraints. In CSL'02, LNCS 2471, pages 473-489. Springer, 2002. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq, S. Lasota and D. Nowak. Logical Relations for Monadic Types. In CSL'02, LNCS 2471, pages 553-568. Springer, 2002. ( PS | PS.GZ | BibTeX )

S. Hornus and Ph. Schnoebelen. On Solving Temporal Logic Queries. In AMAST'02, LNCS 2422, pages 163-177. Springer, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )

M. Bidoit, D. Sannella and A. Tarlecki. Global Development via Local Observational Construction Steps. In MFCS'02, LNCS 2420, pages 1-24. Springer, 2002. Invited paper. ( PS | PS.GZ | BibTeX )

M. Duflot, L. Fribourg and C. Picaronny. Randomized Dining Philosophers without Fairness Assumption. In IFIP TCS'02, IFIP Conference Proceedings 223, pages 169-180. Kluwer Academic Publishers, 2002. ( PS | PS.GZ | BibTeX )

A. Finkel, J.-F. Raskin, M. Samuelides and L. Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In INFINITY'02, ENTCS 68(6), pages 121-144. Elsevier Science Publishers, 2002. ( PS | PS.GZ | BibTeX )

S. Lasota. Decidability of Strong Bisimilarity for Timed BPP. In CONCUR'02, LNCS 2421, pages 562-578. Springer, 2002. ( PS | PS.GZ | BibTeX )

N. Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In EXPRESS'02, ENTCS 68(2), pages 87-104. Elsevier Science Publishers, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )

B. Masson and Ph. Schnoebelen. 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 )

F. Laroussinie, N. Markey and Ph. Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Computer Society Press, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )

L. Petrucci, L. M. Kristensen, J. Billington and Z. H. Qureshi. Towards Formal Specification and Analysis of Avionics Mission Systems. In Proceedings of the Workshops on Software Ingineering and Formal Methods and Formal Methods Applied to Defence Systems, Adelaide, Australia, June 2002, Conferences in Research and Practice in Information Technology 12, pages 95-104. Australian Computer Society, 2002. ( PS | PS.GZ | BibTeX )

M. Bidoit and R. Hennicker. On the Integration of Observability and Reachability Concepts. In FoSSaCS'02, LNCS 2303, pages 21-36. Springer, 2002. ( PS | PS.GZ | BibTeX )

F. Herbreteau, F. Cassez, A. Finkel, O. F. Roux and G. Sutre. Verification of Embedded Reactive Fiffo Systems. In LATIN'02, LNCS 2286, pages 400-414. Springer, 2002. ( PS | PS.GZ | BibTeX )

F. Laroussinie, N. Markey and Ph. Schnoebelen. 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 )

S. Demri, F. Laroussinie and Ph. Schnoebelen. 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 )

Theses

B. Blanc. Prise en compte de principes architecturaux lors de la formalisation des besoins. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2002. ( PS | PS.GZ | BibTeX )

E. Fleury. Automates temporisés avec mises à jour. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2002. ( PS | PS.GZ | BibTeX )

L. Petrucci. Modélisation, vérification et applications. Mémoire d'habilitation, Université d'Évry, France, December 2002. ( PS | PS.GZ | BibTeX )

F. Magniette. Preuves d'algorithmes auto-stabilisants. Thèse de doctorat, Université Paris-Sud 11, Orsay, France, June 2002. ( PS | PS.GZ | BibTeX )

B. Bérard. Vérification de modèles temporisés. Mémoire d'habilitation, Université Paris 7, Paris, France, April 2002. ( PS | PS.GZ | BibTeX )

P. Bouyer. Modèles et algorithmes pour la vérification des systèmes temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, April 2002. ( PDF | PS | PS.GZ | BibTeX )

A. Labroue. Méthodes algébriques pour la vérification des systèmes infinis. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2002. ( PS | PS.GZ | BibTeX )

Other Publications

R. Lazic and D. Nowak. On a Semantic Definition of Data Independence. Research Report CS-RR-392, Department of Computer Science, University of Warwick, UK, December 2002. 19 pages. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq. Un algorithme pour l'analyse de logs. Research Report LSV-02-18, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2002. 33 pages. ( PS | PS.GZ | BibTeX )

M. Baclet. Langages de données. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002. ( PS | PS.GZ | BibTeX )

M. Baudet. Contrôle de ressource et évitement des interblocages sur la mémoire. Rapport de DEA, DEA Programmation, Paris, France, September 2002. ( PDF | PS | PS.GZ | BibTeX )

V. Bernat. Transformation de l'authentification en secret. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002. ( BibTeX )

N. Bertrand. Vérification de canaux à pertes stochastiques. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002. ( PS | PS.GZ | BibTeX )

L. Fribourg, S. Messika and C. Picaronny. Traces of Randomized Distributed Algorithms as Gibbs Fields. Research Report LSV-02-12, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2002. 16 pages. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq. Vérification de protocoles cryptographiques: la logique à la rescousse! In SECI'02, pages 119-152. INRIA, 2002. Invited paper. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq and K. N. Verma. Alternating Two-Way AC-Tree Automata. Research Report LSV-02-11, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2002. 21 pages. ( PS | PS.GZ | BibTeX )

S. Lasota. A Polynomial-Time Algorithm for Deciding True Concurrency Equivalences of Basic Parallel Processes. Research Report LSV-02-13, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2002. 16 pages. ( PS | PS.GZ | BibTeX )

S. Messika. Vérification paramétrée de réseaux à processus probabiliste. Application du théorème de Hammersley et Clifford aux algorithmes distribués. Rapport de DEA, DEA Logique et Fondements de l'Informatique, Paris, France, September 2002. ( PS | PS.GZ | BibTeX )

Y. Zhang. Logical Relations For Names. Rapport de DEA, DEA Programmation, Paris, France, September 2002. ( PS | PS.GZ | BibTeX )

B. Bérard, P. Bouyer and A. Petit. Analysing the PGM Protocol with UPPAAL. In RT-TOOLS'02. Uppsala University, 2002. Published as Technical Report 2002-025, Department of Information Technology, Uppsala University, Sweden. ( PS | PS.GZ | BibTeX + Abstract )

J. Goubault-Larrecq. SKInT Labels. Research Report LSV-02-7, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 15 pages. ( PS | PS.GZ | BibTeX )

J. Goubault-Larrecq. A Note on the Completeness of Certain Refinements of Resolution. Research Report LSV-02-8, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 16 pages. ( PS | PS.GZ | BibTeX )

A. Boisseau. Signatures électroniques de contrats. Research Report LSV-02-4, Laboratoire Spécification et Vérification, ENS Cachan, France, April 2002. 22 pages. ( PS | PS.GZ | BibTeX )

V. Cortier. Observational Equivalence and Trace Equivalence in an Extension of Spi-calculus. Application to Cryptographic Protocols Analysis. Extended Version. Research Report LSV-02-3, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2002. 33 pages. ( PS | PS.GZ | BibTeX )

About LSV

Select by Year

Search this list

Search the LSV database

List of coauthors