Publications : 2002

[DD02]
S. Demri and D. D'Souza. An Automata-Theoretic Approach to Constraint LTL. In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02), volume 2556 of Lecture Notes in Computer Science, pages 121--132, Kanpur, India, December 2002. Springer.
BibTex | Web page | PS ]
[FL02]
A. Finkel and J. Leroux. How To Compose Presburger-Accelerations: Applications to Broadcast Protocols. In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02), volume 2556 of Lecture Notes in Computer Science, pages 145--156, Kanpur, India, December 2002. Springer.
BibTex | Web page | PS ]
[LN02]
R. Lazić 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.
BibTex | Web page | PS ]
[Bla02]
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.
BibTex | Web page | PS ]
[Fle02]
E. Fleury. Automates temporisés avec mises à jour. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2002.
BibTex | Web page | PS ]
[HS02a]
N. Halbwachs and Ph. Schnoebelen. Vérification de propriétés quantitatives. Final report, Action Spécifique 22 du Département STIC du CNRS, December 2002.
BibTex ]
[Pet02]
L. Petrucci. Modélisation, vérification et applications. Mémoire d'habilitation, Université d'Évry, France, December 2002.
BibTex | Web page | PS ]
[Gou02h]
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.
BibTex | Web page | PS ]
[Bou02a]
P. Bouyer. A Logical Characterization of Data Languages. Information Processing Letters, 84(2):75--85, October 2002.
BibTex | Web page | PS ]
[KBP+02]
L. M. Kristensen, J. Billington, L. Petrucci, Z. H. Qureshi, and R. Kiefer. Formal specification and analysis of airborne mission systems. In Proceedings of the 21st IEEE Digital Avionics Systems Conference (DASC'02), volume 1, pages 4.D.4.1--4.D.4.13, Irvine, California, USA, October 2002. IEEE Aerospace and Electronic Systems Society.
BibTex | Web page | PS ]
[PKB02]
L. Petrucci, L. M. Kristensen, and J. Billington. Modelling and Analysis of Airborne Mission Systems. Final report, phase 4, DSTO/UniSA contract, October 2002. 68 pages.
BibTex ]
[Cor02a]
V. Cortier. About the Decision of Reachability for Register Machines. Informatique Théorique et Applications, 36(4):341--358, October-December 2002.
BibTex | Web page | PS ]
[Bac02]
M. Baclet. Langages de données. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002.
BibTex | Web page | PS ]
[Ber02b]
V. Bernat. Transformation de l'authentification en secret. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002.
BibTex ]
[GLN02]
J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical Relations for Monadic Types. In Proceedings of the 16th International Workshop on Computer Science Logic (CSL'02), volume 2471 of Lecture Notes in Computer Science, pages 553--568, Edinburgh, Scotland, UK, September 2002. Springer.
BibTex | Web page | PS ]
[HS02b]
S. Hornus and Ph. Schnoebelen. On Solving Temporal Logic Queries. In Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology (AMAST'02), volume 2422 of Lecture Notes in Computer Science, pages 163--177, Saint Gilles les Bains, Reunion Island, France, September 2002. Springer.
BibTex | Web page | PS | PDF ]
[Gou02b]
J. Goubault-Larrecq. Higher-Order Positive Set Constraints. In Proceedings of the 16th International Workshop on Computer Science Logic (CSL'02), volume 2471 of Lecture Notes in Computer Science, pages 473--489, Edinburgh, Scotland, UK, September 2002. Springer.
BibTex | Web page | PS ]
[Gou02a]
J. Goubault-Larrecq, editor. Actes du 1er Workshop International sur la Sécurité des Communications sur Internet (SECI'02), Tunis, Tunisia, September 2002. INRIA.
BibTex | Web page ]
[Gou02i]
J. Goubault-Larrecq. Vérification de protocoles cryptographiques: la logique à la rescousse! In Actes du 1er Workshop International sur la Sécurité des Communications sur Internet (SECI'02), pages 119--152, Tunis, Tunisia, September 2002. INRIA. Invited paper.
BibTex | Web page | PS ]
[GV02]
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.
BibTex | Web page | PS ]
[FMP02]
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.
BibTex | Web page | PS ]
[Las02b]
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.
BibTex | Web page | PS ]
[Bau02]
M. Baudet. Contrôle de ressource et évitement des interblocages sur la mémoire. Rapport de DEA, DEA Programmation, Paris, France, September 2002.
BibTex | Web page | PS | PDF ]
[Ber02c]
N. Bertrand. Vérification de canaux à pertes stochastiques. Rapport de DEA, DEA Algorithmique, Paris, France, September 2002.
BibTex | Web page | PS ]
[ABK+02]
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):153--196, September 2002.
BibTex | Web page | PS ]
[Mes02]
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.
BibTex | Web page | PS ]
[Sch02b]
Ph. Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters, 83(5):251--261, September 2002.
doi: 10.1016/S0020-0190(01)00337-4.
BibTex | DOI | Web page | PS | PDF ]
[Zha02]
Y. Zhang. Logical Relations For Names. Rapport de DEA, DEA Programmation, Paris, France, September 2002.
BibTex | Web page | PS ]
[BST02b]
M. Bidoit, D. Sannella, and A. Tarlecki. Global Development via Local Observational Construction Steps. In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02), volume 2420 of Lecture Notes in Computer Science, pages 1--24, Warsaw, Poland, August 2002. Springer. Invited paper.
BibTex | Web page | PS ]
[DFP02]
M. Duflot, L. Fribourg, and C. Picaronny. Randomized Dining Philosophers without Fairness Assumption. In Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science (IFIP TCS'02), volume 223 of IFIP Conference Proceedings, pages 169--180, Montréal, Québec, Canada, August 2002. Kluwer Academic Publishers.
BibTex | Web page | PS ]
[FRSV02]
A. Finkel, J.-F. Raskin, M. Samuelides, and L. Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In Proceedings of the 4th International Workshop on Verification of Infinite State Systems (INFINITY'02), volume 68 of Electronic Notes in Theoretical Computer Science, pages 121--144, Brno, Czech Republic, August 2002. Elsevier Science Publishers.
BibTex | Web page | PS ]
[MS02]
B. Masson and Ph. Schnoebelen. On Verifying Fair Lossy Channel Systems. In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02), volume 2420 of Lecture Notes in Computer Science, pages 543--555, Warsaw, Poland, August 2002. Springer.
BibTex | Web page ]
[Mar02]
N. Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In Proceedings of the 9th International Workshop on Expressiveness in Concurrency (EXPRESS'02), volume 68 of Electronic Notes in Theoretical Computer Science, pages 87--104, Brno, Czech Republic, August 2002. Elsevier Science Publishers.
doi: 10.1016/S1571-0661(05)80366-4.
BibTex | DOI | Web page | PS | PDF ]
[PKG+02]
L. Petrucci, L. M. Kristensen, G. E. Gallasch, M. Elliot, P. Dauchy, J. Billington, and M. Aziz. Modelling and Analysis of Airborne Mission Systems. Contract Report Final report for phase 3, DSTO/UniSA contract, August 2002. 79 pages.
BibTex ]
[AL02]
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:7--51, August 2002.
doi: 10.1016/S1567-8326(02)00022-X.
BibTex | DOI | Web page | PS ]
[BBP02]
B. Bérard, P. Bouyer, and A. Petit. Analysing the PGM Protocol with UPPAAL. In Proceedings of the 2nd Workshop on Real-Time Tools (RT-TOOLS'02), Copenhagen, Denmark, August 2002. Uppsala University.
BibTex | Web page | PS ]
[Las02a]
S. Lasota. Decidability of Strong Bisimilarity for Timed BPP. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02), volume 2421 of Lecture Notes in Computer Science, pages 562--578, Brno, Czech Republic, August 2002. Springer.
BibTex | Web page | PS ]
[BST02a]
M. Bidoit, D. Sannella, and A. Tarlecki. Architectural Specifications in CASL. Formal Aspects of Computing, 13(3-5):252--273, July 2002.
doi: 10.1007/s001650200012.
BibTex | DOI | Web page | PS ]
[LMS02b]
F. Laroussinie, N. Markey, and Ph. Schnoebelen. Temporal Logic with Forgettable Past. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pages 383--392, Copenhagen, Denmark, July 2002. IEEE Computer Society Press.
doi: 10.1109/LICS.2002.1029846.
BibTex | DOI | Web page | PS | PDF ]
[Gou02f]
J. Goubault-Larrecq. SKInT Labels. Research Report LSV-02-7, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 15 pages.
BibTex | Web page | PS ]
[Gou02c]
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.
BibTex | Web page | PS ]
[LS02a]
A. Labroue and Ph. Schnoebelen. An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems. Nordic Journal of Computing, 9(2):118--144, July 2002.
BibTex | Web page | PS ]
[GPD+02]
J. Goubault-Larrecq, J.-Ph. Pouzol, S. Demri, L. Mé, and P. Carle. Langages de détection d'attaques par signatures. Contract Report (Sous-projet 3, livrable 1), Projet RNTL DICO, June 2002. 30 pages.
BibTex ]
[PKBQ02]
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, volume 12 of Conferences in Research and Practice in Information Technology, pages 95--104, Adelaide, Australia, June 2002. Australian Computer Society.
BibTex | Web page | PS ]
[Mag02]
F. Magniette. Preuves d'algorithmes auto-stabilisants. Thèse de doctorat, Université Paris-Sud 11, Orsay, France, June 2002.
BibTex | Web page | PS ]
[Sch02a]
Ph. Schnoebelen. Temporal Logic and Verification. Invited tutorial, 5th Summer School on Modelling and Verifying Parallel Processes (MOVEP'02), Nantes, France, June 2002.
BibTex ]
[Gou02d]
J. Goubault-Larrecq. Outils CPV et CPV2. Contract Report 8, Projet RNTL EVA, May 2002. 7 pages.
BibTex | Web page | PDF ]
[Cor02c]
V. Cortier. Outil de vérification SECURIFY. Contract Report 7, projet RNTL EVA, May 2002. 6 pages.
BibTex | Web page | PDF ]
[DS02b]
S. Demri and Ph. Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation, 174(1):84--103, April 2002.
doi: 10.1006/inco.2001.3094.
BibTex | DOI | Web page | PS | PDF ]
[HCF+02]
F. Herbreteau, F. Cassez, A. Finkel, O. F. Roux, and G. Sutre. Verification of Embedded Reactive Fiffo Systems. In Proceedings of the 5th Latin American Symposium on Theoretical Informatics (LATIN'02), volume 2286 of Lecture Notes in Computer Science, pages 400--414, Cancun, Mexico, April 2002. Springer.
BibTex | Web page | PS ]
[LMS02a]
F. Laroussinie, N. Markey, and Ph. Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'02), volume 2303 of Lecture Notes in Computer Science, pages 264--279, Grenoble, France, April 2002. Springer.
BibTex | Web page | PS | PDF ]
[Boi02]
A. Boisseau. Signatures électroniques de contrats. Research Report LSV-02-4, Laboratoire Spécification et Vérification, ENS Cachan, France, April 2002. 22 pages.
BibTex | Web page | PS ]
[Bou02b]
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.
BibTex | Web page | PS | PDF ]
[Bér02a]
B. Bérard. Vérification de modèles temporisés. Mémoire d'habilitation, Université Paris 7, Paris, France, April 2002.
BibTex | Web page | PS ]
[BH02]
M. Bidoit and R. Hennicker. On the Integration of Observability and Reachability Concepts. In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'02), volume 2303 of Lecture Notes in Computer Science, pages 21--36, Grenoble, France, April 2002. Springer.
BibTex | Web page | PS ]
[DLS02]
S. Demri, F. Laroussinie, and Ph. Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract). In Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS'02), volume 2285 of Lecture Notes in Computer Science, pages 620--631, Antibes Juan-les-Pins, France, March 2002. Springer.
BibTex | Web page | PS | PDF ]
[Cor02b]
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.
BibTex | Web page | PS ]
[LS02c]
D. Lugiez and Ph. Schnoebelen. The Regular Viewpoint on PA-Processes. Theoretical Computer Science, 274(1-2):89--115, March 2002.
doi: 10.1016/S0304-3975(00)00306-6.
BibTex | DOI | Web page | PS | PDF ]
[LS02b]
A. Labroue and Ph. Schnoebelen. An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems. In Proceedings of the 8th International Workshop on Expressiveness in Concurrency (EXPRESS'01), volume 52 of Electronic Notes in Theoretical Computer Science, pages 1--20, Aalborg, Denmark, February 2002. Elsevier Science Publishers.
doi: 10.1016/S1571-0661(04)00213-0.
BibTex | DOI | Web page | PS | PDF ]
[BP02]
P. Bouyer and A. Petit. A KleeneashBüchi-like Theorem for Clock Languages. Journal of Automata, Languages and Combinatorics, 7(2):167--186, 2002.
BibTex | Web page | PS ]
[DO02]
S. Demri and E. Orlowska. Incomplete Information: Structure, Inference, Complexity. EATCS Monographs. Springer, 2002.
BibTex | Web page ]
[DS02a]
S. Demri and U. Sattler. Automata-Theoretic Decision Procedures for Information Logics. Fundamenta Informaticae, 53(1):1--22, 2002.
BibTex | Web page | PS | PDF ]
[HHB02]
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, volume 2263 of Lecture Notes in Computer Science, pages 69--84. Springer, 2002.
BibTex | Web page | PS ]
[Gou02g]
J. Goubault-Larrecq. Special Issue on Models and Methods for Cryptographic Protocol Verification. Journal of Telecommunications and Information Technology, 4/2002, 2002.
BibTex | Web page ]
[Gou02e]
J. Goubault-Larrecq. Sécurité, modélisation et analyse de protocoles cryptographiques. Phœbus, la revue de la sûreté de fonctionnement, 20, 2002.
BibTex | Web page ]
[Lab02]
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.
BibTex | Web page | PS ]
[CS02]
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:5--15, 2002.
BibTex | Web page | PDF ]
[Cor02d]
V. Cortier. Securify version 1. Available at http://www.lsv.ens-cachan.fr/~cortier/EVA/securify.tar.gz, 2002. Started 2001. See [Cor02c] for description. Written in Caml (about 3200 lines).
BibTex ]

This file was generated by bibtex2html 1.98.

About LSV