Publications : 2003
-
[Cor03a]
-
V. Cortier.
A Guide for SECURIFY.
Technical Report 13, projet RNTL EVA, December 2003.
9 pages.
[ BibTex |
Web page |
PDF ]
-
[Ler03]
-
J. Leroux.
Algorithmique de la vérification des systèmes à
compteurs. Approximation et accélération. Implémentation de
l'outil FAST.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, December 2003.
[ BibTex |
Web page |
PS ]
-
[BL03]
-
B. Bérard and F. Laroussinie.
Vérification compositionnelle des p-automates.
Contract Report (Lot 4.1 fourniture 1), Projet RNTL Averroes,
November 2003.
16 pages.
[ BibTex ]
-
[BFN03b]
-
S. Bardin, A. Finkel, and D. Nowak.
Rapport final.
Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et
le LSV, November 2003.
50 pages.
[ BibTex ]
-
[CJ03]
-
H. Comon and F. Jacquemard.
Ground Reducibility is EXPTIME-complete.
Information and Computation, 187(1):123--153, November 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[GB03a]
-
A. Galland and M. Baudet.
Controlling and Optimizing the Usage of One Resource.
In Proceedings of the 1st Asian Symposium on Programming
Languages and Systems (APLAS'03), volume 2895 of Lecture Notes in
Computer Science, pages 195--211, Beijing, China, November 2003. Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[KNT03]
-
M. Kerbœuf, D. Nowak, and J.-P. Talpin.
Formal Proof of a Polychronous Protocol for Loosely
Time-Triggered Architectures.
In Proceedings of the 5th International Conference on Formal
Engineering Methods (ICFEM'03), volume 2885 of Lecture Notes in
Computer Science, pages 359--374, Singapore, November 2003. Springer.
[ BibTex |
Web page |
PS ]
-
[Del03c]
-
S. Delaune.
Vérification de protocoles de sécurité dans un
modèle de l'intrus étendu.
Research Report LSV-03-15, Laboratoire Spécification et
Vérification, ENS Cachan, France, November 2003.
[ BibTex |
Web page |
PS ]
-
[BBP03]
-
B. Bérard, P. Bouyer, and A. Petit.
Une analyse du protocole PGM avec UPPAAL.
In Actes du 4ème Colloque sur la Modélisation des
Systèmes Réactifs (MSR'03), pages 415--430, Metz, France,
October 2003. Hermès.
[ BibTex |
Web page |
PS ]
-
[BP03]
-
M. Baclet and R. Pacalet.
Vérifications du protocole VCI.
In Actes du 4ème Colloque sur la Modélisation des
Systèmes Réactifs (MSR'03), pages 431--445, Metz, France,
October 2003. Hermès.
[ BibTex |
Web page |
PS ]
-
[GB03b]
-
A. Galland and M. Baudet.
Économiser l'or du banquier.
In Actes de la 3ème Conférence Française sur les
Systèmes d'Exploitation (CFSE'03), pages 638--649, La Colle sur
Loup, France, October 2003. INRIA.
[ BibTex |
Web page |
PS |
PDF ]
-
[DDG+03]
-
S. Demri, M. Ducassé, J. Goubault-Larrecq, L. Mé,
J. Olivain, C. Picaronny, J.-Ph. Pouzol, É. Totel, and
B. Vivinis.
Algorithmes de détection et langages de signatures.
Contract Report (Sous-projet 3, livrable 3), projet RNTL DICO,
October 2003.
72 pages.
[ BibTex ]
-
[Rog03b]
-
M. Roger.
Raffinements de la résolution et vérification de
protocoles cryptographiques.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, October 2003.
[ BibTex |
Web page |
PS ]
-
[MS03b]
-
N. Markey and Ph. Schnoebelen.
TSMV v1.0.
Available at http://www.lsv.ens-cachan.fr/~markey/TSMV/,
October 2003.
See description in [?]. Written in C (about
4000 lines on top of NuSMV v2.1.2).
[ BibTex |
Web page ]
-
[Ber03]
-
V. Bernat.
Towards a Logic for Verification of Security Protocols.
In Proceedings of the Workshop on Security Protocols
Verification (SPV'03), pages 31--35, Marseilles, France, September 2003.
[ BibTex |
Web page |
PS ]
-
[Del03a]
-
S. Delaune.
Intruder Deduction Problem in Presence of Guessing Attacks.
In Proceedings of the Workshop on Security Protocols
Verification (SPV'03), pages 26--30, Marseilles, France, September 2003.
[ BibTex |
Web page |
PDF ]
-
[Del03b]
-
S. Delaune.
Vérification de protocoles de sécurité dans un
modèle de l'intrus étendu.
Rapport de DEA, DEA Programmation, Paris, France, September 2003.
[ BibTex |
Web page |
PS ]
-
[Dem03a]
-
S. Demri.
(Modal) Logics for Semistructured Data (Bis).
Invited talk, 3rd Workshop on Methods for Modalities
(M4M'03), Nancy, France, September 2003.
[ BibTex ]
-
[DdN03]
-
S. Demri and H. de Nivelle.
Relational Translations into GF2.
In Proceedings of the 3rd Workshop on Methods for Modalities
(M4M-3), pages 93--108, Nancy, France, September 2003.
[ BibTex ]
-
[Jac03c]
-
F. Jacquemard.
Reachability and Confluence are Indecidable for Flat Term
Rewriting Systems.
Information Processing Letters, 87(5):265--270, September 2003.
[ BibTex |
Web page |
PS ]
-
[Bac03]
-
M. Baclet.
Logical Characterization of Aperiodic Data Languages.
Research Report LSV-03-12, Laboratoire Spécification et
Vérification, ENS Cachan, France, September 2003.
16 pages.
[ BibTex |
Web page |
PS ]
-
[Boi03]
-
A. Boisseau.
Abstractions pour la vérification de propriétés de
sécurité de protocoles cryptographiques.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, September 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[Duf03]
-
M. Duflot.
Algorithmes distribués sur des anneaux
paramétrés --- Preuves de convergence probabiliste et
déterministe.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, September 2003.
[ BibTex |
Web page |
PS ]
-
[Ver03a]
-
K. N. Verma.
Automates d'arbres bidirectionnels modulo théories
équationnelles.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, September 2003.
[ BibTex |
Web page |
PS ]
-
[CSS03]
-
J.-M. Couvreur, N. Saheb, and G. Sutre.
An Optimal Automata Approach to LTL Model Checking of
Probabilistic Systems.
In Proceedings of the 10th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning (LPAR'03),
volume 2850 of Lecture Notes in Artificial Intelligence, pages 361--375,
Almaty, Kazakhstan, September 2003. Springer.
[ BibTex |
Web page |
PS ]
-
[Lar03]
-
F. Laroussinie.
Automates temporisés et hybrides, modélisation et
vérification.
Invited lecture, école d'été ETR 2003 (École Temps Réel),
Toulouse, France, September 2003.
[ BibTex ]
-
[Ben03]
-
M. Ben Gaid.
Modélisation et vérification des aspects temporisés
des langages pour automates programmables industriels.
Rapport de DEA, DEA Informatique Distribuée, Orsay, France,
September 2003.
68 pages.
[ BibTex |
Web page |
PDF ]
-
[Ver03b]
-
K. N. Verma.
On Closure under Complementation of Equational Tree Automata for
Theories Extending AC.
In Proceedings of the 10th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning (LPAR'03),
volume 2850 of Lecture Notes in Artificial Intelligence, pages 183--195,
Almaty, Kazakhstan, September 2003. Springer.
[ BibTex |
Web page |
PS ]
-
[BFN03a]
-
S. Bardin, A. Finkel, and D. Nowak.
Note de synthèse à 10 mois.
Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et
le LSV, August 2003.
21 pages.
[ BibTex ]
-
[BFL+03b]
-
S. Bardin, A. Finkel, J. Leroux, L. Petrucci, and
L. Worobel.
FAST User's Manual, August 2003.
33 pages.
[ BibTex |
Web page |
PS ]
-
[Wor03]
-
L. Worobel.
INTERFAST v1.0: A GUI for FAST, August 2003.
See [BFL+03b] for description. Written in Java (6300 lines)
and C (1600 lines), using Java Cup.
[ BibTex |
Web page ]
-
[MS03a]
-
N. Markey and Ph. Schnoebelen.
Model Checking a Path (Preliminary Report).
In Proceedings of the 14th International Conference on
Concurrency Theory (CONCUR'03), volume 2761 of Lecture Notes in
Computer Science, pages 251--265, Marseilles, France, August 2003. Springer.
doi:
10.1007/b11938.
[ BibTex |
DOI |
Web page |
PS |
PDF ]
-
[ZN03]
-
Y. Zhang and D. Nowak.
Logical Relations for Dynamic Name Creation.
In Proceedings of the 17th International Workshop on Computer
Science Logic (CSL'03), volume 2803 of Lecture Notes in Computer
Science, pages 575--588, Vienna, Austria, August 2003. Springer.
[ BibTex |
Web page |
PS ]
-
[BDMP03]
-
P. Bouyer, D. D'Souza, P. Madhusudan, and A. Petit.
Timed Control with Partial Observability.
In Proceedings of the 15th International Conference on
Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in
Computer Science, pages 180--192, Boulder, Colorado, USA, July 2003.
Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[BFNS03]
-
S. Bardin, A. Finkel, D. Nowak, and
Ph. Schnoebelen.
Note de synthèse à 6 mois.
Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et
le LSV, July 2003.
43 pages.
[ BibTex ]
-
[Jac03a]
-
F. Jacquemard.
The EVA Translator, version 2.
Technical Report 9, projet RNTL EVA, July 2003.
38 pages.
[ BibTex |
Web page |
PDF ]
-
[Jac03b]
-
F. Jacquemard.
The EVA translator, version 2, July 2003.
See [Jac03a] for description. Written in OCaml (about 11000
lines).
[ BibTex ]
-
[BFLP03]
-
S. Bardin, A. Finkel, J. Leroux, and L. Petrucci.
FAST: Fast Acceleration of Symbolic Transition
Systems.
In Proceedings of the 15th International Conference on
Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in
Computer Science, pages 118--121, Boulder, Colorado, USA, July 2003.
Springer.
[ BibTex |
Web page |
PS ]
-
[BFL03a]
-
S. Bardin, A. Finkel, and J. Leroux.
FAST v1.0: Fast Acceleration of Symbolic Transition
Systems, July 2003.
See [BFLP03] for description. Written in C++ (about 4400
lines on top of the MONA v1.4 library).
[ BibTex |
Web page ]
-
[FMP03b]
-
L. Fribourg, S. Messika, and C. Picaronny.
Traces of Randomized Distributed Algorithms As Markov Fields.
Application to Rapid Mixing.
Research Report LSV-03-10, Laboratoire Spécification et
Vérification, ENS Cachan, France, July 2003.
19 pages.
[ BibTex |
Web page |
PS ]
-
[Jac03d]
-
F. Jacquemard.
SPORE: Security Protocols Open REpository, July 2003.
Works with Perl scripts (about 1200 lines) and contains about 50
protocol descriptions (as of Aug. 2004).
[ BibTex |
Web page ]
-
[CC03a]
-
H. Comon-Lundh and V. Cortier.
New Decidability Results for Fragments of First-Order Logic and
Application to Cryptographic Protocols.
In Proceedings of the 14th International Conference on
Rewriting Techniques and Applications (RTA'03), volume 2706 of
Lecture Notes in Computer Science, pages 148--164, Valencia, Spain, June
2003. Springer.
[ BibTex |
Web page |
PS ]
-
[PKBQ03]
-
L. Petrucci, L. M. Kristensen, J. Billington, and Z. H.
Qureshi.
Developing a Formal Specification for the Mission System of a
Maritime Surveillance Aircraft.
In Proceedings of the 3rd International Conference on
Application of Concurrency to System Design (ACSD'03), pages
92--101, Guimarães, Portugal, June 2003. IEEE Computer Society Press.
[ BibTex |
Web page |
PS ]
-
[LN03]
-
R. Lazić and D. Nowak.
On a Semantic Definition of Data Independence.
In Proceedings of the 6th International Conference on Typed
Lambda Calculi and Applications (TLCA'03), volume 2701 of Lecture
Notes in Computer Science, pages 226--240, Valencia, Spain, June 2003.
Springer.
[ BibTex |
Web page |
PS ]
-
[Sch03c]
-
Ph. Schnoebelen.
Oracle circuits for branching-time model checking.
In Proceedings of the 30th International Colloquium on
Automata, Languages and Programming (ICALP'03), volume 2719 of
Lecture Notes in Computer Science, pages 790--801, Eindhoven, The
Netherlands, June 2003. Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[CS03b]
-
H. Comon-Lundh and V. Shmatikov.
Intruder Deductions, Constraint Solving and Insecurity Decision
in Presence of Exclusive Or.
In Proceedings of the 18th Annual IEEE Symposium on Logic
in Computer Science (LICS'03), pages 271--280, Ottawa, Canada, June
2003. IEEE Computer Society Press.
[ BibTex ]
-
[BCvH+03]
-
J. Billington, S. Christensen, K. M. van Hee, E. Kindler,
O. Kummer, L. Petrucci, R. Post, Ch. Stehno, and M. Weber.
The Petri Net Markup Language: Concepts, Technology
and Tools.
In Proceedings of the 24th International Conference on
Applications and Theory of Petri Nets (ICATPN'03), volume 2679 of
Lecture Notes in Computer Science, pages 483--505, Eindhoven, The
Netherlands, June 2003. Springer.
Invited paper.
[ BibTex |
Web page |
PS ]
-
[Ver03c]
-
K. N. Verma.
Two-Way Equational Tree Automata for AC-like Theories:
Decidability and Closure Properties.
In Proceedings of the 14th International Conference on
Rewriting Techniques and Applications (RTA'03), volume 2706 of
Lecture Notes in Computer Science, pages 180--196, Valencia, Spain, June
2003. Springer.
[ BibTex |
Web page |
PS ]
-
[ABBL03]
-
L. Aceto, P. Bouyer, A. Burgueño, and K. G. Larsen.
The Power of Reachability Testing for Timed Automata.
Theoretical Computer Science, 300(1-3):411--475, May 2003.
doi:
10.1016/S0304-3975(02)00334-1.
[ BibTex |
DOI |
Web page |
PS ]
-
[BPT03]
-
P. Bouyer, A. Petit, and D. Thérien.
An Algebraic Approach to Data Languages and Timed Languages.
Information and Computation, 182(2):137--162, May 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[Dem03b]
-
S. Demri.
A Polynomial-Space Construction of Tree-Like Models for Logics
with Local Chains of Modal Connectives.
Theoretical Computer Science, 300(1-3):235--258, May 2003.
doi:
10.1016/S0304-3975(02)00082-8.
[ BibTex |
DOI |
Web page |
PS |
PDF ]
-
[J+03]
-
B. Jonsson et al.
Roadmap on Component-based Design and Integration Platforms.
Contract Report (Deliverable W1.A2.N1.Y1), European Project
IST-2001-34820 "ARTIST" Advanced Real-Time Systems, May 2003.
78 pages.
[ BibTex ]
-
[Sch03b]
-
Ph. Schnoebelen.
Model Checking Branching-Time Temporal Logics.
Invited talk, Franco-Israeli Workshop on Semantics and Verification
of Hardware and Software Systems, Tel-Aviv, Israel, May 2003.
[ BibTex ]
-
[BBFL03]
-
G. Behrmann, P. Bouyer, E. Fleury, and K. G. Larsen.
Static Guard Analysis in Timed Automata Verification.
In Proceedings of the 9th International Conference on Tools
and Algorithms for Construction and Analysis of Systems (TACAS'03),
volume 2619 of Lecture Notes in Computer Science, pages 254--277, Warsaw,
Poland, April 2003. Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[BS03]
-
N. Bertrand and Ph. Schnoebelen.
Model Checking Lossy Channels Systems Is Probably Decidable.
In Proceedings of the 6th International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS'03), volume 2620 of Lecture Notes in Computer Science, pages
120--135, Warsaw, Poland, April 2003. Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[CC03b]
-
H. Comon-Lundh and V. Cortier.
Security properties: two agents are sufficient.
In Proceedings of the 12th European Symposium on Programming
(ESOP'03), volume 2618 of Lecture Notes in Computer Science, pages 99--113,
Warsaw, Poland, April 2003. Springer.
[ BibTex |
Web page |
PS ]
-
[FMP03a]
-
L. Fribourg, S. Messika, and C. Picaronny.
On the Absence of Phase Transition in Randomized Distributed
Algorithms.
Research Report LSV-03-7, Laboratoire Spécification et
Vérification, ENS Cachan, France, April 2003.
17 pages.
[ BibTex |
Web page |
PS ]
-
[Mar03a]
-
N. Markey.
Logiques temporelles pour la vérification: expressivité,
complexité, algorithmes.
Thèse de doctorat, Laboratoire d'Informatique Fondamentale
d'Orléans, France, April 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[BHK03]
-
M. Bidoit, R. Hennicker, and A. Kurz.
Observational Logic, Constructor-Based Logic, and their
Duality.
Theoretical Computer Science, 298(3):471--510, April 2003.
[ BibTex |
Web page |
PS ]
-
[Cor03b]
-
V. Cortier.
Vérification automatique des protocoles cryptographiques.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, March 2003.
[ BibTex |
Web page |
PS ]
-
[LST03]
-
F. Laroussinie, Ph. Schnoebelen, and M. Turuani.
On the Expressivity and Complexity of Quantitative
Branching-Time Temporal Logics.
Theoretical Computer Science, 297(1-3):297--315, March 2003.
doi:
10.1016/S0304-3975(02)00644-8.
[ BibTex |
DOI |
Web page |
PS ]
-
[Bou03]
-
P. Bouyer.
Untameable Timed Automata!
In Proceedings of the 20th Annual Symposium on Theoretical
Aspects of Computer Science (STACS'03), volume 2607 of Lecture Notes
in Computer Science, pages 620--631, Berlin, Germany, February 2003.
Springer.
[ BibTex |
Web page |
PS |
PDF ]
-
[CT03]
-
H. Comon-Lundh and R. Treinen.
Easy Intruder Deductions.
In Verification: Theory and Practice, Essays Dedicated to
Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of
Lecture Notes in Computer Science, pages 225--242. Springer, February 2003.
Invited paper.
[ BibTex |
Web page |
PS ]
-
[FPS03]
-
A. Finkel, S. Purushothaman Iyer, and G. Sutre.
Well-Abstracted Transition Systems: Application to FIFO
Automata.
Information and Computation, 181(1):1--31, February 2003.
[ BibTex |
Web page |
PS ]
-
[Mar03b]
-
N. Markey.
Temporal Logic with Past is Exponentially More Succinct.
EATCS Bulletin, 79:122--128, February 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[Gou03]
-
J. Goubault-Larrecq, editor.
Proceedings of the 1st Workshop on Logical Aspects of
Cryptographic Protocol Verification (LACPV 2001), volume 55 of
Electronic Notes in Theoretical Computer Science, Paris, France, January
2003. Elsevier Science Publishers.
doi:
10.1016/S1571-0661(05)80576-6.
[ BibTex |
DOI ]
-
[ADdR03]
-
N. Alechina, S. Demri, and M. de Rijke.
A Modal Perspective on Path Constraints.
Journal of Logic and Computation, 13(6):939--956, 2003.
[ BibTex |
Web page |
PS |
PDF ]
-
[BFKM03]
-
B. Bérard, L. Fribourg, F. Klay, and J.-F. Monin.
A Compared Study of Two Correctness Proofs for the Standardized
Algorithm of ABR Conformance.
Formal Methods in System Design, 22(1):59--86, January 2003.
doi:
10.1023/A:1021704214464.
[ BibTex |
DOI |
Web page |
PS ]
-
[CNNR03]
-
H. Comon, P. Narendran, R. Nieuwenhuis, and M. Rusinowitch.
Deciding the Confluence of Ordered Term Rewrite Systems.
ACM Transactions on Computational Logic, 4(1):33--55, January 2003.
[ BibTex ]
-
[GG03]
-
J. Goubault-Larrecq and É. Goubault.
On the Geometry of Intuitionistic S4 Proofs.
Homology, Homotopy and Applications, 5(2):137--209, 2003.
[ BibTex |
Web page |
PS ]
-
[DW03]
-
Ph. David and H. Waeselynck, editors.
Logiciel libre et sûreté de fonctionnement: cas des
systèmes critiques.
Hermès, 2003.
[ BibTex |
Web page ]
-
[CS03a]
-
H. Comon-Lundh and V. Shmatikov.
Constraint Solving, Exclusive Or and the Decision of
Confidentiality for Security Protocols Assuming a Bounded Number of
Sessions.
Research Report LSV-03-1, Laboratoire Spécification et
Vérification, ENS Cachan, France, January 2003.
17 pages.
[ BibTex |
Web page |
PS ]
-
[Rog03a]
-
M. Roger.
MOP: MOdular Prover, 2003.
See description in [?]. Written in OCaml
(9611 lines).
[ BibTex ]
-
[CP03]
-
J.-M. Couvreur and D. Poitrenaud.
Dépliage pour la vérification de propriétés
temporelles.
In Vérification et mise en œuvre des réseaux de
Petri --- Tome 2, chapter 3, pages 127--161. Hermès, January 2003.
[ BibTex ]
-
[Sch03a]
-
Ph. Schnoebelen.
The Complexity of Temporal Logic Model Checking.
In Selected Papers from the 4th Workshop on Advances in
Modal Logics (AiML'02), pages 393--436, Toulouse, France, 2003. King's
College Publication.
Invited paper.
[ BibTex |
Web page |
PS |
PDF ]
-
[CD03]
-
V. Cortier and S. Delaune.
Securify version 2, 2003.
See [Cor03a] for description. Written in Caml (about 3300
lines).
[ BibTex |
Web page ]
-
[Pet03]
-
L. Petrucci.
symprod: construction et analyse du produit
synchronisé modulaire d'automates, 2003.
[ BibTex ]
This file was generated by
bibtex2html 1.98.