@article{CL-tsi06,
  publisher = {Herm{\`e}s},
  journal = {Technique et Science Informatiques},
  author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
  editor = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
  title = {Contr{\^o}le des applications temps-r{\'e}el~: mod{\`e}les
                  temporis{\'e}s et hybrides},
  volume = 25,
  number = 3,
  year = 2006,
  url = {http://www.lavoisier.fr/notice/fr2746214830.html}
}
@incollection{jgl-encyc06,
  author = {Goubault{-}Larrecq, Jean},
  title = {Preuve et v{\'e}rification pour la s{\'e}curit{\'e} 
	  et la s{\^u}ret{\'e}},
  booktitle = {Encyclop{\'e}die de l'informatique et des syst{\`e}mes 
	  d'information},
  editor = {Akoka, Jacky and Comyn-Wattiau, Isabelle},
  pages = {683-703},
  publisher = {Vuibert},
  year = 2006,
  month = dec,
  chapter = {I.6},
  url = {http://www.vuibert.com/livre12401.html},
  abstract = {La s\^uret\'e, comme la s\'ecurit\'e, \'enonce qu'un mal n'arrive
  jamais.  Le but de cet article est de d\'efinir la notion de propri\'et\'e
  de s\^uret\'e, et d'en d\'ecrire quelques techniques de v\'erification et de
  preuve~: model-checking, interpr\'etation abstraite notamment.  Apr\`es
  avoir remarqu\'e qu'il n'y avait pas de s\'ecurit\'e sans s\^uret\'e, il est
  expliqu\'e que l'analyse de s\'ecurit\'e d'un syst\`eme repose sur un
  mod\`ele, des hypoth\`eses, des propri\'et\'es \`a v\'erifier, et une
  architecture de s\'ecurit\'e.  Finalement, il est donn\'e un aper\c{c}u de
  quelques mod\`eles et m\'ethodes de preuve de protocoles
  cryptographiques.}
}
@inproceedings{BJ-secret06,
  address = {Venice, Italy},
  month = jul,
  year = 2006,
  editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude},
  acronym = {{SecReT}'06},
  booktitle = {{P}reliminary {P}roceedings of the 1st 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'06)},
  author = {Bouhoula, Adel and Jacquemard, Florent},
  title = {Security Protocols Verification with Implicit Induction and 
		  Explicit Destructors},
  pages = {37-44},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf},
  abstract = {We present a new method for automatic implicit induction theorem
proving, and its application for the verification of a key distribution
cryptographic protocol. The~method can handle axioms between constructor
terms, a~feature generally not supported by other induction procedure. We~use
such axioms in order to specify explicit destructors representing
cryptographic operators.}
}
@inproceedings{BBS-forte06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4229,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Najm, Elie and Pradat{-}Peyre, Jean-Fran{\c{c}}ois and
             Vigui{\'e} Donzeau-Gouge, V{\'e}ronique},
  acronym = {{FORTE}'06},
  booktitle = {{P}roceedings of 26th {IFIP} {WG6.1} 
           {I}nternational {C}onference on {F}ormal
           {T}echniques for {N}etworked and {D}istributed {S}ystems
	   ({FORTE}'06)},
  author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
  title = {Symbolic verification of communicating systems with
		  probabilistic message losses: liveness and fairness},
  pages = {212-227},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-forte06.ps},
  doi = {10.1007/11888116_17},
  abstract = {NPLCS's are a new model for nondeterministic channel systems
	where unreliable communication is modeled by probabilistic message losses.
	We~show that, for \(\omega\)-regular linear-time properties and finite-memory
	schedulers, qualitative model-checking is decidable. The~techniques extend
	smoothly to questions where fairness restrictions are imposed on the
	schedulers. The~symbolic procedure underlying our decidability proofs has been
	implemented and used to study a simple protocol handling two-way transfers in
	an unreliable setting.}
}
@inproceedings{BP06,
  address = {Taipei, Taiwan},
  month = aug,
  year = 2006,
  volume = 4094,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Ibarra, Oscar H. and Yen, Hsu-Chun},
  acronym = {{CIAA}'06},
  booktitle = {{P}roceedings of the 11th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'06)},
  author = {Baclet, Manuel and Pagetti, Claire},
  title = {Around {H}opcroft's Algorithm},
  pages = {114-125},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf},
  doi = {10.1007/11812128_12},
  abstract = {In this paper, a reflection is made on an indeterminism inherent
to Hopcroft's minimization algorithm: the splitter choice. We have implemented
two natural policies (FIFO and~FILO) for managing the set of splitters for
which we obtain the following practical results: the FILO strategy performs
better than the FIFO strategy, in the case of a one letter alphabet, the FILO
practical complexity never exceeds a linear one and our implementation is more
efficient than the minimization algorithm of the FSM tool. This implementation
is being integrated in a finite automata library, the Dash library. Thus, we
present an efficient manner to manipulate automata by using canonical minimal
automata.}
}
@inproceedings{abw-fossacs2006,
  address = {Vienna, Austria},
  month = mar,
  year = 2006,
  volume = 3921,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna},
  acronym = {{FoSSaCS}'06},
  booktitle = {{P}roceedings of the 9th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'06)},
  author = {Abadi, Mart{\'\i}n and Baudet, Mathieu and 
		Warinschi, Bogdan},
  title = {Guessing Attacks and the Computational Soundness of 
		Static Equivalence},
  pages = {398-412},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABW_Fossacs06.ps},
  doi = {10.1007/11690634_27},
  abstract = {The indistinguishability of two pieces of 
	data (or two lists of pieces of data) can be 
	represented formally in terms of a relation called 
	static equivalence. Static equivalence depends on an 
	underlying equational theory. The choice of an 
	inappropriate equational theory can lead to overly 
	pessimistic or overly optimistic notions of 
	indistinguishability, and in turn to security criteria 
	that require protection against impossible attacks 
	or ---worse yet--- that ignore feasible ones.  In this 
	paper, we define and justify an equational theory for 
	standard, fundamental cryptographic operations. This 
	equational theory yields a notion of static equivalence 
	that implies computational indistinguishability. Static 
	equivalence remains liberal enough for use in 
	applications. In particular, we develop and analyze a 
	principled formal account of guessing attacks in terms 
	of static equivalence.}
}
@inproceedings{BKRS-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Bozzelli, Laura and K{\v{r}}et{\'\i}nsk{\'y}, Mojm{\'\i}r and
                 {\v{R}}eh{\'a}k, Vojt{\v{e}}ch and Strej{\v c}ek, Jan},
  title = {On Decidability of {LTL} Model Checking for Process Rewrite Systems},
  pages = {248-259},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf},
  doi = {10.1007/11944836_24}
}
@inproceedings{BLMR-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas and
		 Rasmussen, Jacob Illum},
  title = {Almost Optimal Strategies in One-Clock Priced Timed Automata},
  pages = {345-356},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMR-fsttcs06.ps},
  doi = {10.1007/11944836_32},
  abstract = {We consider timed games extended with cost information, and
      prove computability of the optimal cost and of \(\epsilon\)-optimal memoryless
      strategies in timed games with one~clock. In~contrast, this problem has
      recently been proved undecidable for timed games with three clocks.}
}
@proceedings{GDV06,
  editor = {Bouyer, Patricia and Madhusudan, P.},
  title = {Proceedings of the 3rd Workshop on Games in Design and Verification
		({GDV}'06)},
  booktitle = {Proceedings of the 3rd Workshop on Games in Design and Verification
		({GDV}'06)},
  address = {Seattle, Washington, USA},
  year = 2006,
  month = aug
}
@inproceedings{BBBL-atva06,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia 
		 and Laroussinie, Fran{\c{c}}ois},
  title = {Timed temporal logics for abstracting transient states},
  pages = {337-351},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
  doi = {10.1007/11901914_26},
  abstract = {In previous work, the timed logic TCTL was extended with an
{"}almost everywhere{"} Until modality which abstracts negligible sets of
positions (i.e.,~with a null duration) along a run of a timed automaton. 
We~propose here an extension of this logic with more powerful modalities, in 
order to specify properties abstracting transient states, which are events
that last for less than k time units. Our main result is that modelchecking
is still decidable and PSPACE-complete for this extension. On the other
hand, a second semantics is defined, in which we consider the total duration
where the property does not hold along a run. In~this case, we prove that
model-checking is undecidable.}
}
@inproceedings{BBC-concur06,
  address = {Bonn, Germany},
  month = aug,
  year = 2006,
  volume = 4137,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Baier, Christel and Hermanns, Holger},
  acronym = {{CONCUR}'06},
  booktitle = {{P}roceedings of the 17th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'06)},
  author = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice},
  title = {Controller Synthesis for {MTL} Specifications},
  pages = {450-464},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-concur06.ps},
  doi = {10.1007/11817949_30},
  abstract = {We consider the control problem for timed automata
  against specifications given as MTL formulas. The logic MTL is a
  linear-time timed temporal logic which extends LTL with timing
  constraints on modalities, and recently, its model-checking has been
  proved decidable in several cases. We investigate these decidable
  fragments of MTL (full MTL when interpreted over finite timed
  words, and SafetyMTL when interpreted over infinite timed words),
  and prove two kinds of results. (1)~We first prove that,
  contrary to model-checking, the control problem is
  undecidable. Roughly, the computation of a lossy channel system
  could be encoded as a model-checking problem, and we prove here that
  a perfect channel system can be encoded as a control
  problem. (2)~We then prove that if we fix the resources
  of the controller (by resources we mean clocks and constants that
  the controller can use), the control problem becomes decidable. This
  decidability result relies on properties of well (and better)
  quasi-orderings.}
}
@article{BBLP-STTT05,
  publisher = {Springer},
  journal = {International Journal on Software Tools 
             for Technology Transfer},
  author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim G.
		   and Pel{\'a}nek, Radek},
  title = {Lower and Upper Bounds in Zone-Based Abstractions of 
		  Timed Automata},
  year = 2006,
  month = jun,
  pages = {204-215},
  number = 3,
  volume = 8,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-STTT05.ps},
  doi = {10.1007/s10009-005-0190-0},
  abstract = {The semantics of timed automata is 
	defined using an infinite-state transition system. 
	For verification purposes, one usually uses zone 
	based abstractions w.r.t.~the maximal constants to 
	which clocks of the timed automaton are compared. 
	We show that by distinguishing maximal lower and 
	upper bounds, significantly coarser abstractions 
	can be obtained. We show soundness and 
	completeness of the new abstractions 
	w.r.t.~reachability. We demonstrate how 
	information about lower and upper bounds can be 
	used to optimise the algorithm for bringing a 
	difference bound matrix into normal form. Finally, 
	we experimentally demonstrate that the new 
	techniques dramatically increases the scalability 
	of the real-time model checker~{\scshape 
	Uppaal}.}
}
@article{BC06-beatcs,
  publisher = {European Association for 
                 Theoretical Computer Science},
  journal = {EATCS Bulletin},
  author = {Bouyer, Patricia and Chevalier, Fabrice},
  title = {On the Control of Timed and Hybrid Systems},
  volume = 89,
  year = {2006},
  month = jun,
  pages = {79-96},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC-beatcs89.ps},
  abstract = {In this paper, we survey some of the results which have
	been obtained the last ten years on the control of hybrid and timed
	systems.}
}
@inproceedings{BBC-lics2006,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'06},
  booktitle = {{P}roceedings of the 21st
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'06)},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and 
		  Chevalier, Fabrice},
  title = {Control in o-Minimal Hybrid Systems},
  pages = {367-378},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lics06.ps},
  doi = {10.1109/LICS.2006.22},
  abstract = {In this paper, we consider 
	the control of general hybrid systems. In 
	this context we show that time-abstract 
	bisimulation is not adequate for solving 
	such a problem. That is why we consider 
	an other equivalence, namely the suffix 
	equivalence based on the encoding of 
	trajectories through words. We show that 
	this suffix equivalence is in general a 
	correct abstraction for control problems. 
	We apply this result to o-minimal hybrid 
	systems, and get decidability and 
	computability results in this framework.}
}
@inproceedings{BLP-cav06,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  volume = 4144,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ball, {\relax Th}omas and Jones, Robert B.},
  acronym = {{CAV}'06},
  booktitle = {{P}roceedings of the 18th
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'06)},
  author = {Bardin, S{\'e}bastien and Leroux, J{\'e}r{\^o}me and Point, G{\'e}rald},
  title = {{FAST} {E}xtended {R}elease},
  pages = {63-66},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLP-cav06.ps},
  doi = {10.1007/11817963_9},
  abstract = {{\scshape Fast} is a tool designed for the analysis of
counter systems, \emph{i.e.}~automata extended with unbounded integer variables.
Despite the reachability set is not recursive in general, Fast implements
several innovative techniques such as acceleration and circuit selection to
solve this problem in practice. In its latest version, the tool is built upon
an open architecture: the Presburger library is manipulated through a clear
and convenient interface, thus any Presburger arithmetics package can be
plugged to the tool. We provide four implementations of the interface using
Lash, Mona, Omega and a new shared automata package with computation cache.
Finally new features are available, like different acceleration algorithms.}
}
@inproceedings{BFLS-avis06,
  address = {Vienna, Austria},
  month = apr,
  year = 2006,
  editor = {Bharadwaj, Ramesh},
  acronym = {{AVIS}'06},
  booktitle = {{P}roceedings of the 5th {I}nternational
               {W}orkshop on {A}utomated {V}erification
               of {I}nfinite-{S}tate {S}ystems
               ({AVIS}'06)},
  author = {Bardin, S{\'e}bastien and Finkel, Alain and Lozes, {\'E}tienne
		 and Sangnier, Arnaud},
  title = {From Pointer Systems to Counter Systems Using Shape Analysis},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS-AVIS-06.ps},
  abstract = {We aim at checking safety properties on systems 
	manipulating dynamic linked lists. First we prove that every 
	pointer system is bisimilar to an effectively constructible 
	counter system. We then deduce a two-step analysis procedure. 
	We first build an over-approximation of the reachability set 
	of the pointer system. If this over-approximation is too 
	coarse to conclude, we then extract from it a bisimilar 
	counter system which is analyzed via efficient symbolic 
	techniques developed for general counter systems.}
}
@inproceedings{edos2006wsl,
  address = {Porto Allegre, Brazil},
  month = apr,
  year = 2006,
  editor = {Berger, Olivier},
  acronym = {{IWFS}'06},
  booktitle = {{P}roceedings of the {I}nternational
           {W}orkshop on {F}ree {S}oftware
           ({IWFS}'06)},
  author = {Boender, Jaap and Di Cosmo, Roberto and Durak, Berke and Leroy, Xavier
            and Mancinelli, Fabio and Morgado, Mario and Pinheiro, David and
	   Treinen, Ralf and  Trezentos, Paulo and Vouillon, J{\'e}r{\^o}me},
  title = {News from the {EDOS} project: improving the maintenance of free
               software distributions},
  pages = {199-207},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf},
  abstract = {The EDOS research project aims 
	at contributing to the quality assurance of free software 
	distributions. This is a major technical and engineering 
	challenge, due to the size and complexity of these 
	distributions (tens of thousands of software packages). We 
	present here some of the challenges that we have tackled so 
	far, and some of the advanced tools that are already 
	available to the community as an outcome of the first year 
	of work. }
}
@inproceedings{edos2006ase,
  address = {Tokyo, Japan},
  month = sep,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{ASE}'06},
  booktitle = {{P}roceedings of the 21st {IEEE}/{ACM} {I}nternational
           {C}onference on {A}utomated {S}oftware {E}ngineering
           ({ASE}'06)},
  author = {Mancinelli, Fabio and Boender, Jaap and Di Cosmo, Roberto and
            Vouillon, J{\'e}r{\^o}me and Durak, Berke and Leroy, Xavier 
	    and Treinen, Ralf},
  title = {Managing the Complexity of Large Free and Open Source
           Package-Based Software Distributions},
  pages = {199-208},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf},
  doi = {10.1109/ASE.2006.49},
  abstract = {The widespread adoption of Free and Open Source Software~(FOSS)
in many strategic contexts of the information technology society has drawn the
attention on the issues regarding how to handle the complexity of assembling
and managing a huge number of (packaged) components in a consistent and
effective~way. FOSS~distributions (and~in particular GNU\slash Linux-based~ones)
have always provided tools for managing the tasks of installing, removing and
upgrading the (packaged) components they were made~of. While these tools
provide a (not always effective) way to handle these tasks on the client side,
there is still a lack of tools that could help the distribution editors to
maintain, on the server side, large and high-quality distributions. In~this
paper we present our research whose main goal is to fill this gap: we~show our
approach, the tools we have developed and their application with experimental
results. Our~contribution provides an effective and automatic way to support
distribution editors in handling those issues that were, until now, mostly
addressed using ad-hoc tools and manual techniques.}
}
@inproceedings{BKSS-tacas06,
  address = {Vienna, Austria},
  month = mar,
  year = 2006,
  volume = {3920},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Hermanns, Holger and Palsberg, Jens},
  acronym = {{TACAS}'06},
  booktitle = {{P}roceedings of the 12th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'06)},
  author = {Bollig, Benedikt and Kern, Carsten and 
		 Schl{\"u}tter, Markus and Stolz, Volker},
  title = {{MSC}an: A Tool for Analyzing {MSC} Specifications},
  pages = {455-458},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSCan.ps},
  doi = {10.1007/11691372_32},
  abstract = {We present the tool MSCan, which supports MSC-based 
  system development. In particular, it automatically checks 
  high-level MSC specifications for implementability.}
}
@article{BBM-ipl06,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
                Markey, Nicolas},
  title = {Improved Undecidability Results on Weighted Timed
                 Automata},
  year = 2006,
  month = jun,
  volume = 98,
  number = 5,
  pages = {188-194},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBM06.ps},
  doi = {10.1016/j.ipl.2006.01.012},
  abstract = {In this paper, we improve two recent undecidability
        results of Brihaye, Bruy{\`e}re and Raskin about
        weighted timed automata, an extension of timed automata with a
        cost variable. Our results rely on a new encoding of the two
        counters of a Minsky machine that only require three clocks and 
	one stopwatch cost, while previous reductions required five clocks 
	and one stopwatch cost.}
}
@inproceedings{BBS-lpar06,
  address = {Phnom Penh, Cambodia},
  month = nov,
  year = 2006,
  volume = 4246,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Hermann, Miki and Voronkov, Andrei},
  acronym = {{LPAR}'06},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'06)},
  author = {Baier, Christel and Bertrand, Nathalie and
                   Schnoebelen, {\relax Ph}ilippe},
  title = {On Computing Fixpoints in Well-Structured Regular Model
		Checking, with Applications to Lossy Channel Systems},
  pages = {347-361},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-lpar06.ps},
  doi = {10.1007/11916277_24},
  abstract = {We prove a general finite convergence theorem for
{"}upward-guarded{"} fixpoint expressions over a well-quasi-ordered~set. This
has immediate applications in regular model checking of well-structured
systems, where a main issue is the eventual convergence of fixpoint
computations. In~particular, we are able to directly obtain several new
decidability results on lossy channel systems.}
}
@article{BBS-ipl05,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Baier, Christel and Bertrand, Nathalie and
                   Schnoebelen, {\relax Ph}ilippe},
  title = {A note on the attractor-property of infinite-state {M}arkov chains},
  year = 2006,
  month = jan,
  number = 2,
  volume = 97,
  pages = {58-63},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBS.ps},
  doi = {10.1016/j.ipl.2005.09.011},
  abstract = {In the past five years, a series of verification algorithms
                  has been proposed for infinite Markov chains that have a
                  finite attractor, \emph{i.e.}, a set that will be visited
                  infinitely often almost surely starting from any state. \par
                  In this paper, we establish a sufficient criterion for
                  the existence of an attractor. We show that if the states
                  of a Markov chain can be given levels (positive integers)
                  such that the expected next level for states at some
                  level \(n > 0\) is less than \(n-\Delta\) for some positive
                  \(\Delta\), then the states at level~\(0\) constitute an
                  attractor for the chain. As an application, we obtain a
                  direct proof that some probabilistic channel systems
                  combining message losses with duplication and insertion
                  errors have a finite attractor.}
}
@inproceedings{BG-lpar06,
  address = {Phnom Penh, Cambodia},
  month = nov,
  year = 2006,
  volume = 4246,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Hermann, Miki and Voronkov, Andrei},
  acronym = {{LPAR}'06},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'06)},
  author = {Bozzelli, Laura and Gascon, R{\'e}gis},
  title = {Branching Time Temporal Logic Extended with {P}resburger Constraints},
  pages = {197-211},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BG-LPAR06.ps},
  doi = {10.1007/11916277_14},
  abstract = {Recently, \(\mathrm{LTL}\) extended with atomic formulas built
over a constraint language interpreting variables in~\(\mathbb{Z}\) has been
shown to have a decidable satisfiability and model-checking problem.
This~language allows to compare the variables at different states of the model
and include periodicity constraints, comparison constraints, and a restricted
form of quantification. On the other hand, the \(\mathrm{CTL}\) counterpart of
this logic (and hence also its \(\mathrm{CTL}^{*}\) counterpart which subsumes
both \(\mathrm{LTL}\) and~\(\mathrm{CTL}\)) has an undecidable model-checking
problem. In~this paper, we substantially extend the decidability border, by
considering a meaningful fragment of \(\mathrm{CTL}^{*}\) extended with such
constraints (which subsumes both the universal and existential fragments, as
well as the \(\mathrm{EF}\)-like fragment) and show that satisfiability and
model-checking over relational automata that are abstraction of counter
machines are decidable. The~correctness and the termination of our algorithm
rely on a suitable well quasi-ordering defined over the set of variable
valuations.}
}
@misc{chevalier-prefsttcs06,
  author = {Chevalier, Fabrice},
  title = {Decision procedures for timed logics},
  year = 2006,
  month = dec,
  howpublished = {Invited talk, Advances and Issues in Timed Systems,
                  Kolkata, India}
}
@misc{gastin-prefsttcs06,
  author = {Gastin, Paul},
  title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
  year = 2006,
  month = dec,
  howpublished = {Invited talk, Advances and Issues in Timed Systems,
                  Kolkata, India}
}
@misc{gastin-wata06,
  author = {Gastin, Paul},
  title = {Weigthed logics and weighted automata},
  year = 2006,
  month = mar,
  howpublished = {Invited talk, Workshop Weighted Automata: Theory and Applications,
		Leipzig, Germany}
}
@misc{gastin-epit06,
  author = {Gastin, Paul},
  title = {Distributed synthesis: synchronous and asynchronous semantics},
  year = 2006,
  month = may,
  howpublished = {Invited talk, 34{\`e}me {\'E}cole de Printemps en 
		Informatique Th{\'e}orique, Ile de R{\'e}, France}
}
@misc{gastin-mfps22,
  author = {Gastin, Paul},
  title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
  year = 2006,
  month = may,
  howpublished = {Invited talk, 22nd {C}onference on 
        {M}athematical {F}oundations of {P}rogramming 
        {S}emantics ({MFPS}'06)}
}
@inproceedings{Bouyer-MFPS22,
  address = {Genova, Italy},
  month = may,
  year = 2006,
  volume = 158,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Brookes, Steve and Mislove, Michael},
  acronym = {{MFPS}'06},
  booktitle = {{P}roceedings of the 22nd {C}onference on 
	{M}athematical {F}oundations of {P}rogramming 
	{S}emantics ({MFPS}'06)},
  author = {Bouyer, Patricia},
  title = {Weighted Timed Automata: {M}odel-Checking and Games},
  pages = {3-17},
  note = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bouyer-mfps06.ps},
  doi = {10.1016/j.entcs.2006.04.002},
  abstract = {In this paper, we present weighted\slash priced 
	timed automata, an extension of timed automaton with 
	costs, and solve several interesting problems on that model.}
}
@article{bid-hen-JLAP-2005,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Logic and Algebraic Programming},
  author = {Bidoit, Michel and Hennicker, Rolf},
  title = {Constructor-Based Observational Logic},
  year = {2006},
  month = apr # {-} # may,
  number = {1-2},
  volume = 67,
  pages = {3-51},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
  doi = {10.1016/j.jlap.2005.09.002},
  abstract = {This paper focuses on the integration of reachability and
observability concepts within an algebraic,
institution-based framework. In the first part of this work,  
we develop the essential ingredients that are needed to define the 
constructor-based observational logic institution, called
COL, which takes into account both 
the generation- and observation-oriented aspects of software systems. The 
underlying paradigm of our approach is that the semantics of a specification should be as
loose as possible to capture all its correct realizations. We also consider the {"}black
box{"} semantics of a specification which is useful to study the behavioral properties
a user can observe when he\slash she is experimenting with the system.\par
   In the second part of this work, we develop proof techniques for structured
COL-specifications. For this purpose we introduce an
institution encoding from the COL 
institution to the institution of many-sorted first-order logic with equality
and sort-generation constraints. Using this institution
encoding, we can then reduce proofs of 
consequences of structured specifications built over COL to proofs of consequences
of structured specifications written in a simple subset of the algebraic specification
language {\scshape Casl}. This means, in particular, that any inductive theorem prover, such
as \emph{e.g.} the Larch Prover or PVS, can be used to prove theorems over structured
COL-specifications.}
}
@inproceedings{BH-Goguen06,
  address = {San Diego, California, USA},
  month = jun,
  year = 2006,
  volume = 4060,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Futatsugi, Kokichi and Jouannaud, Jean-Pierre and 
	   Meseguer, Jos{\'e}},
  acronym = {{A}lgebra, {M}eaning and {C}omputation},
  booktitle = {{A}lgebra, {M}eaning and {C}omputation~--- Essays dedicated to 
	   Joseph~A.~Goguen on the Occasion of His 65th~Birthday},
  author = {Bidoit, Michel and Hennicker, Rolf},
  title = {Proving Behavioral Refinements of {COL}-Specifications},
  pages = {333-354},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
  doi = {10.1007/11780274_18},
  abstract = {The COL institution (constructor-based 
	observational logic) has been introduced as a formal 
	framework to specify both generation- and 
	observation-oriented properties of software systems. In 
	this paper we consider behavioral refinement relations 
	between COL-specifications taking into account 
	implementation constructions. We propose a general 
	strategy for proving the correctness of such 
	refinements by reduction to (standard) first-order 
	theorem proving with induction. Technically our 
	strategy relies on appropriate proof rules and on a 
	lifting construction to encode the reachability and 
	observability notions of the COL institution.}
}
@inproceedings{BHR06-acsd,
  address = {Turku, Finland},
  month = jun,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  editor = {Goossens, Kees and Petrucci, Laure},
  acronym = {{ACSD}'06},
  booktitle = {{P}roceedings of the 6th {I}nternational
               {C}onference on {A}pplication of {C}oncurrency
               to {S}ystem {D}esign
               ({ACSD}'06)},
  author = {Bouyer, Patricia and Haddad, Serge and 
                  Reynier, Pierre-Alain},
  title = {Extended Timed Automata and Time {P}etri Nets},
  pages = {91-100},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2006-01.ps},
  doi = {10.1109/ACSD.2006.6},
  abstract = {Timed Automata (TA) and Time Petri Nets (TPN) are two
 well-established formal models for real-time systems. Recently, a
 linear transformation of TA to TPNs preserving reachability
 properties and timed languages has been proposed, which does however
 not extend to larger classes of TA which would allow diagonal
 constraints or more general resets of clocks. Though these features
 do not add expressiveness, they yield exponentially more concise
 models. \par
 In this work, we propose two translations: one from extended TA to
 TPNs whose size is either linear or quadratic in the size of the
 original TA, depending on the features which are allowed; another
 one from a parallel composition of TA to TPNs, which is also linear.
 As a consequence, we get that TPNs are exponentially more concise
 than~TA.}
}
@inproceedings{BHR-ICALP2006,
  address = {Venice, Italy},
  month = jul,
  year = 2006,
  volume = 4052,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
  acronym = {{ICALP}'06},
  booktitle = {{P}roceedings of the 33rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'06)~--- {P}art~{II}},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Timed {P}etri Nets and Timed Automata: On the Discriminating Power of
            {Z}eno Sequences},
  pages = {420-431},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-icalp06.ps},
  doi = {10.1007/11787006_36},
  abstract = {Timed Petri nets and timed 
	automata are two standard models for the 
	analysis of real-time systems. In this 
	paper, we prove that they are incomparable 
	for the timed language equivalence. Thus we 
	propose an extension of timed Petri nets 
	with read-arcs~(RA-TdPN), whose coverability 
	problem is decidable. We also show that this 
	model unifies timed Petri nets and timed 
	automata. Then, we establish numerous 
	expressiveness results and prove that Zeno 
	behaviours discriminate between several 
	sub-classes of RA-TdPNs. This has surprising 
	consequences on timed automata, 
	\emph{e.g.}~on the power of 
	non-deterministic clock resets.}
}
@inproceedings{BHR-atva06,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Timed Unfoldings for Networks of Timed Automata},
  pages = {292-306},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-atva06.ps},
  doi = {10.1007/11901914_23},
  abstract = {Whereas partial order methods have proved their efficiency for
the analysis of discrete-event systems, their application to
timed systems remains a challenging research topic. Here, we
design a verification algorithm for networks of timed automata
with invariants. Based on the unfolding technique, our method
produces a branching process as an acyclic Petri net extended
with read arcs. These arcs verify conditions on tokens without
consuming them, thus expressing concurrency between conditions
checks. They are useful for avoiding the explosion of the size
of the unfolding due to clocks which are compared with constants
but not reset. Furthermore, we attach zones to events, in addition
to markings. We~then compute a complete finite prefix of the
unfolding. The~presence of invariants goes against the concurrency
since it entails a global synchronization on time. The use of read
arcs and the analysis of the clock constraints appearing in
invariants will help increasing the concurrency relation between
events. Finally, the finite prefix we compute can be used to decide
reachability properties, and transition enabling.}
}
@incollection{BL-VAT06,
  author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
  title = {V{\'e}rification par automates temporis{\'e}s},
  booktitle = {Syst{\`e}mes temps-r{\'e}el~1~: techniques de description 
		et de v{\'e}rification},
  editor = {Navet, Nicolas},
  publisher = {Herm{\`e}s},
  year = 2006,
  month = jun,
  pages = {121-150},
  url = {http://www.lavoisier.fr/fr/livres/index.asp?texte=2746213030&select=isbn&from=Hermes},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-VAT06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-VAT06.ps},
  isbn = {2-7462-1303-6}
}
@inproceedings{BMR-latin06,
  address = {Valdivia, Chile},
  month = mar,
  year = 2006,
  volume = 3887,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Correa, Jose R. and Hevia, Alejandro and Kiwi, Marcos},
  acronym = {{LATIN}'06},
  booktitle = {{P}roceedings of the 7th {L}atin {A}merican
               {S}ymposium on {T}heoretical {I}nformatics
               ({LATIN}'06)},
  author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain},
  title = {Robust Model-Checking of Linear-Time Properties in Timed Automata},
  pages = {238-249},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-latin06.ps},
  doi = {10.1007/11682462_25},
  abstract = {Formal verification of timed systems 
	is well understood, but their 
	\emph{implementation} is still challenging. Recent 
	works by Raskin \emph{et al.} have brought out a 
	model of parameterized timed automata that can be 
	used to prove \emph{implementability} of timed 
	systems for safety properties. We define here a 
	more general notion of robust model-checking for 
	linear-time properties, which consists in 
	verifying whether a property still holds even if 
	the transitions are slightly delayed or expedited. 
	We provide PSPACE algorithms for the robust 
	model-checking of B{\"u}chi-like and LTL 
	properties. We also verify bounded-response-time 
	properties. }
}
@book{Bollig06,
  author = {Bollig, Benedikt},
  title = {Formal Models of Communicating Systems~--- Languages, Automata, 
		and Monadic Second-Order Logic},
  year = {2006},
  month = jun,
  publisher = {Springer},
  isbn = {3-540-32922-6},
  otherurl = {http://www.springer.com/978-3-540-32922-6},
  url = {http://www.lsv.ens-cachan.fr/~bollig/fmcs/},
  abstract = {This book studies the relationship between automata and 
monadic second-order logic, focusing on classes of automata that 
describe the concurrent behavior of distributed systems.\par
It provides a unifying theory of communicating automata and their 
logical properties. Based on Hanf's Theorem and Thomas's graph 
acceptors, it develops a result that allows us to characterize many 
popular models of distributed computation in terms of the existential 
fragment of monadic second-order logic. In particular, the book covers 
finite automata, asynchronous (cellular) automata, communicating 
finite-state machines, and lossy channel systems. Model behavior is 
described using graphs and partial orders, leading to the notions of 
Mazurkiewicz traces, message sequence charts, and live sequence 
charts.\par
This book is suitable for senior undergraduate and graduate courses on 
advanced automata theory, concurrency and communication issues. It can 
also be used as a reference by researchers concerned with the formal 
modeling of concurrent systems. Some knowledge of automata theory is a 
prerequisite. Numerous exercises, chapter summaries, and suggested 
reading allow for self-study, while the book is supported with a website 
containing course material and solutions.}
}
@inproceedings{BS05-express,
  address = {San Francisco, California, USA},
  month = jul,
  year = 2006,
  number = 3,
  volume = 154,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Baeten, Jos and Phillips, Iain},
  acronym = {{EXPRESS}'05},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {W}orkshop on {E}xpressiveness in
               {C}oncurrency
               ({EXPRESS}'05)},
  author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
  title = {A short visit to the {STS} hierarchy},
  pages = {59-69},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BS05-express.ps},
  doi = {10.1016/j.entcs.2006.05.007},
  abstract = {The hierarchy of Symbolic 
	Transition Systems, introduced by Henzinger,
	Majumdar and Raskin, is an elegant 
	classification  
	tool for some families of infinite-state
	operational models that support some variants of 
	a symbolic {"}backward closure{"}
	verification algorithm. It was first used and 
	illustrated with families of hybrid 
	systems.\par 
	  In this paper we investigate whether the STS 
	hierarchy can account for classical
	families of infinite-state systems outside of 
	timed or hybrid systems.}
}
@inproceedings{TED-hldvt06,
  address = {Monterey, California, USA},
  month = nov,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{HLDVT}'06},
  booktitle = {{P}roceedings of the {IEEE} {H}igh {L}evel {D}esign 
		 {V}erification and {T}est Workshop ({HLDVT}'06)},
  author = {Taktak, Sami and Encrenaz, Emmanuelle and Desbarbieux, Jean-Lou},
  title = {A Tool for Automatic Detection of Deadlock in Wormhole Networks
	on Chip},
  pages = {203-210},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf},
  doi = {10.1109/HLDVT.2006.319992},
  abstract = {We present an extension of Duato's necessary and
sufficient condition a routing function must satisfy in order to
be deadlock-free, to support environment constraints inducing
extra-dependencies between messages. We also present an original
algorithm to automatically check the deadlock-freeness of a
network with a given routing function. A~prototype tool has
been developed and automatic deadlock checking of large scale
networks with various routing functions have been successfully
achieved.}
}
@inproceedings{BE-rsp06,
  address = {Chania, Crete},
  month = jun,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{RSP}'06},
  booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop
           on {R}apid {S}ystem {P}rototyping ({RSP}'06)},
  author = {Braunstein, C{\'e}cile and Encrenaz, Emmanuelle},
  title = {Formalizing the incremental design and verification process of
		a pipelined protocol converter},
  pages = {103-109},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BE-rsp06.ps},
  doi = {10.1109/RSP.2006.19},
  abstract = {This work studies the relations between pipeline 
	architectures and their specification expressed in~CTL. We 
	propose a method to build pipeline structures incrementally
	from a simple one (already verified) to a more complex one.
	Moreover, we show how each increment can be integrated
	in a CTL specification. We define increments to model 
	treatment delay and treatment abortion of a pipeline flow, and
	we formalize the composition of the different increments. In
	order to represent the increments added to an architecture,
	we derive a set of CTL formulae transformations. Finally
	we model a control flow of a protocol converter by 
	composition of these increments. We show how CTL properties
	of the complex architecture are built by applying automatic
	transformations on the set of CTL properties of the simplest
	architecture.}
}
@inproceedings{GSZ-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
  title = {Distributed synthesis for well-connected architectures},
  pages = {321-332},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
  doi = {10.1007/11944836_30},
  abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates input
and output variables. We~introduce the subclass of uniformly
well-connected~(UWC) architectures for which there exists a routing allowing
each output process to get the values of all inputs it is connected to, as
soon as possible. We~prove that the distributed synthesis problem is decidable
on UWC architectures if and only if the set of all sets of input variables
visible by output variables is totally ordered, under set inclusion. We~also
show that if we extend this class by letting the routing depend on the output
process, then the previous decidability result fails. Finally, we provide a
natural restriction on specifications under which the whole class of~UWC
architectures is decidable.}
}
@proceedings{AB-lncs4202,
  title = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4202,
  year = 2006,
  month = sep,
  address = {Paris, France},
  isbn = {3-540-45026-2},
  url = {http://www.springer.com/978-3-540-45026-2},
  doi = {10.1007/11867340}
}
@inproceedings{BGP1-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
  title = {Refinements and abstractions of signal-event (timed) languages},
  pages = {67-81},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP1-formats06.ps},
  doi = {10.1007/11867340_6},
  abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they describe
a change in the specification level, from an abstract view to a more concrete
one, or conversely. For~timed systems, there is up to now no uniform notion of
substitutions. In~this paper, we study the timed substitutions in the general
framework of signal-event languages, where both signals and events are taken
into account. We~prove that regular signal-event languages are closed under
substitutions and inverse substitutions. }
}
@inproceedings{BGP2-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
  title = {Intersection of regular signal-event (timed) languages},
  pages = {52-66},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP2-formats06.ps},
  doi = {10.1007/11867340_5},
  abstract = {We propose in this paper a construction for a {"}well known{"}
result: regular signal-event languages are closed by intersection. In~fact,
while this result is indeed trivial for languages defined by Alur and Dill's
timed automata (the proof is an immediate extension of the one in the untimed
case), it turns out that the construction is much more tricky when considering
the most involved model of signal-event automata. While several constructions
have been proposed in particular cases, it is the first time, up to our
knowledge, that a construction working on finite and infinite signal-event
words and taking into account signal stuttering, unobservability of
zero-duration \(\tau\)-signals and Zeno runs is proposed.}
}
@inproceedings{CDP-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Chevalier, Fabrice and D'Souza, Deepak and Prabhakar, Pavithra},
  title = {On continuous timed automata with input-determined guards},
  pages = {369-380},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDP-fsttcs06.ps},
  doi = {10.1007/11944836_34},
  abstract = {We consider a general class of timed automata parameterized by a
  set of {"}input-determined{"} operators, in a continuous time setting. We show
  that for any such set of operators, we have a monadic second order logic
  characterization of the class of timed languages accepted by the corresponding
  class of automata. Further, we consider natural timed temporal logics based on
  these operators, and show that they are expressively equivalent to the
  first-order fragment of the corresponding MSO logics. As~a~corollary of these
  general results we obtain an expressive completeness result for the continuous
  version of MTL.}
}
@inproceedings{CKKW-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Cortier, V{\'e}ronique and Kremer, Steve and 
		 K{\"u}sters, Ralf and Warinschi, Bogdan},
  title = {Computationally Sound Symbolic Secrecy in the Presence of Hash Functions},
  pages = {176-187},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CKKW-fsttcs06.ps},
  doi = {10.1007/11944836_18},
  abstract = {The standard symbolic, deducibility-based notions of secrecy are
in general insufficient from a cryptographic point of view, especially in
presence of hash functions. In~this paper we devise and motivate a more
appropriate secrecy criterion which exactly captures a standard cryptographic
notion of secrecy for protocols involving public-key enryption and hash
functions: protocols that satisfy it are computationally secure while any
violation of our criterion directly leads to an attack. Furthermore, we prove
that our criterion is decidable via an NP decision procedure. Our~results hold
for standard security notions for encryption and hash functions modeled as
random oracles.}
}
@article{CDL05-survey,
  publisher = {{IOS} Press},
  journal = {Journal of Computer Security},
  author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie
                 and Lafourcade, Pascal},
  title = {A Survey of Algebraic Properties Used in Cryptographic
                 Protocols},
  year = {2006},
  volume = 14,
  number = 1,
  pages = {1-43},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/surveyCDL.ps},
  abstract = {Cryptographic protocols are 
	successfully analyzed using formal methods. 
	However, formal approaches usually consider the 
	encryption schemes as black boxes and assume that 
	an adversary cannot learn anything from an 
	encrypted message except if he has the key. Such an 
	assumption is too strong in general since some 
	attacks exploit in a clever way the interaction 
	between protocol rules and properties of 
	cryptographic operators. Moreover, the executability of some 
	protocols relies explicitly on some algebraic 
	properties of cryptographic primitives such as 
	commutative encryption. We give a list of some 
	relevant algebraic properties of cryptographic 
	operators, and for each of them, we provide 
	examples of protocols or attacks using these 
	properties. We also give an overview of the 
	existing methods in formal approaches for analyzing 
	cryptographic protocols.}
}
@inproceedings{CEFX-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
		  Fribourg, Laurent and Xu, Weiwen},
  title = {Verification of the Generic Architecture of a Memory Circuit Using 
		  Parametric Timed Automata},
  pages = {113-127},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-formats06.ps},
  econtrat = {MEDEA+ Blueberries},
  doi = {10.1007/11867340_9},
  abstract = {Using a variant of Clariso-Cortadella's parametric method
for verifying asynchronous circuits, we formally derive a set of linear
constraints that ensure the correctness of some crucial timing behaviours
of the architecture of SPSMALL memory. This allows us to check two
different implementations of this architecture.}
}
@article{CEFX-wseas06,
  publisher = {World Scientific and Engineering Academy and Society},
  journal = {WSEAS Transactions on Circuits and Systems},
  author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
		  Fribourg, Laurent and Xu, Weiwen},
  title = {Timing analysis of an embedded memory: {SPSMALL}},
  pages = {973-978},
  volume = 5,
  number = 7,
  year = 2006,
  month = jul,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
  abstract = {This paper proposes a high-level formalism, called
    Abstract Functional and Timing Graph~(AFTG), for describing a memory
    architecture, which combines logical functionality and timing. After
    translation of the~AFTG into the form a timed automaton, we are able to
    compute the response times of the modeled memory, and check their consistency
    with the values specified in the datasheet. We also address the problem of
    finding optimal values of setup timings.}
}
@inproceedings{DDFG-atva06,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Demri, St{\'e}phane and Finkel, Alain
		and Goranko, Valentin and van Drimmelen, Govert},
  title = {Towards a model-checker for counter systems},
  pages = {493-507},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
  doi = {10.1007/11901914_36},
  abstract = {This paper deals with model-checking of fragments and extensions
of~\(\mathrm{CTL}^{*}\) on infinite-state Presburger counter systems, where
the states are vectors of integers and the transitions are determined by means
of relations definable within Presburger arithmetic. We have identified a
natural class of admissible counter systems~(ACS) for which we show that the
quantification over paths in~\(\mathrm{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing translation
of the whole Presburger-\(\mathrm{CTL}^{*}\) into Presburger arithmetic,
thereby enabling effective model checking. We have provided evidence that our
results are close to optimal with respect to the class of counter systems
described above. Finally, we design a complete semi-algorithm to verify
first-order~\(\mathrm{LTL}\) properties over trace-flattable counter systems,
extending the previous underlying FAST semi-algorithm to verify reachability
questions over flattable counter systems. }
}
@inproceedings{DL-lics2006,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'06},
  booktitle = {{P}roceedings of the 21st
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'06)},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
  title = {{LTL} with the freeze quantifier and register automata},
  pages = {17-26},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
  doi = {10.1109/LICS.2006.31},
  abstract = {Temporal logics, first-order logics, and automata over data
words have recently attracted considerable attention. A~data word is a word
over a finite alphabet, together with a datum (an element of an infinite
domain) at each position. Examples include timed words and XML documents. To
refer to the data, temporal logics are extended with the freeze quantifier,
first-order logics with predicates over the data domain, and automata with
registers or pebbles.\par
    We investigate relative expressiveness and complexity of standard decision
problems for~\(\mathrm{LTL}\) with the freeze
quantifier~(\(\mathrm{LTL}^{\downarrow}\)), 2-variable first-order logic
(\(\mathrm{FO}^{2}\)) over data words, and register automata. The only
predicate available on data is equality. Previously undiscovered connections
among those formalisms, and to counter automata with in- crementing errors,
enable us to answer several questions left open in recent literature.\par
    We show that the future-time fragment of~\(\mathrm{LTL}^{\downarrow}\)
which corresponds to \(\mathrm{FO}^{2}\) over finite data words can be
extended considerably while preserving decidability, but at the expense of
non-primitive recursive complexity, and that most of further extensions are
undecidable. We also prove that surprisingly, over infinite data words,
\(\mathrm{LTL}^{\downarrow}\) without the `until' operator, as well as
nonemptiness of one-way universal register automata, are undecidable even when
there is only one register.}
}
@inproceedings{DL-ijcar06,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  volume = 4130,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  editor = {Furbach, Ulrich and Shankar, Natarajan},
  acronym = {{IJCAR}'06},
  booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint
           {C}onference on {A}utomated {R}easoning
           ({IJCAR}'06)},
  author = {Demri, St{\'e}phane and Lugiez, Denis},
  title = {{P}resburger Modal Logic is Only {PSPACE}-complete},
  pages = {541-556},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-25.pdf},
  doi = {10.1007/11814771_44},
  abstract = {We introduce a Presburger modal logic PML with regularity
constraints and full Presburger constraints on the number of children that
generalize graded modalities, also known as number restrictions in description
logics. We~show that PML satisfiability is only PSPACE-complete by designing a
Ladner-like algorithm that can be turned into an analytic proof system 
algorithm. This extends a well-known and non-trivial PSPACE upper bound for
graded modal logic. Furthermore, we provide a detailed comparison with logics
that contain Presburger constraints and that are dedicated to query XML
documents. As~an application, we show that satisfiability for Sheaves Logic SL
is PSPACE-complete, improving significantly its best known upper bound.}
}
@article{delaune-tcs06,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Delaune, St{\'e}phanie},
  title = {An Undecidability Result for~{\textsf{\MakeUppercase{AG}h}}},
  volume = 368,
  number = {1-2},
  pages = {161-167},
  year = 2006,
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/delaune-tcs06.ps},
  doi = {10.1016/j.tcs.2006.08.018},
  abstract = {We present an undecidability result for 
	the verification of security protocols. Since the 
	\emph{perfect cryptography assumption} is unrealistic 
	for cryptographic primitives with visible algebraic 
	properties, several recent works relax this assumption, 
	allowing the intruder to exploit these properties. We 
	are interested in the \emph{Abelian groups} theory in 
	combination with the homomorphism axiom. We show that 
	satisfaisability of symbolic deducibility constraints 
	is undecidable, obtaining in this way the first 
	undecidability result concerning a theory for which 
	unification is known to be decidable~[F.~Baader, Unification 
        in commutative theories, Hilbert's basis theorem, and 
        Gr{\"{o}}bner 
        bases, J.~ACM~40(3) (1993)~477-503].}
}
@inproceedings{DKR-wote06,
  address = {Cambridge, UK},
  month = jun,
  year = 2006,
  acronym = {{WOTE}'06},
  booktitle = {{P}roceedings of the {IAVoSS} {W}orkshop {O}n {T}rustworthy {E}lections
               ({WOTE}'06)},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and 
		 Ryan, Mark D.},
  title = {Verifying Properties of Electronic Voting Protocols},
  pages = {45-52},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-wote06.ps},
  abstract = {In this paper we report on some recent work to formally specify
and verify electronic voting protocols. In particular, we use the formalism of
the applied pi calculus: the applied pi calculus is a formal language
similar to the pi calculus but with useful extensions for modelling
cryptographic protocols. We model several important properties, namely
fairness, eligibility, privacy, receipt-freeness and coercion-resistance.
Verification of these properties is illustrated on two cases studies and has
been partially automated using the Blanchet's ProVerif tool.}
}
@inproceedings{DKR-csfw06,
  address = {Venice, Italy},
  month = jul,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{CSFW}'06},
  booktitle = {{P}roceedings of the 
               19th {IEEE} {C}omputer {S}ecurity {F}oundations
               {W}orkshop ({CSFW}'06)},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and 
		 Ryan, Mark D.},
  title = {Coercion-Resistance and Receipt-Freeness in
		Electronic Voting},
  pages = {28-39},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-csfw06.ps},
  doi = {10.1109/CSFW.2006.8},
  abstract = {In this paper we formally study 
	important properties of electronic voting protocols. 
	In particular we are interested in 
	coercion-resistance and receipt-freeness. 
	Intuitively, an election protocol is 
	coercion-resistant if a voter \(A\) cannot prove to a 
	potential coercer~\(C\) that she voted in a particular 
	way.  We assume that \(A\) cooperates with~\(C\) in an 
	interactive way. Receipt-freeness is a weaker 
	property, for which we assume that \(A\) and~\(C\) 
	cannot interact during the protocol, but \(A\) later 
	provides evidence (the receipt) of how she voted. 
	While receipt-freeness can be expressed using 
	observational equivalence from the applied pi 
	calculus, we need to introduce a new relation to 
	capture coercion-resistance. Our formalization of 
	coercion-resistance and receipt-freeness are quite 
	different. Nevertheless, we show in accordance with 
	intuition that coercion-resistance implies 
	receipt-freeness, which implies privacy, the basic 
	anonymity property of voting protocols, as defined 
	in previous work. Finally we illustrate the 
	definitions on a simplified version of the 
	Lee~\emph{et~al.}\ voting protocol.}
}
@inproceedings{DLLT-ICALP2006,
  address = {Venice, Italy},
  month = jul,
  year = 2006,
  volume = 4052,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
  acronym = {{ICALP}'06},
  booktitle = {{P}roceedings of the 33rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'06)~--- {P}art~{II}},
  author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and 
		Lugiez, Denis and Treinen, Ralf},
  title = {Symbolic Protocol Analysis in Presence of a Homomorphism 
		Operator and {\emph{Exclusive~Or}}},
  pages = {132-143},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLLT-icalp06.ps},
  doi = {10.1007/11787006_12},
  abstract = {Security of a cryptographic 
	protocol for a bounded number of sessions is 
	usually expressed as a symbolic trace 
	reachability problem. We show that symbolic 
	trace reachability for well-defined protocols 
	is decidable in presence of the exclusive or 
	theory in combination with the homomorphism 
	axiom. These theories allow us to model basic 
	properties of important cryptographic 
	operators. This trace reachability problem 
	can be expressed as a system of symbolic 
	deducibility constraints for a certain 
	inference system describing the capabilities 
	of the attacker. One main step of our proof 
	consists in reducing deducibility constraints 
	to constraints for deducibility in one step 
	of the inference system. This constraint 
	system, in turn, can be expressed as a system 
	of quadratic equations of a particular form 
	over \(\mathbb{Z}/2\mathbb{Z}[h]\), the ring 
	of polynomials in one indeterminate over the 
	finite field \(\mathbb{Z}/2\mathbb{Z}\). We 
	show that satisfiability of such systems is 
	decidable. }
}
@proceedings{CK-fcc2006,
  editor = {Cortier, V{\'e}ronique and Kremer, Steve},
  booktitle = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and
		 {C}omputational {C}ryptography ({FCC}'06)},
  title = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and
		 {C}omputational {C}ryptography ({FCC}'06)},
  address = {Venice, Italy},
  year = 2006,
  month = jul,
  url = {http://hal.inria.fr/FCC2006/}
}
@article{CKS-jar2005,
  publisher = {Springer},
  journal = {Journal of Automated Reasoning},
  author = {Chadha, Rohit and Kremer, Steve and Scedrov, Andre},
  title = {Formal Analysis of Multi-Party Contract Signing},
  volume = 36,
  number = {1-2},
  pages = {39-83},
  year = 2006,
  month = jan,
  nmnote = {Special Issue on Automated Reasoning for Security Protocol Analysis},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf},
  doi = {10.1007/s10817-005-9019-5},
  abstract = {We analyze the multi-party contract-signing protocols
   of Garay and MacKenzie (GM) and of Baum and Waidner
   (BW). We use a finite-state tool, {\scshape Mocha},
   which allows specification of protocol properties in
   a branching-time temporal logic with game semantics.
   While our analysis does not reveal any errors in the
   BW protocol, in the GM protocol we discover serious
   problems with fairness for four signers and an
   oversight regarding abuse-freeness for three signers.
   We propose a complete revision of the GM subprotocols
   in order to restore fairness.}
}
@article{dj-jar05,
  publisher = {Springer},
  journal = {Journal of Automated Reasoning},
  author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
  title = {Decision Procedures for the Security of
		Protocols with Probabilistic Encryption against 
		Offline Dictionary Attacks},
  volume = 36,
  number = {1-2},
  year = 2006,
  month = jan,
  pages = {85-124},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps},
  doi = {10.1007/s10817-005-9017-7},
  abstract = {We consider the problem of formal 
	automatic verification of cryptographic protocols 
	when some data, like poorly chosen passwords, can 
	be guessed by dictionary attacks. First, we define 
	a theory of these attacks and propose an inference 
	system modeling the deduction capabilities of an 
	intruder. This system extends a set of well 
	studied deduction rules for symmetric and public 
	key encryption often called Dolev-Yao rules with 
	the introduction of a probabilistic encryption 
	operator and guessing abilities for the intruder. 
	Then, we show that the intruder deduction problem 
	in this extended model is decidable in~PTIME. The 
	proof is based on a locality lemma for our 
	inference system. This first result yields to an 
	NP decision procedure for the protocol insecurity 
	problem in presence of a passive intruder. In the 
	active case, the same problem is proved to be 
	NP-complete: we give a procedure for 
	simultaneously solving symbolic constraints with 
	variables which represent intruder deductions. We 
	illustrate the procedure with examples of 
	published protocols and compare our model to other 
	recent formal definitions of dictionary attacks.}
}
@article{SD-ipl05,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Delaune, St{\'e}phanie},
  title = {Easy Intruder Deduction Problems with Homomorphisms},
  volume = 97,
  number = 6,
  pages = {213-218},
  month = mar,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SD-ipl05.ps},
  doi = {10.1016/j.ipl.2005.11.008},
  abstract = {We present complexity results for 
	the verification of security protocols. Since 
	the perfect cryptography assumption is 
	unrealistic for cryptographic primitives with 
	visible algebraic properties, we extend the 
	classical \emph{Dolev-Yao} model by permitting 
	the intruder to exploit these properties. More 
	precisely, we are interested in theories such 
	as \emph{Exclusive or} and \emph{Abelian 
	groups} in combination with the homomorphism 
	axiom. We show that the intruder deduction 
	problem is in PTIME in both cases, improving 
	the EXPTIME complexity results presented 
	in~(Lafourcade, Lugiez, Treinen,~2005).}
}
@article{Demri06,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane},
  title = {{LTL} over integer periodicity constraints},
  year = {2006},
  volume = 360,
  number = {1-3},
  pages = {96-123},
  month = aug,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
  doi = {10.1016/j.tcs.2006.02.019},
  abstract = {Periodicity constraints are used 
	in many logical formalisms, in fragments of Presburger~LTL, 
	in calendar logics, and in  logics for access 
	control, to quote a few examples. In the paper, we 
	introduce the logic PLTL\(^{\mathrm{mod}}\), an 
	extension of Linear-Time Temporal Logic LTL with 
	past-time operators whose atomic formulae are defined 
	from a first-order constraint language dealing with 
	periodicity. Although the underlying constraint language 
	is a fragment of Presburger arithmetic shown to admit a 
	{\scshape pspace}-complete satisfiability problem, we establish 
	that PLTL\(^{\mathrm{mod}}\) model-checking and 
	satisfiability problems remain in {\scshape pspace} as plain~LTL 
	(full Presburger LTL is known to be highly undecidable). 
	This is particularly interesting for dealing with 
	periodicity constraints since the language of 
	PLTL\(^{\mathrm{mod}}\) has a language more concise than 
	existing languages and the temporalization of our 
	first-order language of periodicity constraints has the 
	same worst case complexity as the underlying constraint 
	language. Finally, we show examples of introduction the 
	quantification in the logical language that provide to 
	PLTL\(^{\mathrm{mod}}\), {\scshape expspace}-complete 
	problems. As another application, we establish that the 
	equivalence problem for extended single-string automata, 
	known to express the equality of time granularities, is 
	{\scshape pspace}-complete by designing a reduction from~QBF and by 
	using our results for PLTL\(^{\mathrm{mod}}\). }
}
@article{DLS-jcss-param,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Demri, St{\'e}phane and Laroussinie, Fran{\c{c}}ois
        and Schnoebelen, {\relax Ph}ilippe},
  title = {A Parametric Analysis of the State Explosion Problem in
		Model Checking},
  year = 2006,
  month = jun,
  volume = 72,
  number = 4,
  pages = {547-575},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-jcss-param.ps},
  doi = {10.1016/j.jcss.2005.11.003},
  abstract = {In model checking, the 
	state-explosion problem occurs when one checks a 
	non-flat system, \emph{i.e.}, a system implicitly 
	described as a synchronized product of elementary 
	subsystems. In this paper, we investigate the 
	complexity of a wide variety of model checking 
	problems for non-flat systems under the light of 
	parameterized complexity, taking the number of 
	synchronized components as a parameter.  We provide 
	precise complexity measures (in the parameterized 
	sense) for most of the problems we investigate, and 
	evidence that the results are robust.}
}
@article{FGRV-tcs05,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
                 Van{~}Begin, Laurent},
  title = {On the \(\omega\)-Language Expressive Power of Extended
                 {P}etri Nets},
  year = 2006,
  month = may,
  volume = 356,
  number = 3,
  pages = {374-386},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
  doi = {10.1016/j.tcs.2006.02.008},
  abstract = {In this paper, we study the expressive power of several
monotonic extensions of Petri
nets. We compare the expressive power of Petri nets, Petri nets extended 
with \emph{non-blocking arcs} and Petri nets extended with \emph{transfer arcs}, 
in terms of \(\omega\)-languages.
We show that the hierarchy of expressive powers of those models is strict. To prove
these results, we propose \emph{original techniques} that rely on 
well-quasi orderings and monotonicity properties.}
}
@article{FMP-dc05,
  publisher = {Springer},
  journal = {Distributed Computing},
  author = {Fribourg, Laurent and Messika, St{\'e}phane and 
                  Picaronny, Claudine},
  title = {Coupling and Self-Stabilization},
  year = 2006,
  month = feb,
  volume = 18,
  number = 3,
  pages = {221-232},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/dcmessika.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
  doi = {10.1007/s00446-005-0142-7},
  abstract = {A randomized self-stabilizing algorithm~\(\mathcal{A}\)
is an algorithm that, whatever the initial configuration
is, reaches a set~\(\mathcal{L}\) of \emph{legal configurations} in finite time
with probability~1. The proof of convergence towards~\(\mathcal{L}\)
is generally done by exhibiting a potential function~\(\varphi\),
which measures the {"}vertical{"} distance of any configuration 
to~\(\mathcal{L}\), such that \(\varphi\) decreases with non-null probability
at each step of~\(\mathcal{A}\). We propose here a method, based on
the notion of coupling, which makes use of a {"}horizontal{"}
distance~\(\delta\) between any pair of configurations, such that \(\delta\)
decreases in expectation at each step of~\(\mathcal{A}\). In contrast
with classical methods, our coupling method does not
require the knowledge of~\(\mathcal{L}\). In addition to the proof of
convergence, the method allows us to assess the convergence 
rate according to two different measures. Proofs
produced by the method are often simpler or give better
upper bounds than their classical counterparts, as 
examplified here on Herman's mutual exclusion and Iterated 
Prisoner's Dilemma algorithms in the case of cyclic
graphs.}
}
@inproceedings{BGM-atva2006,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan},
  title = {A fresh look at testing for asynchronous communication},
  pages = {369-383},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGM-atva06.ps},
  doi = {10.1007/11901914_28},
  abstract = {Testing is one of the fundamental techniques for verifying if a
computing system conforms to its specification. We~take a fresh look at the
theory of testing for message-passing systems based on a natural notion of
observability in terms of input-output relations. We~propose two notions of
test equivalence: one which corresponds to presenting all test inputs up front
and the other which corresponds to interactively feeding inputs to the system
under test. We compare our notions with those studied earlier, notably the
equivalence proposed by Tretmans. In~Tretmans' framework, asynchrony is
modelled using synchronous communication by augmenting the state space of the
system with queues. We~show that the first equivalence we consider is strictly
weaker than Tretmans' equivalence and undecidable, whereas the second notion
is incomparable. We~also establish (un)decidability results for these
equivalences.}
}
@article{DG-icomp2006,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Pure future local temporal logics are expressively complete for 
                   {M}azurkiewicz traces},
  pages = {1597-1619},
  year = 2006,
  month = nov,
  volume = 204,
  number = 11,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
  doi = {10.1016/j.ic.2006.07.002},
  abstract = {The paper settles a long standing problem for Mazurkiewicz
traces: the pure future local temporal logic defined with the basic modalities
exists-next and until is expressively complete. This means every first-order
definable language of Mazurkiewicz traces can be defined in a pure future
local temporal logic. The~analogous result with a global interpretation has
been known, but the treatment of a local interpretation turned out to be much
more involved. Local logics are interesting because both the satisfiability
problem and the model checking problem are solvable in PSPACE for these logics
whereas they are non-elementary for global logics. Both, the (previously
known) global and the (new) local results generalize Kamp's Theorem for words,
because for sequences local and global viewpoints coincide. }
}
@article{DG06-TCS,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Diekert, Volker and Gastin, Paul},
  title = {From local to global temporal logics over {M}azurkiewicz traces},
  year = 2006,
  month = may,
  volume = 356,
  number = {1-2},
  pages = {126-135},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
  doi = {10.1016/j.tcs.2006.01.035},
  abstract = {We review some results on global and local temporal logic on
Mazurkiewicz traces. Our~main contribution is to show how to derive the
expressive completeness of global temporal logic with respect to first-order
logic [V.~Diekert, P.~Gastin, LTL~is expressively complete for Mazurkiewicz
traces, J.~Comput. System Sci.~64 (2002) 396-418] from the similar result on
local temporal logic [V.~Diekert, P.~Gastin, Pure future local temporal logics
are expressively complete for Mazurkiewicz traces, in: M.~Farach-Colton~(Ed.),
Proc.~LATIN'04, Lecture Notes in Computer Science, Vol.~2976, Springer,
Berlin, 2004, pp.~232-241, Full version available as Research Report
LSV-05-22, Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France].}
}
@inproceedings{JRV-ijcar06,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  volume = 4130,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  editor = {Furbach, Ulrich and Shankar, Natarajan},
  acronym = {{IJCAR}'06},
  booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint
           {C}onference on {A}utomated {R}easoning
           ({IJCAR}'06)},
  author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l
            and Vigneron, Laurent},
  title = {Tree automata with equality constraints modulo equational
                theories},
  pages = {557-571},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-07.pdf},
  doi = {10.1007/11814771_45},
  abstract = {This paper presents new classes
        of tree automata combining automata with
        equality test and automata modulo equational
        theories. We believe that this class has a
        good potential for application in
        \emph{e.g.}~software verification. These tree
        automata are obtained by extending the
        standard Horn clause representations with
        equational conditions and rewrite systems.
        We show in particular that a generalized
        membership problem (extending the emptiness
        problem) is decidable by proving that the
        saturation of tree automata presentations
        with suitable paramodulation strategies
        terminates. Alternatively our results can be
        viewed as new decidable classes of
        first-order formula.}
}
@misc{markey-SynthVerif06,
  author = {Markey, Nicolas},
  title = {Verification of Multi-Agent Systems with~{ATL}},
  year = 2006,
  month = oct,
  howpublished = {Invited talk, FNRS meeting on {"}Synthesis and 
	Verification{"}}
}
@article{KucSch-TCS,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Ku{\v c}era, Anton{\'\i}n and 
         	  Schnoebelen, {\relax Ph}ilippe},
  title = {A General Approach to Comparing Infinite-State Systems
                   with Their Finite-State Specifications},
  number = {2-3},
  volume = {358},
  pages = {315-333},
  month = aug,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KucSch-TCS.ps},
  doi = {10.1016/j.tcs.2006.01.021},
  abstract = {We introduce a generic family of 
	behavioral relations for which the regular 
	equivalence problem (\emph{i.e.}, comparing an arbitrary 
	transition system to some finite-state 
	specification) can be reduced to the model 
	checking problem against simple modal formulae. 
	As an application, we derive decidability of 
	several regular equivalence problems for 
	well-known families of infinite-state systems. }
}
@inproceedings{LLT-unif2006,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  editor = {Levy, Jordi},
  acronym = {{UNIF}'06},
  booktitle = {{P}roceedings of the 20th {I}nternational
               {W}orkshop on {U}nification
               ({UNIF}'06)},
  author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
  title = {{ACUNh}: Unification and Disunification Using Automata Theory},
  pages = {6-20},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LLT-unif06.ps},
  abstract = {We show several results about unification problems in the
equational theory~ACUNh consisting of the theory of exclusive or with one
homomorphism. These results are shown using only techniques of automata and
combinations of unification problems. We~show how to construct a most-general
unifier for ACUNh-unification problems with constants using automata. We also
prove that the first-order theory of ground terms modulo~ACUNh is decidable if
the signature does not contain free non-constant function symbols, and that
the existential fragment is decidable in the general case. Furthermore, we
show a technical result about the set of most-general unifiers obtained for
general unification problems.}
}
@inproceedings{BJ-unif2006,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  editor = {Levy, Jordi},
  acronym = {{UNIF}'06},
  booktitle = {{P}roceedings of the 20th {I}nternational
               {W}orkshop on {U}nification
               ({UNIF}'06)},
  author = {Bouhoula, Adel and Jacquemard, Florent},
  title = {Automating Sufficient Completeness Check for Conditional 
                and Constrained~{TRS}},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf},
  abstract = {We present a procedure for checking sufficient completeness for
conditional and constrained term rewriting systems containing axioms for
constructors which may be constrained (by~e.g.~equalities, disequalities,
ordering, membership...). Such axioms allow to specify complex data structures
like e.g.~sets, sorted lists or powerlists. Our approach is integrated in a
framework for inductive theorem proving based on tree grammars with
constraints, a formalism which permits an exact representation of languages of
ground constructor terms in normal form. The key technique used in the
procedure is a generalized form of narrowing where, given a term, instead of
unifying it with left members of rewrite rules, we instantiate it, at selected
variables, following the productions of a constrained tree grammar, and test
whether it can be rewritten. Our~procedure is sound and complete and has been
successfully applied to several examples, yielding very natural proofs and, in
case of negative answer, a counter example suggesting how to complete the
specification. Moreover, it is a decision procedure when the TRS is
unconditional but constrained, for a large class of constrained constructor
axioms.}
}
@inproceedings{LMO-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
                 Oreiby, Ghassan},
  title = {Model Checking Timed {ATL} for Durational Concurrent
	         Game Structures},
  pages = {245-259},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMO-formats06.ps},
  doi = {10.1007/11867340_18},
  abstract = {We extend the framework of ATL model-checking to {"}simply
	timed{"} concurrent game structures, i.e., multi-agent structures where
	each transition carry an integral duration (or interval thereof). While
	the case of single durations is easily handled from the semantics point of
	view, intervals of durations raise several interesting questions. Moreover
	subtle algorithmic problems have to be handled when dealing with model
	checking. We propose a semantics for which we develop efficient (PTIME)
	algorithms for timed ATL without equality constraints, while the general
	case is shown to be EXPTIME-complete.}
}
@article{LMS-tcs05,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas
		 and Schnoebelen, {\relax Ph}ilippe},
  title = {Efficient Timed Model Checking for Discrete-Time 
		Systems},
  volume = 353,
  number = {1-3},
  pages = {249-271},
  month = mar,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-TCS05.ps},
  doi = {10.1016/j.tcs.2005.11.020},
  abstract = {We consider model checking of timed 
	temporal formulae in \emph{durational transition 
	graphs} (DTGs), \emph{i.e.}, Kripke structures where 
	transitions have integer durations. Two semantics for 
	DTGs are presented and motivated. We consider timed 
	versions of CTL where subscripts put quantitative 
	constraints on the time it takes before a property is 
	satisfied. \par
	We exhibit an important gap between logics where 
	subscripts of the form {"}\(= c\){"} (exact duration) are 
	allowed, and simpler logics that only allow subscripts 
	of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded 
	duration).\par
	Without exact durations, model checking can be done in 
	polynomial time, but with exact durations, it becomes 
	\(\Delta_{2}^{P}\)-complete or PSPACE-complete 
	depending on the considered semantics.}
}
@inproceedings{MOJ-aisc2006,
  address = {Beijing, China},
  month = sep,
  year = 2006,
  volume = 4120,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Calmet, Jacques and Ida, Tetsuo and Wang, Dongming},
  acronym = {{AISC}'06},
  booktitle = {{P}roceedings of the 8th {I}nternational {C}onference
           on {A}rtificial {I}ntelligence and {S}ymbolic {C}omputation
           ({AISC}'06)},
  author = {Mitsuhashi, Ichiro and Oyamaguchi, Michio and Jacquemard, Florent},
  title = {The Confluence Problem for Flat~{TRSs}},
  pages = {68-81},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf},
  doi = {10.1007/11856290_8},
  abstract = {We prove that the properties of reachability, joinability and
confluence are undecidable for flat~TRSs. Here, a~TRS is flat if the heights
of the left and right-hand sides of each rewrite rule are at most one.}
}
@article{MR-TCS05,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
  title = {Model Checking Restricted Sets of Timed Paths},
  year = {2006},
  month = aug,
  volume = 358,
  number = {2-3},
  pages = {273-292},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
		 Markey-Raskin-TCS05.ps},
  doi = {10.1016/j.tcs.2006.01.019},
  abstract = {In this paper, we study the complexity of 
	model-checking formulas of four important real-time 
	logics (TPTL, MTL, MITL, and TCTL) over restricted sets 
	of timed paths. The classes of restricted sets of timed 
	paths that we consider are \textit{(i)}~a~single finite 
	(or ultimately periodic) timed path, 
	\textit{(ii)}~an~infinite set of finite (or infinite) 
	timed paths defined by a finite (or ultimately periodic) 
	path in a region graph, \textit{(iii)}~an~infinite set of 
	finite (or infinite) timed paths defined by a finite (or 
	ultimately periodic) path in a zone graph.
	\par
	Several results are quite negative: TPTL and MTL 
	remain undecidable along
	region- and zone-paths. On the other hand, 
	we obtained PTIME algorithms for
	model checking TCTL along a region path, 
	and for MTL along a single timed path.}
}
@article{MS05-IPL,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title = {Mu-Calculus Path Checking},
  volume = 97,
  number = 6,
  month = mar,
  year = 2006,
  pages = {225-230},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS05-IPL.ps},
  doi = {10.1016/j.ipl.2005.11.010},
  abstract = {We investigate the path model 
	checking problem for the \(\mu\)-calculus. 
	Surprisingly, restricting to deterministic 
	structures does not allow for more efficient model 
	checking algorithm, as we prove that it can encode 
	any instance of the standard model checking problem 
	for the \(\mu\)-calculus. }
}
@article{RS-btl2,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Rabinovich, Alexander and 
		   Schnoebelen, {\relax Ph}ilippe},
  title = {{\(\mathit{\MakeUppercase{BTL}}_2\)} and the expressive 
		   power of {\(\mathit{\MakeUppercase{ECTL}}^+\)}},
  year = 2006,
  month = jul,
  volume = 204,
  number = 7,
  pages = {1023-1044},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BTL2-InfComp.ps},
  doi = {10.1016/j.ic.2005.07.006},
  abstract = {We show that \(\mathit{ECTL}^+\), the 
	classical extension of \(\mathit{CTL}\) with fairness 
	properties, is expressively equivalent to 
	\(\mathit{BTL}_2\), a natural fragment of the monadic 
	logic of order. \(\mathit{BTL}_2\)~is the branching-time 
	logic with arbitrary quantification over paths, and 
	where path formulae are restricted to quantifier 
	depth~\(2\) first-order formulae in the monadic logic of 
	order. This result, linking \(\mathit{ECTL}^+\) to a 
	natural fragment of the monadic logic of order, provides 
	a characterization that other branching-time logics, 
	\emph{e.g.}, \(\mathit{CTL}\), lack. \par
	We then go on to show that \(\mathit{ECTL}^+\) and 
	\(\mathit{BTL}_2\) are not finitely based (\emph{i.e.}, 
	they cannot be defined by a finite set of temporal 
	modalities) and that their model-checking problems are 
	of the same complexity. }
}
@misc{phs-lipn2006,
  author = {Schnoebelen, {\relax Ph}ilippe},
  title = {De nouvelles applications pour le model-checking},
  year = {2006},
  month = nov,
  howpublished = {Invited lecture, Journ{\'e}es {\`a} l'occasion des
                  20~ans du~LIPN, Villetaneuse, France}
}
@phdthesis{THESE-bernat06,
  author = {Bernat, Vincent},
  title = {Th{\'e}ories de l'intrus pour la v{\'e}rification 
                 des protocoles cryptographiques},
  year = 2006,
  month = jun,
  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/these-bernat.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bernat.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bernat.ps}
}
@phdthesis{THESE-delaune06,
  author = {Delaune, St{\'e}phanie},
  title = {V{\'e}rification des protocoles cryptographiques 
                 et propri{\'e}t{\'e}s alg{\'e}briques},
  year = 2006,
  month = jun,
  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/these-delaune.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-delaune.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-delaune.ps},
  abstract = {Cryptographic protocols are small concurrent programs designed
to guarantee the security of exchanges between participants using non-secure
medium. Establishing the correctness of these protocols is crucial given the
increasing number of applications, such as electronic commerce, that exchange
information on the Internet. Unfortunately, the existence of cryptographic
primitives such as encryption is not sufficient to ensure security. The
security of exchanges is ensured by cryptographic protocols which are
notoriously error-prone.\par
The formal verification of cryptographic protocols is a difficult problem that
can be seen as a particular model-checking problem in an hostile environment.
To verify such protocols, a line of research consists in considering
encryption as a black box and assuming that an adversary can't learn anything
from an encrypted message except if he has the key. This is called the
\emph{perfect cryptography} assumption. Many results have been obtained under
this assumption, but such an assumption is too strong in general. Some attacks
exploit in a clever way the interaction between protocol rules and properties
of cryptographic operators. \par
In this thesis, we relax the perfect cryptography assumption by taking into
account some algebraic properties of cryptographic primitives. We give
decision procedures for the security problem in presence of several algebraic
operators.}
}
@phdthesis{THESE-lafourcade06,
  author = {Lafourcade, Pascal},
  title = {V{\'e}rification des protocoles cryptographiques 
                 en pr{\'e}sence de th{\'e}ories {\'e}quationnelles},
  year = 2006,
  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/these-lafourcade.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-lafourcade.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-lafourcade.ps},
  note = {209~pages},
  abstract = {The rise of the internet of new technologies has reinforced the
key role of computer science in communication technology. The recent progress
in these technologies has brought a dramatic change in the ways how we
communicate and consume. All these communication activities are subject to
complex communication protocols that a user does not control completely. Users
of communication protocols require that their communications are {"}secure{"}.
The developers of these communication protocols aim to secure communications
in a hostile environment by cryptographic means. Such an environment consists
of a dishonest communication participant, called an {"}intruder{"} or
{"}attacker{"}... We suppose that the intruder controls the network on which
the messages are exchanged.\par
The verification of a cryptographic protocol either ensures that no attack is
possible against the execution of the protocol in presence of a certain
intruder, or otherwise exhibits an attack. One important assumption in the
verification of cryptographic protocols is the so-called {"}perfect
cryptography assumption{"}, which states that the only way to obtain knowledge
about an encrypted message is to know its decryption key. This hypothesis is
not sufficient to guarantee security in reality. It is possible that certain
properties used in the protocol allow the intruder to obtain some
information.\par
One way to weaken this perfect cryptography assumption is to take into account
in the model certain algebraic properties. We develop a formal approach for
verifying the so-called secrecy property of cryptographic protocols in the
presence of equational theories and of homomorphism.}
}
@phdthesis{THESE-belmokadem06,
  author = {Bel{ }mokadem, Houda},
  title = {V{\'e}rification des propri{\'e}t{\'e}s temporis{\'e}es des 
                 automates programmables industriels},
  year = 2006,
  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/these-mokadem.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-mokadem.pdf}
}
@phdthesis{THESE-bertrand06,
  author = {Bertrand, Nathalie},
  title = {Mod{\`e}les stochastiques pour les pertes de messages dans les 
                 protocoles asynchrones et techniques de v{\'e}rification automatique},
  year = 2006,
  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/PDF/these-bertrand.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bertrand.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bertrand.ps}
}
@mastersthesis{naves-master,
  author = {Naves, Guyslain},
  title = {Accessibilit{\'e} dans les automates temporis{\'e}s {\`a} deux horloges},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2006,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-naves.ps}
}
@mastersthesis{akshay-master,
  author = {Akshay, S.},
  title = {Formal Specification and Verification of Timed Communicating Systems},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  month = sep,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf}
}
@mastersthesis{brochenin-master,
  author = {Brochenin, R{\'e}mi},
  title = {Techniques d'automates pour raisonner sur la m{\'e}moire},
  school = {{M}aster {R}echerche {I}nformatique de {L}yon~--- 
        {I}nformatique {F}ondamentale, Lyon, France},
  type = {Rapport de {M}aster},
  month = jun,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps}
}
@mastersthesis{bursuc-master,
  author = {Bursuc, Sergiu},
  title = {Contraintes de d{\'e}ductibilit{\'e} modulo
                 Associativit{\'e}-Commutativit{\'e}},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  month = sep,
  year = 2006,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf}
}
@techreport{LSV:06:11,
  author = {Bollig, Benedikt and Kuske, Dietrich},
  title = {Distributed {M}uller Automata and Logics},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2006,
  month = may,
  type = {Research Report},
  number = {LSV-06-11},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2006-11.ps},
  note = {23~pages},
  abstract = {We consider Muller asynchronous cellular automata running on
infinite dags over distributed alphabets. We show that they have the same
expressive power as the existential fragment of a monadic second-order logic
featuring a first-order quantifier to express that there are infinitely many
elements satisfying some property. Our result is based on an extension of the
classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to cope with infinite structures
and the new first-order quantifier. As a byproduct, we obtain a logical
characterization of unbounded Muller message-passing automata running on
infinite message sequence charts.}
}
@techreport{LSV:06:13,
  author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
  title = {Detecting Subverted Cryptographic Protocols by Entropy Checking},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2006,
  month = jun,
  type = {Research Report},
  number = {LSV-06-13},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
  note = {19~pages},
  abstract = {What happens when your implementation of SSL or some other
  cryptographic protocol is subverted through a buffer overflow
  attack?  You have been hacked, right.  Unfortunately, you may be
  unaware of~it: since normal traffic is encrypted, most IDSs cannot
  monitor~it.  We propose a simple, yet efficient technique to detect
  such attacks, by computing the entropy of the flow and comparing it
  against known thresholds.  This was implemented in the Net-Entropy
  sensor.}
}
@techreport{Prouve:rap9,
  author = {Klay, Francis and Bozga, Liana and Lakhnech, Yassine and
		 Mazar{\'e}, Laurent and Delaune, St{\'e}phanie and 
		 Kremer, Steve},
  title = {Retour d'exp{\'e}rience sur la validation du vote {\'e}lectronique},
  institution = {projet RNTL PROUV{\'E}},
  month = nov,
  year = 2006,
  type = {Technical Report},
  number = 9,
  note = {47~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf},
  abstract = {Dans ce rapport, nous pr{\'e}sentons le travail de
    v{\'e}rification qui a {\'e}t{\'e} r{\'e}alis{\'e} sur le protocole de
    vote {\'e}lectronique que nous avons introduit et formalis{\'e} dans le
    rapport RNTL Prouv{\'e} num{\'e}ro~\(6\). Ce protocole a {\'e}t{\'e} mis au
    point par J.~Traor{\'e}, ing{\'e}nieur de recherche chez France
    T{\'e}l{\'e}com. Il est bas{\'e} sur le m{\'e}canisme de signature en
    aveugle et peut {\^e}tre consid{\'e}r{\'e} comme un d{\'e}riv{\'e} du
    protocole de Fujioka, Okamoto et~Ohta.\par
    La formalisation de ce protocole {\`a} mis en {\'e}vidence une grande
    complexit{\'e} due en particulier aux structures de donn{\'e}es et aux
    primitives cryptographiques manipul{\'e}es. D'un autre c{\^o}t{\'e} ce
    travail a {\'e}galement r{\'e}v{\'e}l{\'e} que les propri{\'e}t{\'e}s de
    s{\^u}ret{\'e} {\`a} garantir sont particuli{\`e}rement subtiles.
    Ce~document pr{\'e}sente les r{\'e}sultats qui ont {\'e}t{\'e} obtenus
    lors de la v{\'e}rification de ce protocole. En particulier nous montrons
    que certaines propri{\'e}t{\'e}s de s{\^u}ret{\'e} ont pu {\^e}tre
    prouv{\'e}es automatiquement alors que pour d'autres une preuve manuelle
    s'est av{\'e}r{\'e}e n{\'e}cessaire.}
}
@misc{versydis-final,
  author = {Gastin, Paul and others},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {VERSYDIS}~--- 
            Rapport final},
  year = 2006,
  month = oct,
  type = {Contract Report},
  note = {10~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf}
}
@misc{cortos-final,
  author = {Bouyer, Patricia and others},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}~--- 
            Rapport final},
  year = 2006,
  month = nov,
  type = {Contract Report},
  note = {17~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf}
}
@misc{persee-final,
  author = {Schnoebelen, {\relax Ph}ilippe and Bouajjani, Ahmed and Sutre, Gr{\'e}goire},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~--- 
            Rapport final},
  year = 2006,
  month = nov,
  type = {Contract Report},
  note = {12~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf}
}
@article{Baudet05jalc,
  journal = {Journal of Automata, Languages and Combinatorics},
  author = {Baudet, Mathieu},
  title = {Random Polynomial-Time Attacks and {D}olev-{Y}ao Models},
  year = 2006,
  volume = 11,
  number = 1,
  pages = {7-21},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bau05-jalc.ps},
  abstract = {In this paper we present an extension of 
	Dolev-Yao models for security protocols with a notion 
	of random polynomial-time (Las Vegas) computability. 
	First we notice that Dolev-Yao models can be seen as 
	transition systems, possibly infinite. We then extend 
	these transition systems with computation times and 
	probabilities. The extended models can account for 
	normal Dolev-Yao transitions as well as nonstandard 
	operations such as inverting a one-way function. Our 
	main contribution consists of showing that under 
	reasonable assumptions the extended models are 
	equivalent to standard Dolev-Yao models as far as 
	(safety) security properties are concerned.}
}
@article{Demri-jancl06,
  publisher = {Taylor \& Francis},
  journal = {Journal of Applied Non-Classical Logics},
  author = {Demri, St{\'e}phane},
  title = {Linear-Time Temporal Logics with {P}resburger Constraints: An~Overview},
  year = 2006,
  volume = 16,
  number = {3-4},
  pages = {311-347},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
  abstract = {We present an overview of linear-time temporal logics with
Presburger constraints whose models are sequences of tuples of integers. Such
formal specification languages are well-designed to specify and verify systems
that can be modelled with counter systems. The paper recalls the general
framework of LTL over concrete domains and presents the main decidability and
complexity results related to fragments of Presburger~LTL. Related formalisms
are also briefly presented.}
}
@misc{NB-SuMo-2006,
  author = {Bertrand, Nathalie},
  title = {SuMo~-- Reachability analysis for lossy channels},
  month = feb,
  year = {2006},
  note = {See~\cite{BBS-forte06} for a description. Written in~OCaml (3000~lines)},
  note-fr = {Voir la description dans~\cite{BBS-forte06}. {\'E}crit
                  en~OCaml (3000~lignes)}
}
@misc{gastex-v2.8,
  author = {Gastin, Paul},
  title = {Gas{{\TeX}}: Graphs and Automata Simplified in~{{\TeX}} (v2.8)},
  year = {2006},
  month = nov,
  nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html},
  note = {Written in~\TeX (about 2000 lines)},
  note-fr = {\'Ecrit en~\TeX (environ 2000 lignes)},
  url = {http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html}
}
@proceedings{AGHMR-sasyft04,
  title = {Selected papers of the International Workshop on 
	   Security Analysis of Systems: Formalisms and Tools
           ({SASYFT}'04)},
  booktitle = {Selected papers of the International Workshop on 
	   Security Analysis of Systems: Formalisms and Tools
           ({SASYFT}'04)},
  editor = {Anantharaman, Siva and Gastin, Paul and Hains, Ga{\'e}tan and
           Mullins, John and Rusinowitch, Micha{\"e}l},
  year = 2006,
  address = {Orl{\'e}ans, France},
  journal = {jalc},
  volume = 11,
  number = 1
}
@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.