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.