@proceedings{JGL:LACPV,
title = {{P}roceedings of the 1st {W}orkshop on {L}ogical {A}spects of
{C}ryptographic {P}rotocol {V}erification
({LACPV} 2001)},
booktitle = {{P}roceedings of the 1st {W}orkshop on {L}ogical
{A}spects of
{C}ryptographic {P}rotocol {V}erification
({LACPV} 2001)},
editor = {Goubault{-}Larrecq, Jean},
publisher = {Elsevier Science Publishers},
volume = {55},
number = 1,
series = {Electronic Notes in Theoretical Computer Science},
year = 2003,
month = jan,
address = {Paris, France},
oldurl = {http://www.sciencedirect.com/science?_ob=IssueURL&
_tockey=%23TOC%2313109%232003%23999449998%23521171%23FLP%23
Volume_55,_Issue_1,_Pages_1-26_(January_2003)&
_auth=y&view=c&_acct=C000051058&_version=1&_urlVersion=0&
_userid=1052425&md5=01843f1018b98d2dd1c00502871bfff4},
doi = {10.1016/S1571-0661(05)80576-6}
}
@article{ABBL02,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Aceto, Luca and Bouyer, Patricia and
Burgue{\~n}o, Augusto and Larsen, Kim G.},
title = {The Power of Reachability Testing for Timed Automata},
volume = {300},
number = {1-3},
pages = {411-475},
year = {2003},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-ABBL02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-ABBL02.ps},
doi = {10.1016/S0304-3975(02)00334-1},
abstract = {The computational engine of the verification tool Uppaal
consists of a collection of efficient reachability properties of systems.
Model-checking of properties other than plain reachability ones may
currently be carried out in such a tool as follows. Given a property
\(\phi\) to model-check, the user must provide a test
automaton~\(T_{\phi}\) for it. This test automaton must be such that the
original system \(S\) has the property expressed by \(\phi\) precisely
when none of the distinguished reject states of~\(T_{\phi}\) can be
reached in the synchronized parallel composition of \(S\) with
\(T_{\phi}\). This raises the question of which properties may be analyzed
by {\scshape Uppaal} in such a way. This paper gives an answer to this
question by providing a complete characterization of the class of
properties for which model-checking can be reduced to reachability testing
in the sense outlined above. This result is obtained as a corollary of a
stronger statement pertaining to the compositionality of the property
language considered in this study. In particular, it is shown that our
language is the least expressive compositional language that can express a
simple safety property stating that no reject state can ever be
reached.\par
Finally, the property language characterizing the power of reachability
testing is used to provide a definition of characteristic properties with
respect to a timed version of the ready simulation preorder, for nodes of
\(\tau\)-free, deterministic timed automata.}
}
@article{Alechina::Demri::DeRijke02,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Alechina, Natasha and Demri, St{\'e}phane and
de Rijke, Maarten},
title = {A Modal Perspective on Path Constraints},
volume = {13},
number = {6},
pages = {939-956},
year = {2003},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/final-jlc-adr.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/final-jlc-adr.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/final-jlc-adr.pdf}
}
@techreport{Averroes-4.1.1,
author = {B{\'e}rard, B{\'e}atrice and
Laroussinie, Fran{\c{c}}ois},
title = {V{\'e}rification compositionnelle des p-automates},
year = {2003},
month = nov,
type = {Contract Report},
number = {(Lot~4.1 fourniture~1)},
institution = {Projet RNTL Averroes},
oldhowpublished = {Lot 4.1 fourniture 1, du projet RNTL Averroes},
note = {16~pages}
}
@inproceedings{BBFL-tacas-2003,
address = {Warsaw, Poland},
month = apr,
year = 2003,
volume = 2619,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garavel, Hubert and Hatcliff, John},
acronym = {{TACAS}'03},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'03)},
author = {Behrmann, Gerd and Bouyer, Patricia and
Fleury, Emmanuel and Larsen, Kim G.},
title = {Static Guard Analysis in Timed Automata Verification},
pages = {254-277},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBFL-tacas-2003.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBFL-tacas-2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFL-tacas-2003.ps},
abstract = {By definition Timed Automata have
an infinite state-space, thus for verification
purposes, an exact finite abstraction is
required. We propose a location-based finite
zone abstraction, which computes an abstraction
based on the relevant guards for a particular
state of the model (as opposed to all guards).
We show that the location-based zone abstraction
is sound and complete with respect to location
reachability; that it generalises active-clock
reduction, in the sense that an inactive clock
has no relevant guards at all; that it enlarges
the class of timed automata, that can be
verified. We generalise the new abstraction to
the case of networks of timed automata, and
experimentally demonstrate a potentially
exponential speedup compared to the usual
abstraction.}
}
@inproceedings{BBP-msr2003,
address = {Metz, France},
month = oct,
year = 2003,
publisher = {Herm{\`e}s},
editor = {M{\'e}ry, Dominique and Rezg, Nidhal and
Xie, Xiaolan},
acronym = {{MSR}'03},
booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'03)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Petit, Antoine},
title = {Une analyse du protocole {PGM} avec {UPPAAL}},
pages = {415-430},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol,
designed to minimize both the probability of
negative acknowledgements
(NAK) implosion and the loading of the network
due to retransmissions
of lost packets. This protocol was presented to
the Internet
Engineering Task Force as an open reference
specification. In this
paper, we focus on the main reliability property
which PGM intends to
guarantee: a receiver either receives all data
packets from
transmissions and repairs or is able to detect
unrecoverable data
packet loss. To this purpose, we propose a
modelization of (a
simplified version of) PGM via a network of
timed automata. Using
Uppaal model-checker, we then study the validity
of the reliability
property above, which turns out to not be always
verified but to
depend of the values of several parameters that
we underscore.}
}
@inproceedings{BDMP-cav-2003,
address = {Boulder, Colorado, USA},
month = jul,
year = 2003,
volume = 2725,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
acronym = {{CAV}'03},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'03)},
author = {Bouyer, Patricia and D'Souza, Deepak and
Madhusudan, P. and
Petit, Antoine},
title = {Timed Control with Partial Observability},
pages = {180-192},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDMP-CAV03.ps},
abstract = {We consider the problem of
synthesizing controllers for timed systems
modeled using timed automata. The point of
departure from earlier work is that we
consider controllers that have only a
partial observation of the system that it
controls. In discrete event systems (where
continuous time is not modeled), it is well
known how to handle partial observability,
and decidability issues do not differ from
the complete information setting. We show
however that timed control under partial
observability is undecidable even for
internal specifications (while the analogous
problem under complete observability is
decidable) and we identify a decidable
subclass.}
}
@article{BFKM-FMSD,
publisher = {Kluwer Academic Publishers},
journal = {Formal Methods in System Design},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent and
Klay, Francis and
Monin, Jean-Fran{\c{c}}ois},
title = {A Compared Study of Two Correctness Proofs for the
Standardized Algorithm of {ABR} Conformance},
volume = {22},
number = {1},
pages = {59-86},
year = {2003},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFKM-FMSD.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFKM-FMSD.ps},
doi = {10.1023/A:1021704214464}
}
@techreport{BFN-edf10,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Note de synth{\`e}se {\`a}~10~mois},
year = {2003},
month = aug,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le LSV},
note = {21~pages}
}
@techreport{BFN-edf12,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Rapport final},
year = {2003},
month = nov,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le~LSV},
note = {50~pages}
}
@techreport{BFNS-edf6,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David and
Schnoebelen, {\relax Ph}ilippe},
title = {Note de synth{\`e}se {\`a} 6 mois},
year = {2003},
month = jul,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le LSV},
note = {43~pages}
}
@inproceedings{BP-msr03,
address = {Metz, France},
month = oct,
year = 2003,
publisher = {Herm{\`e}s},
editor = {M{\'e}ry, Dominique and Rezg, Nidhal and
Xie, Xiaolan},
acronym = {{MSR}'03},
booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'03)},
author = {Baclet, Manuel and Pacalet, Renaud},
title = {V{\'e}rifications du protocole~{VCI}},
pages = {431-445},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/vci-msr03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/vci-msr03.ps}
}
@article{BPT03,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Petit, Antoine and
Th{\'e}rien, Denis},
title = {An Algebraic Approach to Data Languages and Timed
Languages},
volume = {182},
number = {2},
pages = {137-162},
year = {2003},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-IetC.ps},
abstract = {Algebra offers an elegant and
powerful approach to understand regular
languages and finite automata. Such framework
has been notoriously
lacking for timed languages and timed automata.
We introduce the
notion of monoid recognizability for data
languages, which includes
timed languages as special case, in away that
respects the spirit of
the classical situation. We study closure
properties and hierarchies
in this model, and prove that emptiness is
decidable under natural
hypotheses. Our class of recognizable
languages properly includes
many families of deterministic timed languages
that have been
proposed until now, and the same holds for
non-deterministic
versions.}
}
@inproceedings{BerSch-fossacs2003,
address = {Warsaw, Poland},
month = apr,
year = 2003,
volume = 2620,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gordon, Andrew D.},
acronym = {{FoSSaCS}'03},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'03)},
author = {Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Lossy Channels Systems Is Probably
Decidable},
pages = {120-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-fossacs2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerSch-fossacs2003.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-fossacs2003.pdf},
abstract = {Lossy channel systems (LCS's) are systems of
finite state automata that communicate via unreliable
unbounded fifo channels. We propose a new probabilistic
model for these systems, where losses of messages are seen
as faults occurring with some given probability, and where
the internal behavior of the system remains
nondeterministic, giving rise to a reactive Markov chains
semantics. We then investigate the verification of
linear-time properties on this new model.}
}
@inproceedings{Bernat-spv2003,
address = {Marseilles, France},
month = sep,
year = 2003,
editor = {Rusinowitch, Micha{\"e}l},
acronym = {{SPV}'03},
booktitle = {{P}roceedings of the {W}orkshop
on {S}ecurity {P}rotocols {V}erification
({SPV}'03)},
author = {Bernat, Vincent},
title = {Towards a Logic for Verification of Security
Protocols},
pages = {31-35},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bernat-spv2003.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bernat-spv2003.ps}
}
@inproceedings{Bou-stacs-2003,
address = {Berlin, Germany},
month = feb,
year = 2003,
volume = 2607,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alt, Helmut and Habib, Michel},
acronym = {{STACS}'03},
booktitle = {{P}roceedings of the 20th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'03)},
author = {Bouyer, Patricia},
title = {Untameable Timed Automata!},
pages = {620-631},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-stacs2003.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-stacs2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-stacs2003.ps},
abstract = {Timed automata are a widely
studied model for real-time systems. Since
8~years, several tools implement this model and
are successfully used to verify real-life
examples. In spite of this well-established
framework, we prove that the forward analysis
algorithm implemented in these tools is not
correct! However, we also prove that it is
correct for a restricted class of timed
automata, which has been sufficient for modeling
numerous real-life systems.}
}
@article{CNNR-tocl03,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Comon, Hubert and Narendran, Paliath and
Nieuwenhuis, Robert and
Rusinowitch, Micha{\"e}l},
title = {Deciding the Confluence of Ordered Term Rewrite
Systems},
volume = {4},
number = {1},
pages = {33-55},
year = {2003},
month = jan
}
@inproceedings{ComCor-esop2003,
address = {Warsaw, Poland},
month = apr,
year = 2003,
volume = 2618,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo},
acronym = {{ESOP}'03},
booktitle = {{P}roceedings of the 12th
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'03)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
title = {Security properties: two agents are sufficient},
pages = {99-113},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierESOP03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierESOP03.ps}
}
@inproceedings{ComCor-rta2003,
address = {Valencia, Spain},
month = jun,
year = 2003,
volume = 2706,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nieuwenhuis, Robert},
acronym = {{RTA}'03},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'03)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
title = {New Decidability Results for Fragments of First-Order
Logic and Application to Cryptographic Protocols},
pages = {148-164},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-2.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-2.rr.ps}
}
@article{ComJac-IC2003,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Comon, Hubert and Jacquemard, Florent},
title = {Ground Reducibility is {EXPTIME}-complete},
volume = {187},
number = {1},
pages = {123-153},
year = {2003},
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJ-icomp.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJ-icomp.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CJ-icomp.ps}
}
@inproceedings{ComTre-mann03,
month = feb,
year = 2003,
volume = 2772,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dershowitz, Nachum},
acronym = {{V}erification: {T}heory and {P}ractice},
booktitle = {{V}erification: {T}heory and {P}ractice,
{E}ssays {D}edicated to {Z}ohar {M}anna on
the {O}ccasion of {H}is 64th {B}irthday},
author = {Comon{-}Lundh, Hubert and Treinen, Ralf},
title = {Easy Intruder Deductions},
pages = {225-242},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CT-manna.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CT-manna.ps}
}
@inproceedings{Del-spv2003,
address = {Marseilles, France},
month = sep,
year = 2003,
editor = {Rusinowitch, Micha{\"e}l},
acronym = {{SPV}'03},
booktitle = {{P}roceedings of the {W}orkshop
on {S}ecurity {P}rotocols {V}erification
({SPV}'03)},
author = {Delaune, St{\'e}phanie},
title = {Intruder Deduction Problem in Presence of Guessing
Attacks},
pages = {26-30},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Del-spv2003.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Del-spv2003.pdf},
abstract = {We present a decidability result in the context of
the verification of cryptographic protocols in presence of data
which take value in a finite known set. Since the perfect
cryptography assumption is unrealistic for cryptographic protocols
that employ weak data, we extend the conventional Dolev-Yao model
to consider guessing attacks, where an intruder guesses the values
of weak data and verify these guesses. We show that the intruder
deduction problem, i.e. the existence of guessing attack, can be
decided in polynomial time for the extended Dolev-Yao model.}
}
@mastersthesis{Delaune-dea2003,
author = {Delaune, St{\'e}phanie},
title = {V{\'e}rification de protocoles de s{\'e}curit{\'e}
dans un
mod{\`e}le de l'intrus {\'e}tendu},
year = {2003},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Delaune-dea2003.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Delaune-dea2003.ps}
}
@article{Demri02,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Demri, St{\'e}phane},
title = {A Polynomial-Space Construction of Tree-Like Models
for Logics with Local Chains of Modal Connectives},
volume = {300},
number = {1-3},
pages = {235-258},
year = {2003},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-tcs02.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs02.pdf},
doi = {10.1016/S0304-3975(02)00082-8}
}
@misc{Demri03,
author = {Demri, St{\'e}phane},
title = {({M}odal) Logics for Semistructured Data (Bis)},
year = 2003,
month = sep,
howpublished = {Invited talk, 3rd
{W}orkshop on {M}ethods for {M}odalities
({M4M}'03), Nancy, France}
}
@inproceedings{Demri::DeNivelle03b,
address = {Nancy, France},
month = sep,
year = 2003,
acronym = {{M4M-3}},
booktitle = {{P}roceedings of the 3rd
{W}orkshop on {M}ethods for {M}odalities
({M4M-3})},
author = {Demri, St{\'e}phane and de Nivelle, Hans},
title = {Relational Translations into {GF2}},
pages = {93-108}
}
@techreport{EVA-TR13,
author = {Cortier, V{\'e}ronique},
title = {A Guide for {SECURIFY}},
year = {2003},
month = dec,
number = 13,
institution = {projet RNTL~EVA},
oldhowpublished = {Rapport technique num\'ero 13 du projet RNTL EVA},
note = {9~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR13.pdf}
}
@techreport{EVA-TR9,
author = {Jacquemard, Florent},
title = {The {EVA} Translator, version~2},
year = {2003},
month = jul,
number = 9,
institution = {projet RNTL EVA},
oldhowpublished = {Rapport technique num\'ero 9 du projet RNTL EVA},
note = {38~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR9.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR9.pdf}
}
@misc{EVA2,
author = {Jacquemard, Florent},
title = {The {EVA} translator, version~2},
year = {2003},
month = jul,
oldhowpublished = {Available??},
note = {See~\cite{EVA-TR9} for description. Written in OCaml
(about 11000 lines)},
note-fr = {Voir~\cite{EVA-TR9} pour la description. \'Ecrit en OCaml
(environ 11000 lignes)}
}
@inproceedings{FAST-cav03,
address = {Boulder, Colorado, USA},
month = jul,
year = 2003,
volume = 2725,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
acronym = {{CAV}'03},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'03)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and
Petrucci, Laure},
title = {{FAST}: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
pages = {118-121},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps},
abstract = {FAST is a tool for the analysis
of infinite systems. This paper describes the
underlying theory, the architecture choices
that have been made in the tool design. The
user must provide a model to analyse, the
property to check and a computation policy.
Several such policies are proposed as a
standard in the package, others can be added by
the user. FAST capabilities are compared with
those of other tools. A range of case studies
from the literature has been investigated. }
}
@article{FPS-ICOMP,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Finkel, Alain and Purushothaman{ }Iyer, S. and
Sutre, Gr{\'e}goire},
title = {Well-Abstracted Transition Systems: {A}pplication to
{FIFO} Automata},
volume = {181},
number = {1},
pages = {1-31},
year = {2003},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FPS-ICOMP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FPS-ICOMP.ps}
}
@misc{Fast1-manual,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Petrucci, Laure
and Worobel, Laurent},
title = {{FAST} User's Manual},
year = {2003},
month = aug,
oldhowpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/fast/doc/manual.ps}},
note = {33~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-manual.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-manual.ps}
}
@misc{FinLer-FAST2002,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me},
title = {{FAST} v1.0: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
year = {2003},
month = jul,
oldhowpublished = {Available at \url{www.lsv.ens-cachan.fr/fast/}},
note = {See~\cite{FAST-cav03} for description. Written in C++
(about 4400 lines on top of the MONA v1.4 library)},
note-fr = {Voir~\cite{FAST-cav03} pour la description. \'Ecrit en C++
(environ 4400 lignes ajout\'ees \`a la biblioth\`eque MONA~v1.4)},
url = {http://www.lsv.ens-cachan.fr/fast/}
}
@inproceedings{GB03aplas,
address = {Beijing, China},
month = nov,
year = 2003,
volume = 2895,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ohori, Atsushi},
acronym = {{APLAS}'03},
booktitle = {{P}roceedings of the 1st {A}sian {S}ymposium
on {P}rogramming {L}anguages and {S}ystems
({APLAS}'03)},
author = {Galland, Antoine and Baudet, Mathieu},
title = {Controlling and Optimizing the Usage of One Resource},
pages = {195-211},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GB03aplas.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GB03aplas.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GB03aplas.pdf},
abstract = {This paper studies the problem of
resource availability in the context of mobile code
for embedded systems such as smart cards. It presents
an architecture dedicated to controlling the usage of
a single resource in a multi-process operating system.
Its specificity lies in its ability to improve the
task scheduling in order to spare resources. Our
architecture comprises two parts. The first statically
computes the resource needs using a dedicated lattice.
The second guarantees at runtime that there will
always be enough resources for every application to
terminate, thanks to an efficient deadlock-avoidance
algorithm. The example studied here is an
implementation on a JVM (Java Virtual Machine) for
smart cards, dealing with a realistic subset of the
Java bytecode.}
}
@inproceedings{GB03cfse,
address = {La Colle sur Loup, France},
month = oct,
year = 2003,
publisher = {INRIA},
editor = {Auguin, Michel and Baude, Fran{\c{c}}oise and
Lavenier, Dominique and Riveill, Michel},
acronym = {{CFSE}'03},
booktitle = {{A}ctes de la 3{\`e}me {C}onf{\'e}rence
{F}ran{\c{c}}aise sur les {S}yst{\`e}mes
d'{E}xploitation
({CFSE}'03)},
author = {Galland, Antoine and Baudet, Mathieu},
title = {{\'E}conomiser l'or du banquier},
pages = {638-649},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GB03cfse.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GB03cfse.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GB03cfse.pdf}
}
@misc{INTERFAST,
author = {Worobel, Laurent},
title = {{INTERFAST}~v1.0: {A}~{GUI} for {FAST}},
year = {2003},
month = aug,
oldhowpublished = {Available at \url{www.lsv.ens-cachan.fr/fast/}},
note = {See~\cite{Fast1-manual} for description. Written in
Java (6300 lines) and C (1600 lines), using Java Cup},
note-fr = {Voir~\cite{Fast1-manual} pour la description. \'Ecrit en
Java (6300 lignes) et C (1600 lignes), utilise Java Cup},
url = {http://www.lsv.ens-cachan.fr/fast/}
}
@article{JGL:S4:geometry,
lsv-note = {Published in partnership with International Press},
publisher = {HHA Publications},
journal = {Homology, Homotopy and Applications},
author = {Goubault{-}Larrecq, Jean and Goubault, {\'E}ric},
title = {On the Geometry of Intuitionistic {S4} Proofs},
volume = {5},
number = {2},
pages = {137-209},
year = {2003},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/S4G.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/S4G.ps}
}
@techreport{JGL:dico:3.3,
author = {Demri, St{\'e}phane and Ducass{\'e}, Mireille and
Goubault{-}Larrecq, Jean
and M{\'e}, Ludovic and Olivain, Julien and
Picaronny, Claudine and
Pouzol, Jean-{\relax Ph}ilippe and
Totel, {\'E}ric and Vivinis, Bernard},
title = {Algorithmes de d{\'e}tection et langages de
signatures},
year = {2003},
month = oct,
type = {Contract Report},
number = {(Sous-projet~3, livrable~3)},
institution = {projet RNTL DICO},
oldhowpublished = {Sous-projet 3, livrable 3 du projet RNTL DICO.
Version~1},
note = {72~pages}
}
@article{Jac-IPL03,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Jacquemard, Florent},
title = {Reachability and Confluence are Indecidable for
Flat
Term Rewriting Systems},
volume = {87},
number = {5},
pages = {265-270},
year = {2003},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-6.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-6.rr.ps}
}
@inproceedings{KNT-icfem2003,
address = {Singapore},
month = nov,
year = 2003,
volume = 2885,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Song Dong, Jin and Woodcock, Jim},
acronym = {{ICFEM}'03},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {F}ormal {E}ngineering
{M}ethods
({ICFEM}'03)},
author = {Kerb{\oe}uf, Micka{\"e}l and Nowak, David and
Talpin, Jean-Pierre},
title = {Formal Proof of a Polychronous Protocol for Loosely
Time-Triggered Architectures},
pages = {359-374},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KNT-icfem03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KNT-icfem03.ps}
}
@book{LLSdFbook-2003,
editor = {David, {\relax Ph}ilippe and Waeselynck, H{\'e}l{\`e}ne},
title = {Logiciel libre et s{\^u}ret{\'e} de fonctionnement:
cas des syst{\`e}mes critiques},
year = {2003},
publisher = {Herm{\`e}s},
oldpublisher = {Herm\`es Lavoisier},
oldnote = {Ouvrage collectif r\'edig\'e sous la direction
de Ph.~David et H.~Waeselynck},
isbn = {2-7462-0727-3},
url = {http://www.lavoisier.fr/fr/livres/index.asp?texte=2746207270&select=isbn}
}
@inproceedings{LP-LK-JB-ZQ-02,
address = {Guimar{\~a}es, Portugal},
month = jun,
year = 2003,
publisher = {{IEEE} Computer Society Press},
editor = {Lilius, Johan and Balarin, Felice and
Machado, Ricardo J.},
acronym = {{ACSD}'03},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'03)},
author = {Petrucci, Laure and Kristensen, Lars M. and
Billington, Jonathan and
Qureshi, Zahid H.},
title = {Developing a Formal Specification for the Mission
System of a Maritime Surveillance Aircraft},
pages = {92-101},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PKBQ-ACSD.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PKBQ-ACSD.ps}
}
@techreport{LSV:03:1,
author = {Comon{-}Lundh, Hubert and Shmatikov, Vitaly},
title = {Constraint Solving, Exclusive Or and the Decision
of
Confidentiality for Security Protocols Assuming a
Bounded Number of Sessions},
type = {Research Report},
number = {LSV-03-1},
year = {2003},
month = jan,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-1.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-1.rr.ps}
}
@techreport{LSV:03:10,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Traces of Randomized Distributed Algorithms As
{M}arkov Fields. {A}pplication to Rapid Mixing},
type = {Research Report},
number = {LSV-03-10},
year = {2003},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-10.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-10.rr.ps}
}
@techreport{LSV:03:12,
author = {Baclet, Manuel},
title = {Logical Characterization of Aperiodic Data Languages},
type = {Research Report},
number = {LSV-03-12},
year = {2003},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-12.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-12.rr.ps}
}
@techreport{LSV:03:15,
author = {Delaune, St{\'e}phanie},
title = {V{\'e}rification de protocoles de s{\'e}curit{\'e} dans un
mod\`ele de l'intrus {\'e}tendu},
type = {Research Report},
number = {LSV-03-15},
year = 2003,
month = nov,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
fulladdress = lsvaddr,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-15.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-15.rr.ps},
abstract = {La difficult\'e de la conception des protocoles de
s\'ecurit\'e tient au fait que les messages \'echang\'es peuvent
\^etre \'ecout\'es, intercept\'es ou modifi\'es par une tierce
personne: la fiabilit\'e de ces protocoles d\'epend donc du
pouvoir de d\'eduction que l'on donne \`a l'intrus.\par
Ce m\'emoire contient d'une part la formalisation et
l'\'etude d'un nouveau mod\`ele d'intrus \'etendant le mod\`ele
standard de Dolev-Yao pour prendre en compte les attaques
par pr\'edictions, et d'autre part une pr\'esentation de
r\'esultats utiles pour la v\'erification pratique des
protocoles.}
}
@techreport{LSV:03:7,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {On the Absence of Phase Transition in Randomized
Distributed Algorithms},
type = {Research Report},
number = {LSV-03-7},
year = {2003},
month = apr,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-7.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-7.rr.ps}
}
@inproceedings{LazNow-tlca2003,
address = {Valencia, Spain},
month = jun,
year = 2003,
volume = 2701,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hofmann, Martin},
acronym = {{TLCA}'03},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {T}yped {L}ambda {C}alculi
and {A}pplications
({TLCA}'03)},
author = {Lazi{\'c}, Ranko and Nowak, David},
title = {On a Semantic Definition of Data Independence},
pages = {226-240},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-LazNow.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-LazNow.ps}
}
@misc{MR:MOP,
author = {Roger, Muriel},
title = {{MOP}: {MO}dular {P}rover},
year = {2003},
note = {See description in~\cite{THESE-ROGER-2003,GLRV:acm}.
Written in OCaml (9611 lines)},
note-fr = {Voir la description dans~\cite{THESE-ROGER-2003,GLRV:acm}.
\'Ecrit en OCaml (9611 lignes)}
}
@inproceedings{MarSch-concur2003,
address = {Marseilles, France},
month = aug,
year = 2003,
volume = 2761,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto M. and Lugiez, Denis},
acronym = {{CONCUR}'03},
booktitle = {{P}roceedings of the 14th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'03)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking a Path (Preliminary Report)},
pages = {251-265},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-concur03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MarSch-concur03.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-concur03.pdf},
doi = {10.1007/b11938},
abstract = {We consider the problem of checking whether a finite (or
ultimately periodic) run satisfies a temporal logic formula. This problem
is at the heart of {"}runtime verification{"} but it also appears in many other
situations. By considering several extended temporal logics, we show that
the problem of model checking a path can usually be solved efficiently,
and profit from specialized algorithms. We further show it is possible to
efficiently check paths given in compressed form.}
}
@inproceedings{Sch-icalp2003,
address = {Eindhoven, The Netherlands},
month = jun,
year = 2003,
volume = 2719,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos C. M. and Lenstra, Jan Karel and
Parrow, Joachim and Woeginger, Gerhard J.},
acronym = {{ICALP}'03},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'03)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Oracle circuits for branching-time model checking},
pages = {790-801},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-icalp03-long.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-icalp03-long.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-icalp03-long.pdf},
abstract = {A special class of oracle
circuits with tree-vector form is introduced.
It is shown that they can be evaluated in
deterministic polynomial-time with a polylog
number of adaptive queries to an NP oracle.
This framework allows us to evaluate the
precise computational complexity of model
checking for some branching-time logics where
it was known that the problem is NP-hard and
coNP-hard.}
}
@phdthesis{THESE-BOISSEAU-2003,
author = {Boisseau, Alexandre},
title = {Abstractions pour la v{\'e}rification de
propri{\'e}t{\'e}s de
s{\'e}curit{\'e} de protocoles cryptographiques},
year = {2003},
month = sep,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Boisseau-these.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Boisseau-these.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Boisseau-these.pdf}
}
@phdthesis{THESE-CORTIER-2003,
author = {Cortier, V{\'e}ronique},
title = {V{\'e}rification automatique des protocoles
cryptographiques},
year = {2003},
month = mar,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cortier-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cortier-these.ps}
}
@phdthesis{THESE-DUFLOT-2003,
author = {Duflot, Marie},
title = {Algorithmes distribu{\'e}s sur des anneaux
param{\'e}tr{\'e}s~---
{P}reuves de convergence probabiliste et
d{\'e}terministe},
year = {2003},
month = sep,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Duflot-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Duflot-these.ps}
}
@phdthesis{THESE-LEROUX-2003,
author = {Leroux, J{\'e}r{\^o}me},
title = {Algorithmique de la v{\'e}rification des
syst{\`e}mes {\`a}
compteurs. {A}pproximation et acc{\'e}l{\'e}ration.
{I}mpl{\'e}mentation de l'outil~{FAST}},
year = {2003},
month = dec,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Leroux-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Leroux-these.ps}
}
@phdthesis{THESE-MARKEY-2003,
author = {Markey, Nicolas},
title = {Logiques temporelles pour la v{\'e}rification:
expressivit{\'e}, complexit{\'e}, algorithmes},
year = {2003},
month = apr,
type = {Th{\`e}se de doctorat},
school = {Laboratoire d'Informatique Fondamentale d'Orl{\'e}ans,
France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-these.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Markey-these.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-these.pdf}
}
@phdthesis{THESE-ROGER-2003,
author = {Roger, Muriel},
title = {Raffinements de la r{\'e}solution et
v{\'e}rification de
protocoles cryptographiques},
year = {2003},
month = oct,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Roger-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Roger-these.ps}
}
@phdthesis{THESE-VERMA-2003,
author = {Verma, Kumar N.},
title = {Automates d'arbres bidirectionnels modulo
th{\'e}ories {\'e}quationnelles},
year = {2003},
month = sep,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Verma-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Verma-these.ps}
}
@misc{TSMVv1.0,
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {{TSMV}~v1.0},
year = {2003},
month = oct,
howpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~markey/TSMV/}},
note = {See description in~\cite{MS-formats2004}. Written in C
(about 4000~lines on top of NuSMV v2.1.2)},
note-fr = {Voir la description dans~\cite{MS-formats2004}. \'Ecrit en C
(environ 4000~lignes \`ajout\'ees \`a NuSMV~v2.1.2)},
url = {http://www.lsv.ens-cachan.fr/~markey/TSMV/}
}
@inproceedings{ZhaNow-csl2003,
address = {Vienna, Austria},
month = aug,
year = 2003,
volume = 2803,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baaz, Matthias and Makowsky, Johann A.},
acronym = {{CSL}'03},
booktitle = {{P}roceedings of the 17th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'03)},
author = {Zhang, Yu and Nowak, David},
title = {Logical Relations for Dynamic Name Creation},
pages = {575-588},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ZN-csl2003.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ZN-csl2003.ps}
}
@techreport{artist-W1A2N1Y1,
author = {Jonsson, Bengt and others},
title = {Roadmap on Component-based Design and Integration
Platforms},
year = {2003},
month = may,
type = {Contract Report},
number = {(Deliverable W1.A2.N1.Y1)},
institution = {European Project IST-2001-34820
{"}ARTIST{"} Advanced Real-Time Systems},
oldhowpublished = {Deliverable W1.A2.N1.Y1 of European Project
IST-2001-34820 ``ARTIST'' Advanced Real-Time Systems},
note = {78~pages}
}
@article{bhk-tcs-fossacs01,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bidoit, Michel and Hennicker, Rolf and
Kurz, Alexander},
title = {Observational Logic, Constructor-Based Logic, and
their Duality},
volume = {298},
number = {3},
pages = {471-510},
year = {2003},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-TCS-FOSSACS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-TCS-FOSSACS01.ps}
}
@inproceedings{comon03lics,
address = {Ottawa, Canada},
month = jun,
year = 2003,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'03},
booktitle = {{P}roceedings of the 18th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'03)},
author = {Comon{-}Lundh, Hubert and Shmatikov, Vitaly},
title = {Intruder Deductions, Constraint Solving and Insecurity
Decision in Presence of Exclusive Or},
pages = {271-280}
}
@incollection{couvreur-chap03,
author = {Couvreur, Jean-Michel and Poitrenaud, Denis},
title = {{D}{\'e}pliage pour la v{\'e}rification de
propri{\'e}t{\'e}s temporelles},
chapter = {3},
editor = {Michel Diaz},
booktitle = {V{\'e}rification et mise en {\oe}uvre des
r{\'e}seaux de {P}etri~--- Tome~2},
pages = {127-161},
year = {2003},
month = jan,
publisher = {Herm{\`e}s}
}
@inproceedings{couvreur-lpar03,
address = {Almaty, Kazakhstan},
month = sep,
year = 2003,
volume = 2850,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Vardi, Moshe Y. and Voronkov, Andrei},
acronym = {{LPAR}'03},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'03)},
author = {Couvreur, Jean-Michel and Saheb, Nasser and
Sutre, Gr{\'e}goire},
title = {An Optimal Automata Approach to {LTL} Model Checking
of Probabilistic Systems},
pages = {361-375},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CSS-lpar03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CSS-lpar03.ps}
}
@misc{fl-cours-etr2003,
author = {Laroussinie, Fran{\c{c}}ois},
title = {Automates temporis{\'e}s et hybrides,
mod{\'e}lisation et
v{\'e}rification},
year = {2003},
month = sep,
howpublished = {Invited lecture, \'ecole d'\'et\'e ETR 2003 (\'Ecole Temps
R\'eel), Toulouse, France}
}
@inproceedings{invLP-ICATPN-03,
address = {Eindhoven, The Netherlands},
month = jun,
year = 2003,
volume = 2679,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van der Aalst, Wil M. P. and Best, Eike},
acronym = {{ICATPN}'03},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN}'03)},
author = {Billington, Jonathan and Christensen, S{\o}ren and
van Hee, Kees M. and
Kindler, Ekkart and Kummer, Olaf and
Petrucci, Laure and Post, Reinier and
Stehno, {\relax Ch}ristian and Weber, Michael},
title = {The {P}etri {N}et {M}arkup {L}anguage: {C}oncepts,
Technology and Tools},
pages = {483-505},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PNML-ATPN03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PNML-ATPN03.ps}
}
@article{lst-TCS2001,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe and
Turuani, Mathieu},
title = {On the Expressivity and Complexity of Quantitative
Branching-Time Temporal Logics},
volume = {297},
number = {1-3},
pages = {297-315},
year = {2003},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LST-TCS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LST-TCS01.ps},
doi = {10.1016/S0304-3975(02)00644-8},
abstract = {We investigate extensions of
CTL allowing to express quantitative
requirements about an abstract notion of time
in a simple discrete-time framework, and
study the expressive power of several
relevant logics.\par
When only subscripted modalities are used,
polynomial-time model checking is possible
even for the largest logic we consider, while
the introduction of freeze quantifiers leads
to a complexity blow-up.}
}
@article{markey-beatcs,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Markey, Nicolas},
title = {Temporal Logic with Past is Exponentially More
Succinct},
volume = {79},
pages = {122-128},
year = {2003},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-succinct.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/NM-succinct.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-succinct.pdf},
abstract = {We positively answer the old question whether temporal logic with
past is more succinct than pure-future temporal logic. Surprisingly,
the proof is quite simple and elementary, although the question
has been open for twenty years.}
}
@mastersthesis{mongi-dea2003,
author = {Ben{ }Gaid, Mongi},
title = {Mod{\'e}lisation et v{\'e}rification des aspects
temporis{\'e}s des langages pour automates
programmables
industriels},
year = {2003},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Informatique Distribu{\'e}e, Orsay, France},
note = {68~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mongi-dea2003.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mongi-dea2003.pdf}
}
@inproceedings{phs-aiml02,
address = {Toulouse, France},
unsure-month = sep,
unsure-nmonth = 9,
year = 2003,
optaddress = {London, UK},
publisher = {King's College Publication},
editor = {Balbiani, {\relax Ph}ilippe and Suzuki, Nobu-Yuki
and Wolter, Frank and Zakharyaschev, Michael},
acronym = {{AiML}'02},
booktitle = {{S}elected {P}apers from the 4th
{W}orkshop on {A}dvances in {M}odal {L}ogics
({AiML}'02)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The Complexity of Temporal Logic Model Checking},
chapter = {19},
pages = {393-436},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-aiml02.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf}
}
@misc{phs-svhss2003,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Branching-Time Temporal Logics},
year = {2003},
month = may,
howpublished = {Invited talk, Franco-Israeli Workshop on Semantics and
Verification of Hardware and Software Systems,
Tel-Aviv, Israel}
}
@misc{securify2,
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {{Securify} version~2},
year = {2003},
missingmonth = {},
missingnmonth = {},
oldhowpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~cortier/EVA/securify2.tar.gz}},
note = {See~\cite{EVA-TR13} for description. Written in Caml
(about 3300 lines)},
note-fr = {Voir~\cite{EVA-TR13} pour la description. \'Ecrit en Caml
(environ 3300 lignes)},
url = {http://www.lsv.ens-cachan.fr/~cortier/EVA/securify2.tar.gz}
}
@misc{spore,
author = {Jacquemard, Florent},
title = {{SPORE}: {S}ecurity {P}rotocols {O}pen {RE}pository},
year = {2003},
month = jul,
oldhowpublished = {A base of protocol descriptions, reachable at
\url{www.lsv.ens-cachan.fr/spore}},
note = {Works with Perl scripts (about 1200 lines) and
contains about 50 protocol descriptions (as of Aug.~2004)},
note-fr = {Utilise des scripts Perl (environ 1200 lignes),
contient environ 50 descriptions de protocoles (en Ao\^ut~2004)},
url = {http://www.lsv.ens-cachan.fr/spore/}
}
@misc{symprod-02,
author = {Petrucci, Laure},
title = {{\ttfamily symprod}: construction et analyse du
produit
synchronis{\'e} modulaire d'automates},
year = {2003},
missingmonth = {},
missingnmonth = {},
nonote = {See~\cite{CL-LP-ACSD04} for description. Written in C
(about 3700 lines)},
nmnote = {J'ai commente la note ci-dessus car CL-LP-ACSD04 est 'ant'
(en fait, posterieur au depart de Laure)},
nmothernote = {URL invalide...}
}
@inproceedings{verma:lpar03,
address = {Almaty, Kazakhstan},
month = sep,
year = 2003,
volume = 2850,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Vardi, Moshe Y. and Voronkov, Andrei},
acronym = {{LPAR}'03},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'03)},
author = {Verma, Kumar N.},
title = {On Closure under Complementation of Equational Tree
Automata for Theories Extending~{AC}},
pages = {183-195},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Verma-lpar03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Verma-lpar03.ps}
}
@inproceedings{verma:rta03,
address = {Valencia, Spain},
month = jun,
year = 2003,
volume = 2706,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nieuwenhuis, Robert},
acronym = {{RTA}'03},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'03)},
author = {Verma, Kumar N.},
title = {Two-Way Equational Tree Automata for {AC}-like
Theories: {D}ecidability and Closure Properties},
pages = {180-196},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ver-rta03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ver-rta03.ps}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
This file was generated by bibtex2html 1.98.