@inproceedings{FLS-ilc07,
  address = {Cape Town, South Africa},
  month = oct,
  year = 2009,
  volume = 5489,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  editor = {Archibald, Margaret and Brattka, Vasco and
	  Goranko, Valentin and L{\"o}we, Benedikt},
  acronym = {{ILC}'07},
  booktitle = {{R}evised {S}elected {P}apers of the 
		 {I}nternational {C}onference on {I}nfinity
		 in {L}ogic {\&} {C}omputation ({ILC}'07)},
  author = {Finkel, Alain and Lozes, {\'E}tienne and Sangnier, Arnaud},
  title = {Towards Model Checking Pointer Systems},
  pages = {56-82},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FLS-ilc07.ps},
  doi = {10.1007/978-3-642-03092-5_6},
  abstract = {We aim at checking safety and temporal properties over models
    representing the behavior of programs manipulating dynamic singly-linked
    lists. The properties we consider not only allow to perform a classical
    shape analysis, but we also want to check quantitative aspect on the
    manipulated memory heap. We first explain how a translation of programs
    into counter systems can be used to check safety problems and temporal
    properties. We then study the decidability of these two problems
    considering some restricted classes of programs, namely flat programs
    without destructive update. We obtain the following results: (1)~the
    model-checking problem is decidable if the considered program works over
    acyclic lists; (2)~the safety problem is decidable for programs without
    alias test. We finally explain the limit of our decidability results,
    showing that relaxing one of the hypothesis leads to undecidability
    results.}
}
@article{CEFX-fmsd08,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
                  Fribourg, Laurent and Xu, Weiwen},
  title = {Timed Verification of the Generic Architecture of a Memory
                  Circuit Using Parametric Timed Automata},
  volume = 34,
  number = 1,
  pages = {59-81},
  year = 2009,
  month = feb,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-fmsd08.ps},
  doi = {10.1007/s10703-008-0061-x},
  abstract = {Using a variant of Clariso-Cortadella's parametric
    method for verifying asynchronous circuits, we analyse some crucial timing
    behaviors of the architecture of SPSMALL memory, a~commercial product of
    STMicroelectronics. Using the model of parametric timed automata and model
    checker HYTECH, we~formally derive a set of linear constraints that ensure
    the correctness of the response times of the memory. We are also able to
    infer the constraints characterizing the optimal setup timings of input
    signals. We have checked, for two different implementations of this
    architecture, that the values given by our model match remarkably with the
    values obtained by the designer through electrical simulation. }
}
@inproceedings{EF-infinity07,
  optaddress = {Lisbon, Portugal},
  month = jul,
  year = 2009,
  volume = 239,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  realeditor = {Madhusudan, P. and Kahlon, Vineet},
  editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
  acronym = {{INFINITY}'06,'07,'08},
  booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational 
               {W}orkshops on {V}erification of {I}nfinite
               {S}tate {S}ystems
               ({INFINITY}'06,'07,'08)},
  author = {Encrenaz, Emmanuelle and Finkel, Alain},
  title = {Automatic verification of counter systems with ranking functions},
  pages = {85-103},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EF-infinity07.ps},
  doi = {10.1016/j.entcs.2009.05.032},
  abstract = {The verification of final termination for counter systems is
    undecidable. For non flattable counter systems, the verification of this
    type of property is generally based on the exhibition of a ranking
    function. Proving the existence of a ranking function for general counter
    systems is also undecidable. We~provide a framework in which the
    verification whether a given function is a ranking function is decidable.
    This framework is applicable to convex counter systems which admit a
    Presburger or a LPDS ranking function. This extends the results of
    [A.~Bradley, Z.~Manna, and B.~Sipma. \textit{Termination analysis of
    integer linear loops}. In~CONCUR'05, LNCS~3653, p.~488-502. Springer].
    From this framework, we derive a model-checking algorithm to verify
    whether a final termination property is satisfied or not. This approach
    has been successfully applied to the verification of a parametric version
    of the ZCSP protocol.}
}
@inproceedings{Bouyer-M4M5,
  address = {Cachan, France},
  month = mar,
  year = 2009,
  volume = 231,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Areces, Carlos and Demri, St{\'e}phane},
  acronym = {{M4M-5}},
  booktitle = {{P}roceedings of the 4th
               {W}orkshop on {M}ethods for {M}odalities
               ({M4M-5})},
  author = {Bouyer, Patricia},
  title = {Model-Checking Timed Temporal Logics},
  pages = {323-341},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
  doi = {10.1016/j.entcs.2009.02.044},
  abstract = {In this paper, we present several timed extensions of temporal
                  logics, that can be used for model-checking real-time
                  systems. We give different formalisms and the corresponding
                  decidability/complexity results. We also give intuition to
                  explain these results.}
}
@proceedings{M4M5-AD,
  editor = {Areces, Carlos and Demri, St{\'e}phane},
  title = {{P}roceedings of the 5th {I}nternational {W}orkshop on
 		{M}ethods for {M}odalities  ({M4M-5})},
  booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on
 		{M}ethods for {M}odalities  ({M4M-5})},
  publisher = {Elsevier Science Publishers},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = 231,
  year = 2009,
  month = mar,
  address = {Cachan, France},
  url = {http://www.sciencedirect.com/science/journal/15710661/231},
  doi = {10.1016/j.entcs.2009.02.025}
}
@article{CD-fmsd08,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  title = {Safely Composing Security Protocols},
  volume = 34,
  number = 1,
  pages = {1-36},
  month = feb,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CD-fmsd08.ps},
  doi = {10.1007/s10703-008-0059-4},
  abstract = {Security protocols are small programs that are executed in
    hostile environments. Many results and tools have been developed to
    formally analyze the security of a protocol in the presence of an active
    attacker that may block, intercept and send new messages. However even
    when a protocol has been proved secure, there is absolutely no guarantee
    if the protocol is executed in an environment where other protocols are
    executed, possibly sharing some common keys like public keys or long-term
    symmetric keys.\par
    In this paper, we show that security of protocols can be easily composed.
    More precisely, we show that whenever a protocol is secure, it remains
    secure even in an environment where arbitrary protocols satisfying a
    reasonable (syntactic) condition are executed. This result holds for a
    large class of security properties that encompasses secrecy and various
    formulations of authentication.}
}
@inproceedings{GGJ-wrs08,
  address = {Castle of Hagenberg, Austria},
  month = apr,
  year = 2009,
  volume = 237,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Middeldorp, Aart},
  acronym = {{WRS}'08},
  booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on 
		{R}eduction {S}trategies in {R}ewriting and {P}rogramming ({WRS}'08)},
  author = {Gasc{\'o}n, Adri{\`a} and Godoy, Guillem and Jacquemard,
                  Florent},
  title = {Closure of Tree Automata Languages under Innermost Rewriting},
  pages = {23-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf},
  doi = {10.1016/j.entcs.2009.03.033},
  abstract = {Preservation of regularity by a term rewriting system~(TRS)
     states that the set of reachable terms from a tree automata~(TA) language
     (a.k.a.~regular term set) is also a TA language. It~is an important and
     useful property, and there have been many works on identifying classes of
     TRS ensuring~it; unfortunately, regularity is not preserved for
     restricted classes of TRS like shallow~TRS. Nevertheless, this property
     has not been studied for important strategies of rewriting like the
     innermost strategy which corresponds to the call by value computation of
     programming languages.\par
     We prove that the set of innermost-reachable terms from a TA language by
     a shallow TRS is not necessarily regular, but it can be recognized by a
     TA with equality and disequality constraints between brothers. As~a
     consequence we conclude decidability of regularity of the reachable set
     of terms from a TA language by innermost rewriting and shallow TRS. This
     result is in contrast with plain (not necessarily innermost) rewriting
     for which we prove undecidability. We also show that, like for plain
     rewriting, innermost rewriting with linear and right-shallow TRS
     preserves regularity.}
}
@inproceedings{EB-fast08,
  address = {Malaga, Spain},
  month = apr,
  year = 2009,
  volume = 5491,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Degano, Pierpaolo and Guttman,  Joshua and 
		Martinelli, Fabio},
  acronym = {{FAST}'08},
  booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop on 
	   {F}ormal {A}spects in {S}ecurity and {T}rust ({FAST}'08)},
  author = {Bursztein, Elie},
  title = {Extending Anticipation Games with Location, Penalty and
        Timeline},
  pages = {272-286},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf},
  doi = {10.1007/978-3-642-01465-9_18},
  abstract = {Over the last few years, attack graphs have became a well
    recognized tool to analyze and model complex network attack. The most
    advanced evolution of attack graphs, called anticipation games, is based
    on game theory. However even if anticipation games allow to model time,
    collateral effects and player interactions with the network, there is
    still key aspects of the network security that cannot be modeled in this
    framework. Theses aspects are network cooperation to fight unknown attack,
    the cost of attack based on its duration and the introduction of new
    attack over the time. In this paper we address these needs, by introducing
    a three-fold extension to anticipation games. We prove that this extension
    does not change the complexity of the framework. We illustrate the
    usefulness of this extension by presenting how it can be used to find a
    defense strategy against 0 days that use an honey net. Finally, we have
    implemented this extension into a prototype, to show that it can be used
    to analyze large networks security.}
}
@article{DKR-jcs08,
  publisher = {{IOS} Press},
  journal = {Journal of Computer Security},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
  title = {Verifying Privacy-type Properties of Electronic Voting 
		 Protocols},
  volume = 17,
  number = 4,
  month = jul,
  year = 2009,
  pages = {435-487},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-jcs08.ps},
  doi = {10.3233/JCS-2009-0340},
  abstract = {Electronic voting promises the possibility of a convenient,
    efficient and secure facility for recording and tallying votes in an
    election. Recently highlighted inadequacies of implemented systems have
    demonstrated the importance of formally verifying the underlying voting
    protocols. We study three privacy-type properties of electronic voting
    protocols: in increasing order of strength, they are vote-privacy,
    receipt-freeness, and coercion-resistance.\par
    We use the applied pi calculus, a formalism well adapted to modelling such
    protocols, which has the advantages of being based on well-understood
    concepts. The privacy-type properties are expressed using observational
    equivalence and we show in accordance with intuition that
    coercion-resistance implies receipt-freeness, which implies vote-privacy.\par
    We illustrate our definitions on three electronic voting protocols from
    the literature. Ideally, these three properties should hold even if the
    election officials are corrupt. However, protocols that were designed to
    satisfy receipt-freeness or coercion-resistance may not do so in the
    presence of corrupt officials. Our model and definitions allow us to
    specify and easily change which authorities are supposed to be
    trustworthy.}
}
@inproceedings{BFS-infinity08,
  optaddress = {Toronto, Canada},
  month = jul,
  year = 2009,
  volume = 239,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
  acronym = {{INFINITY}'06,'07,'08},
  booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational 
               {W}orkshops on {V}erification of {I}nfinite
               {S}tate {S}ystems
               ({INFINITY}'06,'07,'08)},
  author = {Bouchy, Florent and Finkel, Alain and Sangnier, Arnaud},
  title = {Reachability in Timed Counter Systems},
  pages = {167-178},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
  doi = {10.1016/j.entcs.2009.05.038},
  abstract = {We introduce Timed Counter Systems, a~new class of systems
    mixing clocks and counters. Such systems have an infinite state space,
    hence their reachability problems are undecidable. By~abstracting clock
    values with a Region Graph, we~show the Counter Reachability Problem to be
    decidable for three subclasses: Timed~VASS, Bounded Timed Counter Systems,
    and Reversal-Bounded Timed Counter Systems.}
}
@proceedings{HV-infinity2008,
  title = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational 
           {W}orkshops on {V}erification of {I}nfinite
           {S}tate {S}ystems
           ({INFINITY}'06,'07,'08)},
  booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational 
               {W}orkshops on {V}erification of {I}nfinite
               {S}tate {S}ystems
               ({INFINITY}'06,'07,'08)},
  optacronym = {{INFINITY}'06,'07,'08},
  editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
  publisher = {Elsevier Science Publishers},
  doi = {10.1016/j.entcs.2009.05.026},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = 239,
  year = 2009,
  month = jul,
  optaddress = {Toronto, Canada}
}
@incollection{DG-hwa08,
  year = 2009,
  series = {EATCS Monographs in Theoretical Computer Science},
  publisher = {Springer},
  editor = {Kuich, Werner and Vogler, Heiko and Droste, Manfred},
  booktitle = {Handbook of Weighted Automata},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted automata and weighted logics},
  pages = {175-211},
  chapter = 5,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf}
}
@incollection{DG-pct08,
  futureaddress = {},
  month = jan,
  year = 2009,
  series = {IARCS-Universities},
  publisher = {Universities Press},
  booktitle = {Perspectives in Concurrency Theory},
  editor = {Lodaya, Kamal and Mukund, Madhavan and
		 Ramanujam, R.},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Local safety and local liveness for distributed systems},
  pages = {86-106},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
  abstract = {We introduce local safety and local liveness for distributed
    systems whose executions are modeled by Mazurkiewicz traces. We
    characterize local safety by local closure and local liveness by local
    density. Restricting to first-order definable properties, we prove a
    decomposition theorem in the spirit of the separation theorem for linear
    temporal logic. We then characterize local safety and local liveness by
    means of canonical local temporal logic formulae.}
}
@article{DL-tocl08,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
  title = {{LTL} with the freeze quantifier and register automata},
  volume = 10,
  number = 3,
  nopages = {},
  month = apr,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
  doi = {10.1145/1507244.1507246},
  abstract = {A data word is a sequence of pairs of a letter from a finite
    alphabet and an element from an infinite set, where the latter can only be
    compared for equality. To reason about data words, linear temporal logic
    is extended by the freeze quantifier, which stores the element at the
    current word position into a register, for equality comparisons deeper in
    the formula. By translations from the logic to alternating automata with
    registers and then to faulty counter automata whose counters may
    erroneously increase at any time, and from faulty and error-free counter
    automata to the logic, we obtain a complete complexity table for logical
    fragments defined by varying the set of temporal operators and the number
    of registers. In~particular, the~logic with future-time operators and
    \(1\)~register is decidable but not primitive recursive over finite data
    words. Adding past-time operators or \(1\)~more register, or switching to
    infinite data words, cause undecidability.}
}
@article{AP-ieeedeb09,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Data Engineering Bulletin},
  author = {Abiteboul, Serge and Polyzotis, Neoklis},
  title = {Searching Shared Content in Communities with the Data Ring},
  volume = 32,
  number = 2,
  pages = {44-51},
  year = 2009,
  month = jun,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf},
  doi = {},
  abstract = {Information ubiquity has created a large crowd of users (most
    notably scientists), who could employ DBMS technology to share and search
    their data more effectively. Still, this user base prefers to keep its
    data in files that can be easily managed by applications such as
    spreadsheets, rather than deal with the complexity and rigidity of modern
    database systems.\par
    In this article, we describe a vision for enabling non-experts, such as
    scientists, to build content sharing communities in a true database
    fashion: declaratively. The proposed infrastructure, called the data ring,
    enables users to share and search their data with minimal effort; the user
    points to the data that should be shared, and the data ring becomes
    responsible for automatically indexing the data (to make it accessible),
    replicating it (for availability), and reorganizing its physical storage
    (for better query performance). We outline the salient features of our
    proposal, and outline recent technical advancements in realizing data
    rings.}
}
@article{ASV-ieeedeb09,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Data Engineering Bulletin},
  author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor},
  title = {Modeling and Verifying Active {XML} Artifacts},
  volume = 32,
  number = 3,
  pages = {10-15},
  year = 2009,
  month = sep,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf},
  doi = {}
}
@article{AKSS-jvldb09,
  publisher = {ACM Press},
  journal = {The VLDB Journal},
  author = {Abiteboul, Serge and Kimelfeld, Benny and Sagiv, Yehoshua and
  	  	 Senellart, Pierre},
  title = {On the expressiveness of probabilistic {XML} models},
  volume = 18,
  number = 5,
  pages = {1041-1064},
  year = 2009,
  month = oct,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf},
  doi = {10.1007/s00778-009-0146-1},
  abstract = {Various known models of probabilistic XML can be
    represented as instantiations of the abstract notion of
    \emph{p-documents}. In addition to ordinary nodes, p-documents have
    \emph{distributional} nodes that specify the possible worlds and their
    probabilistic distribution. Particular families of p-documents are
    determined by the types of distributional nodes that can be used as well
    as by the structural constraints on the placement of those nodes in a
    p-document. Some of the resulting families provide natural extensions and
    combinations of previously studied probabilistic XML models. The focus of
    the paper is on the expressive power of families of p-documents. In
    particular, two main issues are studied. The first is the ability to
    (efficiently) \emph{translate} a given p-document of one family into
    another family. The second is \emph{closure under updates}, namely, the
    ability to (efficiently) represent the result of updating the instances of
    a p-document of a given family as another p-document of that family. For
    both issues, we distinguish two variants corresponding to
    \emph{value-based} and \emph{object-based} semantics of p-documents.}
}
@inproceedings{ABM-edbt09,
  address = {Saint Petersburg, Russia},
  month = mar,
  year = 2009,
  novolume = {},
  series = {ACM International Conference Proceeding Series},
  publisher = {Springer},
  editor = {Kersten, Martin L. and Novikov, Boris and Teubner, Jens  and
                  Polutin, Vladimir and Manegold, Stefan},
  acronym = {{EDBT}'09},
  booktitle = {{A}dvances in {D}atabase {T}echnology~---
	   {P}roceedings of the 12th {I}nternational {C}onference on
                  {E}xtending {D}atabase {T}echnology ({EDBT}'09)},
  author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan},
  title = {Efficient maintenance techniques for views over active
                  documents},
  pages = {1076-1087},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf},
  doi = {10.1145/1516360.1516483},
  abstract = {Many Web applications are based on dynamic interactions between
    Web components exchanging flows of information. Such a situation arises
    for instance in mashup systems or when monitoring distributed autonomous
    systems. Our work is in this challenging context that has generated
    recently a lot of attention; see Web~2.0. We introduce the axlog formal
    model for capturing such interactions and show how this model can be
    supported efficiently. The central component is the axlog widget defined
    by one tree-pattern query or more, over an active document (in the Active
    XML style) that includes some input streams of updates. A widget generates
    a stream of updates for each query, the updates that are needed to
    maintain the view corresponding to the query. We exploit an array of known
    technologies: datalog optimization techniques such as Differential or
    MagicSet, constraint query languages, and efficient XML filtering
    (YFilter). The novel optimization technique we propose is based on
    fundamental new notions: a relevance (different than that of MagicSet),
    satisfiability and provenance for active documents. We briefly discuss an
    implementation of an axlog engine, an application that we used to test the
    approach, and results of experiments.}
}
@inproceedings{AGMP-icde2009,
  address = {Shanghai, China},
  month = mar # {-} # apr,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  editor = {Ioannidis, Yannis E. and Lee, Dik Lun and Ng, Raymond T.},
  acronym = {{ICDE}'09},
  booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on
                  {D}ata {E}ngineering ({ICDE}'09)},
  author = {Abiteboul, Serge and Greenshpan, Ohad and Milo, Tova and
                  Polyzotis, Neoklis},
  title = {Match{U}p: Autocompletion for Mashups},
  pages = {1479-1482},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf},
  doi = {10.1109/ICDE.2009.47},
  abstract = {A~\emph{mashup} is a Web application that integrates data,
    computation and GUI provided by several systems into a unique tool. The
    concept originated from the understanding that the number of applications
    available on the Web and the need for combining them to meet user
    requirements, are growing very rapidly. This demo presents \emph{MatchUp},
    a system that supports rapid, on-demand, intuitive development of
    \emph{mashups}, based on a novel \emph{autocompletion} mechanism. The key
    observation guiding the development of \emph{MatchUp} is that mashups
    developed by different users typically share common characteristics; they
    use similar classes of mashup components and glue them together in a
    similar manner. \emph{MatchUp} exploits these similarities to predict,
    given a user's partial mashup specification, what are the most likely
    potential \emph{completions} (missing components and connection between
    them) for the specification. Using a novel ranking algorithm, users are
    then offered top-k completions from which they choose and refine according
    to their needs.}
}
@article{CDMP-apal09,
  publisher = {Elsevier Science Publishers},
  journal = {Annals of Pure and Applied Logics},
  author = {Chevalier, Fabrice and D'Souza, Deepak and Matteplackel, Raj Mohan
                  and Prabhakar,  Pavithra},
  title = {Automata and logics over finitely varying functions},
  year = {2009},
  month = dec,
  volume = {161},
  number = {3},
  pages = {324-336},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf},
  doi = {10.1016/j.apal.2009.07.007},
  abstract = {We extend some of the classical connections between automata and
    logic due to B{\"u}chi~(1960) and McNaughton and Papert~(1971) to
    languages of finitely varying functions or {"}signals{"}. In particular,
    we introduce a natural class of automata for generating finitely varying
    functions called ST-NFAs, and show that it coincides in terms of language
    definability with a natural monadic second-order logic interpreted over
    finitely varying functions (Rabinovich, 2002). We also identify a
    {"}counter-free{"} subclass of ST-NFAs which characterise the first-order
    definable languages of finitely varying functions. Our proofs mainly
    factor through the classical results for word languages. These results
    have applications in automata characterisations for continuously
    interpreted real-time logics like Metric Temporal Logic (MTL) (Chevalier
    \emph{et~al.}, 2006,~2007).}
}
@phdthesis{mercier-phd2009,
  author = {Mercier, Antoine},
  title = {Contributions {\`a} l'analyse automatique des protocoles
                  cryptographiques en pr{\'e}sence de propri{\'e}t{\'e}s
                  alg{\'e}briques : protocoles de groupe, {\'e}quivalence
                  statique},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  year = 2009,
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf}
}
@phdthesis{bursuc-phd2009,
  author = {Bursuc, Sergiu},
  title = {Contraintes de d{\'e}ductibilit{\'e} dans une alg{\`e}bre
                  quotient: r{\'e}duction de mod{\`e}les et applications {\`a}
                  la s{\'e}curit{\'e}},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  year = 2009,
  month = dec,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf}
}
@incollection{CM-CES09,
  author = {Cassez, Franck and Markey, Nicolas},
  title = {Control of Timed Systems},
  booktitle = {Communicating Embedded Systems~-- Software and Design},
  editor = {Jard, Claude and Roux, Olivier H.},
  publisher = {Wiley-ISTE},
  year = 2009,
  month = oct,
  pages = {83-120},
  chapter = 3,
  url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  isbn = {9781848211438}
}
@incollection{DH-CES09,
  author = {Donatelli, Susanna and Haddad, Serge},
  title = {Quantitative Verification of {M}arkov Chains},
  booktitle = {Communicating Embedded Systems~-- Software and Design},
  editor = {Jard, Claude and Roux, Olivier H.},
  publisher = {Wiley-ISTE},
  year = 2009,
  month = oct,
  pages = {139-163},
  chapter = 5,
  url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  isbn = {9781848211438}
}
@inproceedings{JGL-asian09,
  address = {Seoul, Korea},
  month = dec,
  year = 2009,
  volume = 5913,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Datta, Anupam},
  acronym = {{ASIAN}'09},
  booktitle = {{P}roceedings of the 13th {A}sian
               {C}omputing {S}cience {C}onference
               ({ASIAN}'09)},
  author = {Goubault{-}Larrecq, Jean},
  title = {{\textquotedbl}{L}ogic Wins!{\textquotedbl}},
  pages = {1-16},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
  doi = {10.1007/978-3-642-10622-4_1},
  abstract = {Clever algorithm design is sometimes superseded by simple
    encodings into logic. We apply this motto to a few case studies in the
    formal verification of security properties. In particular, we examine
    confidentiality objectives in hardware circuit descriptions written in
    VHDL.}
}
@phdthesis{chamseddine-phd2009,
  author = {Chamseddine, Najla},
  title = {Analyse quantitative parametr{\'e}e d'automates temporis{\'e}s probabilistes},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  year = 2009,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf}
}
@phdthesis{bouchy-phd2009,
  author = {Bouchy, Florent},
  title = {Logiques et mod{\`e}les pour la v{\'e}rification de syst{\`e}mes infinis},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  year = 2009,
  month = nov,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf}
}
@phdthesis{sznajder-phd2009,
  author = {Sznajder, Nathalie},
  title = {Synth{\`e}se de syst{\`e}mes distribu{\'e}s ouverts},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  year = 2009,
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf}
}
@inproceedings{SRKK-wissec09,
  address = {Louvain-la-Neuve, Belgium},
  month = nov,
  year = 2009,
  editor = {Pereira, Olivier and Quisquater, Jean-Jacques and
		Standaert, Fran\c{c}ois-Xavier},
  acronym = {{WISSEC}'09},
  booktitle = {{P}roceedings of the 4th {B}enelux {W}orkshop on
		{I}nformation and {S}ystem {S}ecurity ({WISSEC}'09)},
  author = {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and
		   Kourjieh, Mounira},
  title = {Election verifiability in electronic voting protocols
		  (Preliminary version)},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf},
  abstract = {We~present a symbolic definition of election verifiability for
    electronic voting protocols. Our definition is given in terms of
    reachability assertions in the applied pi calculus and is amenable to
    automated reasoning using the tool ProVerif. The~definition distinguishes
    three aspects of verifiability, which we call individual, universal, and
    eligibility verifiability. It also allows us to determine precisely what
    aspects of the system are required to be trusted. We demonstrate our
    formalism by analysing the protocols due to Fujioka, Okamoto \&~Ohta and
    Juels, Catalano \&~Jakobsson; the~latter of which has been implemented by
    Clarkson, Chong \&~Myers. }
}
@inproceedings{CCD-secco09,
  address = {Bologna, Italy},
  month = oct,
  year = 2009,
  editor = {Boreale, Michele and Kremer, Steve},
  acronym = {{SecCo}'09},
  booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational
               {W}orkshop on {S}ecurity {I}ssues in
               {C}oordination {M}odels, {L}anguages and
               {S}ystems ({SecCo}'09)},
  author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
  title = {A~decision procedure for proving observational equivalence},
  nmnote = {did not appear in postproceedings EPTCS7},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf}
}
@proceedings{BK-secco2009,
  title = {{P}roceedings of the 7th {I}nternational {W}orkshop on
	  {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)},
  booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on
	  {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)},
  acronym = {{S}ec{C}o'09},
  editor = {Boreale, Michele and Kremer, Steve},
  doi = {10.4204/EPTCS.7},
  url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?SECCO2009},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = 7,
  year = 2009,
  month = aug,
  address = {Bologna, Italy}
}
@mastersthesis{dimino-m1,
  author = {Dimino, J{\'e}r{\'e}mie},
  title = {Les syst{\`e}mes {\`a} canaux non-fiables vus comme des
                  transducteurs},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de stage de {M1}},
  year = {2009},
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf}
}
@mastersthesis{cheval-master,
  author = {Cheval, Vincent},
  title = {Algorithme de d{\'e}cision de l'{\'e}quivalence symbolique de
                  syst{\`e}mes de contraintes},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = {2009},
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf}
}
@mastersthesis{brenguier-master,
  author = {Brenguier, Romain},
  title = {Calcul des {\'e}quilibres de Nash dans les jeux temporis{\'e}s},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = {2009},
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-brenguier.ps}
}
@techreport{LSV:09:20,
  author = {Andr{\'e}, {\'E}tienne},
  title = {Everything You Always Wanted to Know About {IMITATOR} (But~Were Afraid to~Ask)},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = jul,
  type = {Research Report},
  number = {LSV-09-20},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf},
  note = {11~pages},
  abstract = {We present here the user manual of IMITATOR, a tool for
    synthesizing constraints on timing bounds (seen as parameters) in the
    framework of timed automata. Unlike classical synthesis methods, the tool
    IMITATOR takes advantage of a given reference valuation of the parameters
    for which the system is known to behave properly. The goal of IMITATOR is
    to generate a constraint such that, under any valuation satisfying this
    constraint, the system is guaranteed to behave, in terms of alternating
    sequences of locations and actions, as under the reference valuation.\par
    We give here the installation requirements and the launching commands of
    IMITATOR, as well as the source code of a toy example.}
}
@inproceedings{DJLL-fsttcs09,
  address = {Kanpur, India},
  month = dec,
  year = 2009,
  volume = 4,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Kannan, Ravi and Narayan Kumar, K.},
  acronym = {{FSTTCS}'09},
  booktitle = {{P}roceedings of the 29th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'09)},
  author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish,
                  Oded and Lazi{\'c}, Ranko},
  title = {The covering and boundedness problems for branching vector addition systems},
  pages = {181-192},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2009.2317},
  abstract = {The covering and boundedness problems for branching vector
    addition systems are shown complete for doubly-exponential time.}
}
@inproceedings{DKP-fsttcs09,
  address = {Kanpur, India},
  month = dec,
  year = 2009,
  volume = 4,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Kannan, Ravi and Narayan Kumar, K.},
  acronym = {{FSTTCS}'09},
  booktitle = {{P}roceedings of the 29th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'09)},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and Pereira,
                 Olivier},
  title = {Simulation based security in the applied pi calculus},
  pages = {169-180},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2009.2316},
  abstract = {We present a symbolic framework for refinement and composition
    of security protocols. The framework uses the notion of ideal
    functionalities. These are abstract systems which are secure by
    construction and which can be combined into larger systems. They can be
    separately refined in order to obtain concrete protocols implementing
    them. Our work builds on ideas from computational models such as the
    universally composable security and reactive simulatability frameworks.
    The underlying language we use is the applied pi calculus which is a
    general language for specifying security protocols. In our framework we
    can express the different standard flavours of simulation-based security
    which happen to all coincide. We illustrate our framework on an
    authentication functionality which can be realized using the
    Needham-Schroeder-Lowe protocol. For this we need to define an ideal
    functionality for asymmetric encryption and its realization. We also show
    a joint state result for this functionality which allows composition (even
    though the same key material is reused) using a tagging mechanism.}
}
@article{BCHMMR-ijwsr09,
  publisher = {{IGI} Publishing},
  journal = {International Journal of Web Services Research},
  author = {Boutrous{-}Saab, C{\'e}line and Coulibaly, Demba and Haddad, Serge
                and Melliti, Tarek and Moreaux, Patrice and Rampacek, Sylvain},
  title = {An Integrated Framework for Web Services Orchestration},
  volume = 6,
  number = 4,
  pages = {1-29},
  year = 2009,
  month = sep,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
  abstract = {Currently, Web services give place to active research and this
    is due both to industrial and theoretical factors. On one hand, Web
    services are essential as the design model of applications dedicated to
    the electronic business. On the other hand, this model aims to become one
    of the major formalisms for the design of distributed and cooperative
    applications in an open environment (the Internet). In this article, the
    authors will focus on two features of Web services. The first one concerns
    the interaction problem: given the interaction protocol of a Web service
    described in BPEL, how to generate the appropriate client? Their approach
    is based on a formal semantics for BPEL via process algebra and yields an
    algorithm which decides whether such a client exists and synthesizes the
    description of this client as a (timed) automaton. The second one concerns
    the design process of a service. They propose a method which proceeds by
    two successive refinements: first the service is described via UML, then
    refined in a BPEL model and finally enlarged with JAVA code using JCSWL, a
    new language that we introduce here. Their solutions are integrated in a
    service development framework that will be presented in a synthetic way.}
}
@inproceedings{VLC-aplas09,
  address = {Seoul, Korea},
  month = dec,
  year = 2009,
  volume = {5904},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Hu, Zhenjiang},
  acronym = {{APLAS}'09},
  booktitle = {{P}roceedings of the 7th {A}sian {S}ymposium
               on {P}rogramming {L}anguages and {S}ystems
               ({APLAS}'09)},
  author = {Villard, Jules and Lozes, {\'E}tienne and Calcagno, Cristiano},
  title = {Proving Copyless Message Passing},
  pages = {194-209},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf},
  doi = {10.1007/978-3-642-10672-9_15},
  abstract = {Handling concurrency using a shared memory and locks is tedious
    and error-prone. One solution is to use message passing instead. We study
    here a particular, contract-based flavor that makes the ownership transfer
    of messages explicit. In this case, ownership of the heap region
    representing the content of a message is lost upon sending, which can lead
    to efficient implementations. In this paper, we define a proof system for
    a concurrent imperative programming language implementing this idea and
    inspired by the Singularity OS. The proof system, for which we prove
    soundness, is an extension of separation logic, which has already been
    used successfully to study various ownership-oriented paradigms.}
}
@inproceedings{AFS-avocs09,
  address = {Swansea, UK},
  month = sep,
  year = {2009},
  volume = 23,
  series = {Electronic Communications of the EASST},
  publisher = {European Association of Software Science and Technology},
  editor = {Roggenbach, Markus},
  acronym = {{AVoCS}'09},
  booktitle = {{P}roceedings of the 9th {I}nternational
               {W}orkshop on {A}utomated {V}erification
               of {C}ritical {S}ystems
               ({AVoCS}'09)},
  author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston,
                  Jeremy},
  title = {An Extension of the Inverse Method to Probabilistic Timed Automata},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
  abstract = {Probabilistic timed automata can be used to model systems in
    which probabilistic and timing behavior coexist. Verification of
    probabilistic timed automata models is generally performed with regard to
    a single reference valuation of the timing parameters. Given such a
    parameter valuation, we present a method for obtaining automatically a
    constraint on timing parameters for which the reachability probabilities
    (1)~remain invariant and (2)~are~equal to the reachability probabilities
    for the reference valuation. The method relies on parametric analysis of a
    non-probabilistic version of the probabilistic timed automata model using
    the {"}inverse method{"}. Our approach is useful for avoiding repeated
    executions of probabilistic model checking analyses for the same model
    with different parameter valuations. We provide examples of the
    application of our technique to models of randomized protocols.}
}
@incollection{HI-petrinet-diaz,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Symmetry and Temporal Logic},
  pages = {435-460},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-b,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {Verification of Specific Properties},
  pages = {349-414},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-c,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Tensor Methods and Stochastic {P}etri Nets},
  pages = {321-346},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-b,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Stochastic Well-formed {P}etri Nets},
  pages = {303-320},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-a,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Stochastic {P}etri Nets},
  pages = {269-302},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{H-petrinet-diaz,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge},
  title = {Decidability and Complexity of {P}etri Net Problems},
  pages = {87-122},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-a,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {Analysis Methods for {P}etri Nets},
  pages = {41-86},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@article{BBC-apal09,
  publisher = {Elsevier Science Publishers},
  journal = {Annals of Pure and Applied Logics},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
                 Chevalier, Fabrice},
  title = {Weighted O-Minimal Hybrid Systems},
  year = {2009},
  month = dec,
  volume = {161},
  number = {3},
  pages = {268-288},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
  doi = {10.1016/j.apal.2009.07.014},
  abstract = {We consider weighted o-minimal hybrid systems, which extend
    classical o-minimal hybrid systems with cost functions. These cost
    functions are 'observer variables' which increase while the system evolves
    but do not constrain the behaviour of the system. In this paper, we prove
    two main results: (i)~optimal o-minimal hybrid games are decidable;
    (ii)~the~model-checking of~WCTL, an~extension of CTL which can constrain
    the cost variables, is decidable over that model. This has to be compared
    with the same problems in the framework of timed automata where both
    problems are undecidable in general, while they are decidable for the
    restricted class of one-clock timed automata.}
}
@inproceedings{FLS-nordsec09,
  address = {Oslo, Norway},
  month = oct,
  year = 2009,
  volume = 5838,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {J{\o}sang, Audun and Maseng, Torleiv and Knapskog, Svein Johan},
  acronym = {{NordSec}'09},
  booktitle = {{P}roceedings of the 14th {N}ordic {W}orkshop on {S}ecure {IT}
                  {S}ystems ({NordSec}'09)},
  author = {Focardi, Riccardo and Luccio, Flaminia L. and
		 Steel, Graham},
  title = {Blunting Differential Attacks on {PIN} Processing {API}s},
  pages = {88-103},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
  doi = {10.1007/978-3-642-04766-4_7},
  abstract = {We~propose a countermeasure for a class of known attacks on the
    PIN processing API used in the ATM (cash machine) network. This API
    controls access to the tamper-resistant Hardware Security Modules where
    PIN encryption, decryption and verification takes place. The~attacks are
    differential attacks, whereby an attacker gains information about the
    plaintext values of encrypted customer PINs by making changes to the
    non-confidential inputs to a command. Our~proposed fix adds an integrity
    check to the parameters passed to the command. It~is novel in that it
    involves very little change to the existing ATM network infrastructure.}
}
@inproceedings{KMT-asian09,
  address = {Seoul, Korea},
  month = dec,
  year = 2009,
  volume = 5913,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Datta, Anupam},
  acronym = {{ASIAN}'09},
  booktitle = {{P}roceedings of the 13th {A}sian
               {C}omputing {S}cience {C}onference
               ({ASIAN}'09)},
  author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
  title = {Reducing Equational Theories for the Decision of Static
                  Equivalence},
  pages = {94-108},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-asian09.ps},
  doi = {10.1007/978-3-642-10622-4_8},
  abstract = {Static equivalence is a well established notion of
    indistinguishability of sequences of terms which is useful in the symbolic
    analysis of cryptographic protocols. Static equivalence modulo equational
    theories allows a more accurate representation of cryptographic primitives
    by modelling properties of operators by equational axioms. We develop a
    method that allows in some cases to simplify the task of deciding static
    equivalence in a multi-sorted setting, by removing a symbol from the term
    signature and reducing the problem to several simpler equational theories.
    We illustrate our technique at hand of bilinear pairings.}
}
@inproceedings{AF-ijcai09,
  address = {Pasadena, California, USA},
  month = jul,
  year = 2009,
  publisher = {AAAI Press},
  editor = {Boutilier, Craig},
  acronym = {{IJCAI}'09},
  booktitle = {{P}roceedings of the 21st {I}nternational {J}oint 
               {C}onference on {A}rtificial {I}ntelligence
               ({IJCAI}'09)},
  author = {Areces, Carlos and Figueira, Diego},
  title = {Which Semantics for Neighbourhood Semantics?},
  pages = {671-676},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AF-ijcai09.ps},
  abstract = {In this article we discuss two alternative proposals for
    neighbourhood semantics (which we call strict and loose neighbourhood
    semantics, NSS~and~NSL respectively) that have been previously introduced
    in the literature. Our~main tools are suitable notions of bisimulation.
    While an elegant notion of bisimulation exists for NSL, the required
    bisimulation for NSS is rather involved. We~propose a simple extension of
    NSS with a universal modality that we call NSS(E), which comes together
    with a natural notion of bisimulation. We~also investigate the complexity
    of the satisfiability problem for NSL and NSS(E).}
}
@techreport{LSV:09:16,
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
  title = {Verification on Interrupt Timed Automata},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = jul,
  type = {Research Report},
  number = {LSV-09-16},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
  note = {16~pages},
  abstract = {The class of Interrupt Timed Automata (ITA) has been introduced to
 model multi-task systems with interruptions in a single processor
 environment.  This is a subclass of hybrid automata in which real
 valued variables consist of a restricted type of stopwatches
 (variables with rate \(0\) or~\(1\)) organized along levels. While
 reachability is undecidable with usual stopwatches, it was proved
 that this problem is decidable in ITA and that untimed languages of
 ITA are effectively regular. Here we investigate the problem of
 model checking timed extensions of CTL over ITA and show in
 contrast that this problem is undecidable. On~the other hand, we
 prove that model checking is decidable for two relevant fragments of this
 timed logic: (1)~the~first one where formula contain only model
 clocks and (2)~the~second one where formulas have a single external
 clock.}
}
@techreport{LSV:09:15,
  author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril},
  title = {Seed: an Easy-to-Use Random Generator of Recursive Data Structures for Testing},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = jul,
  type = {Research Report},
  number = {LSV-09-15},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf},
  note = {16~pages},
  abstract = {Random testing represents a simple and tractable way for software
 assessment. This paper presents the Seed tool dedicated to the
 uniform random generation of recursive data structures as labelled
 trees or logical formulas.  We show how Seed can be used in several
 testing contexts, from model based testing to performance
 testing. Generated data structures are defined by grammar-like rules,
 given in an XML format, multiplying Seed possible applications.
 Seed is based on combinatorial techniques, and can generate uniformly
 at random \(k\)~structures of size~\(n\) with a
 time complexity in \(O(n^{2}+ kn\cdot \log(n))\). Finally, Seed is available as a free
 java application and a great effort has been made to make it
 easy-to-use.}
}
@techreport{LSV:09:13,
  author = {Andr{\'e}, {\'E}tienne and Encrenaz, Emmanuelle and Fribourg, Laurent},
  title = {Synthesizing Parametric Constraints on Various Case Studies Using {IMITATOR}},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = jun,
  type = {Research Report},
  number = {LSV-09-13},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
  note = {18~pages},
  abstract = {We present here applications of IMITATOR, a tool for
    synthesizing constraints on timing bounds (seen as parameters) in the
    framework of timed automata. Unlike classical synthesis methods, we take
    advantage of a given reference valuation of the parameters for which the
    system is known to behave properly. Our aim is to generate a constraint
    such that, under any valuation satisfying this constraint, the system is
    guaranteed to behave, in terms of alternating sequences of locations and
    actions, as under the reference valuation. This is useful for safely
    relaxing some values of the reference valuation, and optimizing timing
    bounds of the system. We have successfully applied our tool to various
    examples of asynchronous circuits and protocols, which are detailed in
    this report.}
}
@inproceedings{BFSP-infinity09,
  address = {Bologna, Italy},
  month = nov,
  year = 2009,
  volume = 10,
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Farzan, Azadeh and Legay, Axel},
  acronym = {{INFINITY}'09},
  booktitle = {{P}roceedings of the 11th {I}nternational 
           {W}orkshops on {V}erification of {I}nfinite
           {S}tate {S}ystems
           ({INFINITY}'09)},
  author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi},
  title = {Dense-choice Counter Machines Revisited},
  pages = {3-22},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
  doi = {10.4204/EPTCS.10.1},
  abstract = {This paper clarifies the picture about Dense-choice Counter
    Machines, which have been less studied than (discrete) Counter Machines.
    We revisit the definition of {"}Dense Counter Machines{"} so that it now
    extends (discrete) Counter Machines, and we provide new undecidability and
    decidability results. Using the first-order additive mixed theory of reals
    and integers, we give a logical characterization of the sets of
    configurations reachable by reversal-bounded Dense-choice Counter
    Machines.}
}
@inproceedings{AF-infinity09,
  address = {Bologna, Italy},
  month = nov,
  year = 2009,
  volume = 10,
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Farzan, Azadeh and Legay, Axel},
  acronym = {{INFINITY}'09},
  booktitle = {{P}roceedings of the 11th {I}nternational 
           {W}orkshops on {V}erification of {I}nfinite
           {S}tate {S}ystems
           ({INFINITY}'09)},
  author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
  title = {An Inverse Method for Policy-Iteration Based Algorithms},
  pages = {44-61},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
  doi = {10.4204/EPTCS.10.4},
  abstract = {We present an extension of two policy-iteration based algorithms
    on weighted graphs (viz.,~Markov Decision Problems and Max-Plus Algebras).
    This extension allows us to solve the following inverse problem:
    considering the weights of the graph to be unknown constants or
    parameters, we suppose that a reference instantiation of those weights is
    given, and we aim at computing a constraint on the parameters under which
    an optimal policy for the reference instantiation is still optimal. The
    original algorithm is thus guaranteed to behave well around the reference
    instantiation, which provides us with some criteria of robustness. We
    present an application of both methods to simple examples. A prototype
    implementation has been done.}
}
@inproceedings{BCLD-asian09,
  address = {Seoul, Korea},
  month = dec,
  year = 2009,
  volume = 5913,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Datta, Anupam},
  acronym = {{ASIAN}'09},
  booktitle = {{P}roceedings of the 13th {A}sian
               {C}omputing {S}cience {C}onference
               ({ASIAN}'09)},
  author = {Bursuc, Sergiu and Delaune, St{\'e}phanie and Comon{-}Lundh,
                  Hubert},
  title = {Deducibility constraints},
  pages = {24-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-asian09.ps},
  doi = {10.1007/978-3-642-10622-4_3},
  abstract = {In their work on tractable deduction systems, D.~McAllester and
    later D.~Basin and H.~Ganzinger have identified a property of inference
    systems (the~locality property) that ensures the tractability of the
    \textit{Entscheidungsproblem}.\par
    On~the other hand, deducibility constraints are sequences of deduction
    problems in which some parts (formulas) are unknown. The~problem is to
    decide their satisfiability and to represent the set of all possible
    solutions. Such constraints have also been used for deciding some security
    properties of cryptographic protocols.\par
    In this paper we show that local inference systems (actually a slight
    modification of such systems) yield not only a tractable deduction
    problem, but also decidable deducibility constraints. Our algorithm not
    only allows to decide the existence of a solution, but also gives a
    representation of all solutions.}
}
@incollection{ACL-fps09,
  noaddress = {},
  month = may,
  year = 2009,
  volume = 5458,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  noacronym = {},
  booktitle = {{F}ormal to {P}ractical {S}ecurity},
  editor = {Cortier, V{\'e}ronique and Kirchner, Claude and
		 Okada, Mitsuhiro and Sakurada, Hideki},
  author = {Affeldt, Reynald and Comon{-}Lundh, Hubert},
  title = {Verification of Security Protocols with a Bounded Number of
                  Sessions Based on Resolution for Rigid Variables},
  pages = {1-20},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf},
  doi = {10.1007/978-3-642-02002-5_1},
  abstract = {First-order logic resolution is a standard way to automate the
    verification of security protocols. However, it sometimes fails to produce
    security proofs for secure protocols because of the detection of false
    attacks. For the verification of a bounded number of sessions, false
    attacks can be avoided by introducing rigid variables. Unfortunately, this
    yields complicated resolution procedures. We show here that there is a
    simple translation of the security problem for a bounded number of
    sessions into first-order logic, that does not introduce false attacks.
    This is shown by translating clauses involving rigid variables into
    classical first-order clauses, while preserving satisfiability. We
    illustrate this approach by giving a complete and terminating strategy for
    a first-order logic fragment resulting from the above translation, that
    yields a decision procedure for a bounded number of sessions.}
}
@inproceedings{HMY-msr09,
  address = {Nantes, France},
  month = nov,
  year = 2009,
  number = {7-9},
  volume = {43},
  series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {Herm{\`e}s},
  editor = {Lime, Didier and Roux, Olivier H.},
  acronym = {{MSR}'09},
  booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'09)},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Bornes du temps de r{\'e}ponse des services Web composites},
  pages = {969-983},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
  abstract = {The quality of service (QoS) of Web services is a key
    factor of their success. This requires to design new methods in order to
    study~it. Here we propose families of upper bounding models for the
    response time of composite Web services for two kinds of composition: the
    statical and random {"}fork and merge{"}. In~the first~case, the~complexity of
    bounding models belongs to~\(O(n\cdot \sqrt{n})\) where \(n\)~is the
    number of called services whereas the complexity of the exact model
    belongs to~\(O(n^2)\). In~the second~case, the~complexity of bounding
    models still belongs to~\(O(n\cdot \sqrt{n})\) whereas the complexity of
    the exact model belongs to~\(O(n^3)\). Furthermore, having a family of
    bounding models allows to choose the bounding model depending on the
    parameters of the exact model. The numerical results show the interest of
    our approach w.r.t. complexity and accuracy of the bound.}
}
@inproceedings{ACDFR-msr09,
  address = {Nantes, France},
  month = nov,
  year = 2009,
  number = {7-9},
  volume = {43},
  series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {Herm{\`e}s},
  editor = {Lime, Didier and Roux, Olivier H.},
  acronym = {{MSR}'09},
  booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'09)},
  author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and 
		De{ }Smet, Olivier and Fribourg, Laurent and Ruel, Silvain},
  title = {Synth{\`e}se de contraintes temporis{\'e}es pour
		une architecture d'automatisation en r{\'e}seau},
  pages = {1049-1064},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
  abstract = {We deal with the problem of synthesis of timing constraints for
    concurrent systems. Such systems are modeled by networks of timed automata
    where some constants, represented as parameters, can be tuned. A suitable
    value of these parameters is assumed to be known from a preliminarily
    simulation process. We present a method which infers a zone of suitable
    points around this reference functioning point. This zone is defined by a
    system of linear inequalities over the parameters. This method is applied
    to the case study of a networked automation system.}
}
@inproceedings{ABC-cav09,
  address = {Grenoble, France},
  month = jun # {-} # jul,
  year = 2009,
  volume = 5643,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bouajjani, Ahmad and Maler, Oded},
  acronym = {{CAV}'09},
  booktitle = {{P}roceedings of the 21st
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'09)},
  author = {Abadi, Mart{\'\i}n and Blanchet, Bruno and Comon{-}Lundh,
                  Hubert},
  title = {Models and Proofs of Protocol Security: A~Progress Report},
  pages = {35-49},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf},
  doi = {10.1007/978-3-642-02658-4_5},
  abstract = {This paper discusses progress in the verification of security
                  protocols. Focusing on a small, classic example, it stresses
                  the use of program-like representations of protocols, and
                  their automatic analysis in symbolic and computational
                  models.}
}
@inproceedings{CDL-adhs09,
  address = {Zaragoza, Spain},
  month = sep,
  year = 2009,
  editor = {Giua, Alessandro and Silva, Manuel and Zaytoon, Janan},
  acronym = {{ADHS}'09},
  booktitle = {{P}roceedings of the 3rd {IFAC} {C}onference on {A}nalysis and
                  {D}esign of {H}ybrid {S}ystems ({ADHS}'09)},
  author = {Chatain, {\relax Th}omas and David, Alexandre and Larsen, Kim
                  G.},
  title = {Playing Games with Timed Games},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
  abstract = {In this paper we focus on property-preserving preorders between
    timed game automata and their application to control of partially
    observable systems. Following the example of timed simulation between
    timed automata, we define timed alternating simulation as a preorder
    between timed game automata, which preserves controllability. We define a
    method to reduce the timed alternating simulation problem to a safety
    game. We show how timed alternating simulation can be used to control
    efficiently a partially observable system. This method is illustrated by a
    generic case study.}
}
@inproceedings{BHK-rp09,
  address = {Palaiseau, France},
  month = sep,
  year = 2009,
  volume = 5797,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bournez, Olivier and Potapov, Igor},
  acronym = {{RP}'09},
  booktitle = {{P}roceedings of the 3rd {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'09)},
  author = {Boichut, Yohan and H{\'e}am,
                  Pierre-Cyrille and Kouchnarenko, Olga},
  title = {How to Tackle Integer Weighted Automata Positivity},
  pages = {79-92},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf},
  doi = {10.1007/978-3-642-04420-5_9},
  abstract = {This paper is dedicated to candidate abstractions to capture
                  relevant aspects of the integer weighted automata. The
                  expected effect of applying these abstractions is studied to
                  build the deterministic reachability graphs allowing us to
                  semi-decide the positivity problem on these automata.
                  Moreover, the papers reports on the implementations and
                  experimental results, and discusses other encodings.}
}
@article{BCHK-ijfcs09,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Boichut, Yohan and Courbis, Rom{\'e}o and H{\'e}am,
                  Pierre-Cyrille and Kouchnarenko, Olga},
  title = {Handling Non-left Linear Rules when Completing Tree Automata},
  volume = 20,
  number = 5,
  pages = {837-849},
  year = 2009,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf},
  doi = {10.1142/S0129054109006917},
  abstract = {This paper addresses the following general problem of tree
    regular model-checking: decide whether \(\mathcal{R}^*(\mathcal{L}) \cap
    \mathcal{L}_p = \emptyset\) where \(\mathcal{R}^*\) is the reflexive and
    transitive closure of a successor relation induced by a term rewriting
    system~\(\mathcal{R}\), and \(\mathcal{L}\) and~\(\mathcal{L}_p\) are both
    regular tree languages. We~develop an automatic approximation-based
    technique to handle this---undecidable in general---problem in the case
    when term rewriting system rules are non left-linear.}
}
@article{BDL-apal09,
  publisher = {Elsevier Science Publishers},
  journal = {Annals of Pure and Applied Logics},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes,
                  {\'E}tienne},
  title = {Reasoning about sequences of memory states},
  volume = {161},
  number = {3},
  pages = {305-323},
  year = 2009,
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
  doi = {10.1016/j.apal.2009.07.004},
  abstract = {Motivated by the verification of programs with pointer
    variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
    underlying assertion language is the quantifier-free fragment of
    separation logic and the temporal logic on the top of it is the standard
    linear-time temporal logic LTL. We analyze the complexity of various
    model-checking and satisfiability problems for LTL\textsuperscript{mem},
    considering various fragments of separation logic (including pointer
    arithmetic), various classes of models (with or without constant heap),
    and the influence of fixing the initial memory state. We provide a
    complete picture based on these criteria. Our main decidability result is
    pspace-completeness of the satisfiability problems on the record fragment
    and on a classical fragment allowing pointer arithmetic.
    \(\Sigma_1^0\)-completeness or \(\Sigma_1^1\)-completeness results are
    established for various problems by reducing standard problems for Minsky
    machines, and underline the tightness of our decidability results.}
}
@inproceedings{BCDL-formats09,
  address = {Budapest, Hungary},
  month = sep,
  year = 2009,
  volume = 5813,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
  acronym = {{FORMATS}'09},
  booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'09)},
  author = {Bulychev, Peter and Chatain, {\relax Th}omas and David,
                  Alexandre and Larsen, Kim G.},
  title = {Checking simulation relation between timed game automata},
  pages = {73-87},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
  doi = {10.1007/978-3-642-04368-0_8},
  abstract = {In this paper we focus on property-preserving preorders between
                  timed game automata and their application to control of
                  partially observable systems. We define timed weak
                  alternating simulation as a preorder between timed game
                  automata, which preserves controllability. We define the
                  rules of building a symbolic turn-based two-player game such
                  that the existence of a winning strategy is equivalent to
                  the simulation being satisfied. We also propose an
                  on-the-fly algorithm for solving this game. This simulation
                  checking method can be applied to the case of
                  non-alternating or strong simulations as well. We illustrate
                  our algorithm by a case study and report on results.}
}
@inproceedings{HP-qest09,
  address = {Budapest, Hungary},
  month = sep,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'09},
  booktitle = {{P}roceedings of the 6th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'09)},
  author = {Haddad, Serge and Pekergin, Nihal},
  title = {Using Stochastic Comparison for Efficient
		Model Checking of Uncertain {M}arkov Chains},
  pages = {177-186},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
  doi = {10.1109/QEST.2009.42},
  abstract = {We consider model checking of Discrete Time Markov Chains~(DTMC)
    with transition probabilities which are not exactly known but lie in a
    given interval. Model checking a Probabilistic Computation Tree
    Logic~(PCTL) formula for interval-valued DTMCs~(IMC) has been shown to be
    NP hard and co-NP hard. Since the state space of a realistic DTMC is
    generally huge, these lower bounds prevent the application of exact
    algorithms for such models. Therefore we propose to apply the stochastic
    comparison method to check an extended version of PCTL for IMCs. More
    precisely, we first design linear time algorithms to quantitatively
    analyze IMCs. Then we develop an efficient, semi-decidable PCTL model
    checking procedure for IMCs. Furthermore, our procedure returns more
    refined answers than traditional ones: YES, NO, DON'T~KNOW. Thus we may
    provide useful partial information for modelers in the {"}DON'T~KNOW{"}
    case.}
}
@inproceedings{CFLS-esorics09,
  address = {Saint~Malo, France},
  month = sep,
  year = 2009,
  volume = 5789,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Backes, Michael and Ning, Peng},
  acronym = {{ESORICS}'09},
  booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
		{R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
  author = {Centenaro, Matteo and Focardi, Riccardo and 
		 Luccio, Flaminia L. and Steel, Graham},
  title = {Type-based Analysis of {PIN} Processing {API}s},
  pages = {53-68},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
  doi = {10.1007/978-3-642-04444-1_4},
  abstract = {We examine some known attacks on the PIN verification framework,
    based on weaknesses of the security API for the tamper-resistant Hardware
    Security Modules used in the network. We specify this API in an imperative
    language with cryptographic primitives, and show how its flaws are
    captured by a notion of robustness that extends the one of Myers,
    Sabelfeld and Zdancewic to our cryptographic setting. We~propose an
    improved API, give an extended type system for assuring integrity and for
    preserving confidentiality via randomized and non-randomized encryptions,
    and show our new API to be type-checkable.}
}
@inproceedings{CS-esorics09,
  address = {Saint~Malo, France},
  month = sep,
  year = 2009,
  volume = 5789,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Backes, Michael and Ning, Peng},
  acronym = {{ESORICS}'09},
  booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
		{R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
  author = {Cortier, V{\'e}ronique and Steel, Graham},
  title = {A~generic security {API} for symmetric key management on
                  cryptographic devices},
  pages = {605-620},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
  doi = {10.1007/978-3-642-04444-1_37},
  abstract = {Security APIs are used to define the boundary between trusted
    and untrusted code. The security properties of existing APIs are not
    always clear. In~this paper, we~give a new generic API for managing
    symmetric keys on a trusted cryptographic device. We state and prove
    security properties for our API. In~particular, our API offers a high
    level of security even when the host machine is controlled by an attacker.
    Our API is generic in the sense that it can implement a wide variety of
    (symmetric~key) protocols. As a proof of concept, we give an algorithm for
    automatically instantiating the API commands for a given key management
    protocol. We demonstrate the algorithm on a set of key establishment
    protocols from the Clark-Jacob suite.}
}
@article{CAM-jcss09,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Cautis, Bogdan and Abiteboul, Serge and Milo, Tova},
  title = {Reasoning about {XML} update constraints},
  month = sep,
  year = 2009,
  volume = 75,
  number = 6,
  pages = {336-358},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf},
  doi = {10.1016/j.jcss.2009.02.001},
  abstract = {We introduce in this paper a class of constraints for describing
                  how an XML document can evolve, namely \emph{XML update
                  constraints}. For these constraints, we~study the implication
                  problem, giving algorithms and complexity results for
                  constraints of varying expressive power. Besides classical
                  constraint implication, we also consider an instance-based
                  approach in which we take into account data. More precisely,
                  we study implication with respect to a current tree
                  instance, resulting from a series of unknown updates. The
                  main motivation of our work is reasoning about data
                  integrity under update restrictions in contexts where owners
                  may lose control over their data, such as in publishing or
                  exchange.}
}
@inproceedings{FS-mfcs09,
  address = {Novy Smokovec, Slovakia},
  month = aug,
  year = 2009,
  volume = 5734,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kr{\'a}lovi{\v c}, Rastislav and Niwi{\'n}ski, Damian},
  acronym = {{MFCS}'09},
  booktitle = {{P}roceedings of the 34th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'09)},
  author = {Figueira, Diego and Segoufin, Luc},
  title = {Future-looking logics on data words and trees},
  pages = {331-343},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs09.ps},
  doi = {10.1007/978-3-642-03816-7_29},
  abstract = {In a data word or a data tree each position carries a label
    from a finite alphabet and a data value from an infinite domain. These
    models have been considered in the realm of semistructured data, timed
    automata and extended temporal logics.\par
    Over data words we consider the logic 1-reg-LTL(\(\textbf{F}\)), that
    extends LTL(\(\textbf{F}\)) with one register for storing data values for
    later comparisons. We show that satisfiability over data words of
    1-reg-LTL(\(\textbf{F}\)) is already not primitive recursive. We also show
    that the extension of 1-reg-LTL(\(\textbf{F}\)) with either the reverse
    modality \(\textbf{F}^{-1}\) or with one extra register is undecidable.
    All those lower bounds were already known for
    1-reg-LTL(\(\textbf{X}\),\(\textbf{F}\)) and our results essentially show
    that the \(\textbf{X}\) modality was not necessary.\par
    Moreover we show that over data trees similar lower bounds hold for
    certain fragments of XPATH.}
}
@article{DG-jlc09,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {The Effects of Bounding Syntactic Resources on {P}resburger
                  {LTL}},
  pages = {1541-1575},
  volume = {19},
  number = {6},
  month = dec,
  year = 2009,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
  doi = {10.1093/logcom/exp037},
  abstract = {LTL over Presburger constraints is the extension of LTL where
    the atomic formulae are quantifier-free Presburger formulae having as free
    variables the counters at different states of the model. This logic is
    known to admit undecidable satisfiability and model-checking problems.
    We~study decidability and complexity issues for fragments of LTL with
    Presburger constraints obtained by restricting the syntactic resources of
    the formulae (the number of variables, the maximal distance between two
    states for which counters can be compared and, to a smaller extent, the
    set of Presburger constraints) while preserving the strength of the
    logical operators. We~provide a complete picture refining known results
    from the literature. We~show that model-checking and satisfiability
    problems for the fragments of LTL with difference constraints restricted
    to two variables and distance one and to one variable and distance two are
    highly undecidable, enlarging significantly the class of known undecidable
    fragments. On the positive side, we prove that the fragment restricted to
    one variable and to distance one augmented with propositional variables is
    \textsc{pspace}-complete. Since the atomic formulae can state quantitative
    properties on the counters, this extends some results about model-checking
    pushdown systems and one-counter automata. In~order to establish the
    pspace upper bound, we show that the nonemptiness problem for B{\"u}chi
    one-counter automata taking values in~\(\mathbb{Z}\) and allowing zero
    tests and sign tests, is~only \textsc{nlogspace}-complete. Finally,
    we~establish that model-checking one-counter automata with complete
    quantifier-free Presburger LTL restricted to one variable is also
    \textsc{pspace}-complete whereas the satisfiability problem is
    undecidable.}
}
@inproceedings{KAS-arspawits09,
  address = {York, UK},
  month = aug,
  year = 2009,
  volume = 5511,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
  acronym = {{ARSPA-WITS}'09},
  booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop
	   on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and
           {I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)},
  author = {Keighren, Gavin and Aspinall, David and Steel, Graham},
  title = {Towards a Type System for Security {API}s},
  pages = {173-192},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
  doi = {10.1007/978-3-642-03459-6_12},
  abstract = {Security API analysis typically only considers a subset of an
    API's functions, with results bounded by the number of function calls.
    Furthermore, attacks involving partial leakage of sensitive information
    are usually not covered. Type-based static analysis has the potential to
    alleviate these shortcomings. To that end, we present a type system for
    secure information flow based upon the one of Volpano, Smith and Irvine,
    extended with types for cryptographic keys and ciphertext similar to those
    in Sumii and Pierce. In~contrast to some other type systems, the
    encryption and decryption of keys does not require special treatment. We
    show that a well-typed sequence of commands is non-interferent, based upon
    a definition of indistinguishability where, in certain circumstances, the
    adversary can distinguish between ciphertexts that correspond to encrypted
    public data.}
}
@inproceedings{FS-arspawits09,
  address = {York, UK},
  month = aug,
  year = 2009,
  volume = 5511,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
  acronym = {{ARSPA-WITS}'09},
  booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop
	   on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and
           {I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)},
  author = {Fr{\"o}schle, Sibylle and Steel, Graham},
  title = {Analysing {PKCS}\#11 Key Management {API}s with Unbounded
                  Fresh Data},
  pages = {92-106},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
  doi = {10.1007/978-3-642-03459-6_7},
  abstract = {We extend Delaune, Kremer and Steel's framework for analysis of
    PKCS#11-based APIs from bounded to unbounded fresh data. We achieve this
    by: formally defining the notion of an \emph{attribute policy}; showing
    that a well-designed API should have a certain class of policy we call
    \emph{complete}; showing that APIs with complete policies may be safely
    abstracted to APIs where the attributes are fixed; and proving that these
    \emph{static} APIs can be analysed in a small bounded model such that
    security properties will hold for the unbounded case. We automate analysis
    in our framework using the SAT-based security protocol model checker
    SATMC. We show that a symmetric key management subset of the Eracom
    PKCS#11 API, used in their ProtectServer product, preserves the secrecy of
    sensitive keys for unbounded numbers of fresh keys and \emph{handles},
    i.e.~pointers to keys. We also show that this API is not robust: if~an
    encryption key is lost to the intruder, SATMC finds an attack whereby all
    the keys may be compromised.}
}
@inproceedings{CDK-secret09,
  address = {Port Jefferson, New~York, USA},
  month = jul,
  year = 2009,
  editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
  acronym = {{SecReT}'09},
  booktitle = {{P}reliminary {P}roceedings of the 4th 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'09)},
  author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and
		 Kremer, Steve},
  title = {Computing knowledge in security protocols under convergent
                  equational theories},
  pages = {47-58},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf},
  abstract = {We propose a procedure for the intruder deduction problem and
    for the static equivalence problem, in the case where cryptographic
    primitives are modeled by a convergent equational theory. Our~procedure
    terminates on a wide range of equational theories. In~particular,
    we~obtain a new decidability result for a theory of trapdoor commitment
    that we encountered in the study of e-voting protocols. We~also provide a
    prototype implementation.}
}
@inproceedings{ACD-secret09,
  address = {Port Jefferson, New~York, USA},
  month = jul,
  year = 2009,
  editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
  acronym = {{SecReT}'09},
  booktitle = {{P}reliminary {P}roceedings of the 4th 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'09)},
  author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and
		Delaune, St{\'e}phanie},
  title = {Modeling and Verifying Ad Hoc Routing Protocol},
  pages = {33-46},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACD-secret09.ps},
  abstract = {Mobile ad hoc networks consist of mobile wireless devices which
    autonomously organize their infrastructure. In~such a network, a~central
    issue, ensured by routing protocols, is to find a route from one device to
    another. Those protocols use cryptographic mechanisms in order to prevent
    a malicious node from compromising the discovered route.\par
    We present a calculus for modeling and reasoning about security protocols,
    including in particular secured routing protocols. Our calculus extends
    standard symbolic models to take into account the characteristics of
    routing protocols and to model wireless communication in a more accurate
    way. Then, by using constraint solving techniques, we propose a decision
    procedure for analyzing routing protocols for a bounded number of sessions
    and for a fixed network topology. We~demonstrate the usage and usefulness
    of our approach by analyzing the protocol SRP applied to~DSR.}
}
@inproceedings{KMT-secret09,
  address = {Port Jefferson, New~York, USA},
  month = jul,
  year = 2009,
  editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
  acronym = {{SecReT}'09},
  booktitle = {{P}reliminary {P}roceedings of the 4th 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'09)},
  author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
  title = {Reducing Equational Theories for the Decision of Static
                  Equivalence (Preliminary Version)},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-secret09.ps},
  abstract = {Static equivalence is a well established notion of
    indistinguishability of sequences of terms which is useful in the symbolic
    analysis of cryptographic protocols. Static equivalence modulo equational
    theories allows a more accurate representation of cryptographic primitives
    by modelling properties of operators by equational axioms. We develop a
    method that allows in some cases to simplify the task of deciding static
    equivalence in a multi-sorted setting, by removing a symbol from the term
    signature and reducing the problem to several simpler equational theories.
    We illustrate our technique at hand of bilinear pairings.}
}
@article{ACEF-ijfcs09,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
                  Encrenaz, Emmanuelle and Fribourg, Laurent},
  title = {An Inverse Method for Parametric Timed Automata},
  volume = 20,
  number = 5,
  pages = {819-836},
  month = oct,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
  doi = {10.1142/S0129054109006905},
  abstract = {We consider in this paper systems modeled by timed automata. The
    timing bounds involved in the action guards and location invariants of our
    timed automata are not constants, but parameters. Those parametric timed
    automata allow the modelling of various kinds of timed systems,
    \textit{e.g.} communication protocols or asynchronous circuits. We will
    also assume that we are given an initial tuple~\(\pi_0\) of values for the
    parameters, which corresponds to values for which the system is known to
    behave properly. Our goal is to compute a constraint~\(K_0\) on the
    parameters, satisfied by~\(\pi_0\), guaranteeing that, under any parameter
    valuation satisfying~\(K_0\), the system behaves in the same manner: for any
    two parameter valuations satisfying~\(K_0\), the behaviors of the timed
    automata are (time-abstract) equivalent, \textit{i.e.}, the traces of execution
    viewed as alternating sequences of actions and locations are identical. We
    present an algorithm \texttt{InverseMethod} that terminates in the case of acyclic
    models, and discuss how to extend it in the cyclic case. We also explain
    how to combine our method with classical synthesis methods which are based
    on the avoidance of a given set of bad states. A prototype implementation
    has been done, and various experiments are described.}
}
@techreport{LSV:09:09,
  author = {Goubault{-}Larrecq, Jean},
  title = {On a Generalization of a Result by {V}alk and {J}antzen},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = may,
  type = {Research Report},
  number = {LSV-09-09},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
  note = {18~pages},
  abstract = {We~show that, under mild assumptions on the effective, well
    quasi-ordered set~\(X\), one~can compute a finite basis of an
    upward-closed subset~\(U\) of~\(X\) if and only if one can decide whether
    \(U \cap \downarrow z\) is empty for every \(z \in \widehat{X}\). Here
    \(\widehat{X}\) is the completion of \(X\) as defined in Finkel and
    Goubault-Larrecq, {\em Forward Analysis for WSTS, Part~{I:} Completions},
    STACS'09, pages 433-444, 2009. This generalizes a useful result proved by
    Valk and Jantzen in~1985, which is the case \(X = \\mathbb{N}^k\).}
}
@inproceedings{RBH-formats09,
  address = {Budapest, Hungary},
  month = sep,
  year = 2009,
  volume = 5813,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
  acronym = {{FORMATS}'09},
  booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'09)},
  author = {Bouillard, Anne and Haar, Stefan and Rosario, Sidney},
  title = {Critical paths in the Partial Order Unfolding of a
                 Stochastic {P}etri Net},
  pages = {43-57},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
  doi = {10.1007/978-3-642-04368-0_6},
  abstract = {In concurrent real-time processes, the speed of individual
                  components has a double impact: on the one hand, the overall
                  latency of a compound process is affected by the latency of
                  its components. But, if the composition has race conditions,
                  the very outcome of the process will also depend on the
                  latency of component processes. Using stochastic Petri nets,
                  we investigate the probability of a transition occurrence
                  being critical for the entire process, i.e. such that a
                  small increase or decrease of the duration of the occurrence
                  entails an increase or decrease of the total duration of the
                  process. The first stage of the analysis focuses on
                  occurrence nets, as obtained by partial order unfoldings, to
                  determine criticality of events; we then lift to workflow
                  nets to investigate criticality of transitions inside a
                  workflow.}
}
@inproceedings{LA-ictac09,
  address = {Kuala Lumpur, Malaysia},
  month = aug,
  year = 2009,
  volume = 5684,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Leucker, Martin and Morgan, Carroll},
  acronym = {{ICTAC}'09},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on
	{T}heoretical {A}spects of {C}omputing ({ICTAC}'09)},
  author = {Longuet, Delphine and Aiguier, Marc},
  title = {Integration Testing from Structured First-Order
                  Specifications via Deduction Modulo},
  pages = {261-276},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf},
  doi = {10.1007/978-3-642-03466-4_17},
  abstract = {Testing from first-order specifications has mainly been studied
    for flat specifications, that are specifications of a single software
    module. However, the specifications of large software systems are
    generally built out of small specifications of individual modules, by
    enriching their union. The aim of integration testing is to test the
    composition of modules assuming that they have previously been verified,
    i.e. assuming their correctness. One of the main method for the selection
    of test cases from first-order specifications, called axiom unfolding, is
    based on a proof search for the different instances of the property to be
    tested, thus allowing the coverage of this property. The idea here is to
    use deduction modulo as a proof system for structured first-order
    specifications in the context of integration testing, so as to take
    advantage of the knowledge of the correctness of the individual modules.}
}
@inproceedings{andre-ictac09,
  address = {Kuala Lumpur, Malaysia},
  month = aug,
  year = 2009,
  volume = 5684,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Leucker, Martin and Morgan, Carroll},
  acronym = {{ICTAC}'09},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on
	{T}heoretical {A}spects of {C}omputing ({ICTAC}'09)},
  author = {Andr{\'e}, {\'E}tienne},
  title = {{IMITATOR}: A~Tool for Synthesizing Constraints on Timing
                  Bounds of Timed Automata},
  pages = {336-342},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf},
  doi = {10.1007/978-3-642-03466-4_22},
  abstract = {We present here Imitator, a tool for synthesizing constraints on
    timing bounds (seen as parameters) in the framework of timed automata.
    Unlike classical synthesis methods, we take advantage of a given reference
    valuation of the parameters for which the system is known to behave
    properly. Our aim is to generate a constraint such that, under any
    valuation satisfying this constraint, the system is guaranteed to behave,
    in terms of alternating sequences of locations and actions, as under the
    reference valuation. This is useful for safely relaxing some values of the
    reference valuation, and optimizing timing bounds of the system. We have
    successfully applied our tool to various examples of asynchronous circuits
    and protocols.}
}
@inproceedings{BRBH-atpn09,
  address = {Paris, France},
  month = jun,
  year = 2009,
  volume = 5606,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Franceschinis, Giuliana and Wolf, Karsten},
  acronym = {{PETRI~NETS}'09},
  booktitle = {{P}roceedings of the 30th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'09)},
  author = {Bouillard, Anne and Rosario, Sidney and
		 Benveniste, Albert and Haar, Stefan},
  title = {Monotonicity in Service Orchestrations},
  pages = {263-282},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
  doi = {10.1007/978-3-642-02424-5_16},
  abstract = {Web Service orchestrations are compositions of different Web
    Services to form a new service. The services called during the orchestration
    guarantee a given performance to the orchestrater, usually in the form of
    contracts.\par
    These contracts can be used by the orchestrater to deduce the contract it
    can offer to its own clients, by performing contract composition. An
    implicit assumption in contract based QoS management is: {"}the better the
    component services perform, the better the orchestration's performance
    will~be{"}. Thus, contract based QoS management for Web services
    orchestrations implicitly assumes monotony.\par
    In some orchestrations, however, monotony can be violated, i.e., the
    performance of the orchestration improves when the performance of a
    component service degrades. This is highly undesirable since it can render
    the process of contract composition inconsistent.\par
    In this paper we define monotony for orchestrations modelled by Colored
    Occurrence Nets (CO-nets) and we characterize the classes of monotonic
    orchestrations. We show that few orchestrations are indeed monotonic,
    mostly since latency can be traded for quality of data. We also propose a
    sound refinement of monotony, called \emph{conditional monotony}, which
    forbids this kind of cheating and show that conditional monotony is widely
    satisfied by orchestrations. This finding leads to reconsidering the way
    SLAs should be formulated.}
}
@inproceedings{BDMR-concur09,
  address = {Bologna, Italy},
  month = sep,
  year = 2009,
  volume = 5710,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bravetti, Mario and Zavattaro, Gianluigi},
  acronym = {{CONCUR}'09},
  booktitle = {{P}roceedings of the 20th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'09)},
  author = {Bouyer, Patricia and Duflot, Marie and Markey, Nicolas and
                  Renault, Gabriel},
  title = {Measuring Permissivity in Finite Games},
  pages = {196-210},
  doi = {10.1007/978-3-642-04081-8_14},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
  abstract = {In this paper, we extend the classical notion of strategies in
    turn-based finite games by allowing several moves to be selected.
    We~define and study a quantitative measure for permissivity of such
    strategies by assigning penalties when blocking transitions. We~prove that
    for reachability objectives, most permissive strategies exist, can be
    chosen memoryless, and can be computed in polynomial time, while it is in
    \(\textsf{NP}\cap\textsf{coNP}\) for discounted and mean penalties.}
}
@incollection{EFH-tsmaai09,
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge},
  title = {Interop{\'e}rabilit{\'e} des syst{\`e}mes multi-agents 
		{\`a} l'aide des services web},
  booktitle = {Technologies des syst{\`e}mes multi-agents et 
		 applications industrielles},
  editor = {El~Fallah Seghrouchni, Amal and Briot, Jean-Pierre},
  publisher = {Herm{\`e}s},
  year = 2009,
  month = apr,
  pages = {77-99},
  chapter = 3,
  url = {http://www.lavoisier.fr/notice/fr2746217850.html},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  futureisbn = {}
}
@inproceedings{HKPPT-acc09,
  address = {Saint Louis, Missouri, USA},
  month = jun,
  year = 2009,
  acronym = {{ACC}'09},
  booktitle = {{P}roceedings of the 28th {A}merican {C}ontrol 
	       {C}onference ({ACC}'09)},
  author = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure and 
		Pradat{-}Peyre, Jean-Fran{\c{c}}ois and Tr{\`e}ves, Nicolas},
  title = {Efficient State-Based Analysis by Introducing Bags in 
		{P}etri Nets Color Domains},
  pages = {5018-5025},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
  doi = {10.1109/ACC.2009.5160020},
  abstract = {The use of high-level nets, such as coloured Petri nets, is very
    convenient for modelling complex controllable systems in order to have a
    compact, readable and structured specification. However, when coming to
    the analysis phase, using too elaboratc types becomes a burden.\par
    A good trade-off between expressivene and analy is capabilities is then to
    have only imple types, which is achieved with symmetric nels. These latter
    nels enjoy the possibility of generating a symbolic reachability gralph,
    which is much smallcr than the whole state space and still allows for
    exhaustive analysis.\par
    In this paper, we extend the symmetric net model with bags on arcs. Hence,
    variables can be bags of tokens,leading to more flexible models. We show
    that symmetric nets with bags also allow for applying the symbolic
    reachability graph technique with application to deadlock detection and
    more generally for safety properties.}
}
@misc{dots-2.2,
  author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca
                  and Sznajder, Nathalie and Walukiewicz, Igor and
		  Zeitoun, Marc},
  title = {Distributed control for restricted specifications},
  howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)},
  year = 2009,
  month = mar
}
@misc{dots-1.2a,
  author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
		Lime, Didier and Markey, Nicolas},
  title = {Synthesis of timed controllers},
  howpublished = {Deliverable DOTS~1.2a (ANR-06-SETI-003)},
  year = 2009,
  month = mar
}
@article{DHS-tose09,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Software Engineering},
  author = {Donatelli, Susanna and Haddad, Serge and Sproston, Jeremy},
  title = {Model Checking Timed and Stochastic Properties with {CSL\textsuperscript{TA}}},
  volume = 35,
  number = 2,
  month = mar # {-} # apr,
  year = 2009,
  pages = {224-240},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
  doi = {10.1109/TSE.2008.108},
  abstract = {Markov chains are a well-known stochastic process that provide
    a balance between being able to adequately model the system's behavior and
    being able to afford the cost of the model solution. Systems can be
    modelled directly as Markov chains, or with a higher-level formalism for
    which Markov chains represent the underlying semantics. Markov chains are
    widely used to study the performance of computer and telecommunication
    systems. The definition of stochastic temporal logics like Continuous
    Stochastic Logic~(CSL) and its variant~asCSL, and of their model-checking
    algorithms, allows a unified approach to the verification of systems,
    allowing the mix of performance evaluation and probabilistic verification.
    \par
    In this paper we present the stochastic logic CSL\textsuperscript{TA} ,
    which is more expressive than CSL and~asCSL, and in which properties can
    be specified using automata (more precisely, timed automata with a single
    clock). The extension with respect to expressiveness allows the
    specification of properties referring to the probability of a finite
    sequence of timed events. A~typical example is the responsiveness property
    {"}with probability at least~0.75, a~message sent at time~0 by a
    system~\(A\) will be received before time~5 by system~\(B\) and the
    acknowledgment will be back at~\(A\) before time~7{"}, a property that
    cannot be expressed in either CSL or~asCSL. Furthermore, the choice of
    using automata rather than the classical temporal operators Next and Until
    should help in enlarging the accessibility of model checking to a larger
    public. We~also present a model-checking algorithm
    for~CSL\textsuperscript{TA}.}
}
@inproceedings{AFGM-tableaux09,
  address = {Oslo, Norway},
  month = jul,
  year = 2009,
  volume = 5607,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Giese, Martin and Waaler, Arild},
  acronym = {{TABLEAUX}'09},
  booktitle = {{P}roceedings of the 18th {I}nternational
               {W}orkshop on {T}heorem {P}roving with 
               {A}nalytic {T}ableaux and {R}elated {M}ethods
               ({TABLEAUX}'09)},
  author = {Areces, Carlos and Figueira, Diego and Gor{\'\i}n, Daniel
  		and Mera, Sergio},
  title = {Tableaux and Model Checking for Memory Logics},
  pages = {47-61},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AFGM-tableaux09.ps},
  doi = {10.1007/978-3-642-02716-1_5},
  abstract = {Memory logics are modal logics whose semantics is specified in
    terms of relational models enriched with additional data structure to
    represent memory. The logical language is then extended with a collection
    of operations to access and modify the data structure. In~this paper we
    study their satisfiability and the model checking problems.\par
    We first give sound and complete tableaux calculi for the memory logic
    \(ML(k,r,e)\) (the basic modal language extended with the operator \(r\) used
    to memorize a state, the operator \(e\) used to wipe out the memory, and the
    operator \(k\) used to check if the current point of evaluation is
    memorized) and some of its sublanguages. As the satisfiability problem of
    \(ML(k,r,e)\) is undecidable, the tableau calculus we present is non
    terminating. Hence, we furthermore study a variation that ensures
    termination, at the expense of completeness, and we use model checking to
    ensure soundness. Secondly, we show that the model checking problem is
    PSpace-complete.}
}
@inproceedings{DHL-mbt09,
  address = {York, UK},
  month = oct,
  year = 2009,
  number = {2},
  volume = {253},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  acronym = {{MBT}'09},
  booktitle = {{P}roceedings of the 5th Workshop on Model-Based Testing
	  ({MBT}'09)},
  author = {Dadeau, Fr{\'e}d{\'e}ric and H{\'e}am, Pierre-Cyrille and
                  Levrey, Jocelyn},
  title = {On the Use of Uniform Random Generation of Automata for Testing},
  pages = {37-51},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf},
  doi = {10.1016/j.entcs.2009.09.050 },
  abstract = {Developing efficient and automatic testing techniques is one of
    the major challenges facing software validation community. In this paper,
    we show how a uniform random generation process of finite automata,
    developed in a recent work by Bassino and Nicaud, is relevant for many
    faces of automatic testing. The main contribution is to show how to
    combine two major testing approaches: model-based testing and random
    testing. This leads to a new testing technique successfully experimented
    on a realistic case study. We also illustrate how the power of random
    testing, applied on a Chinese Postman Problem implementation, points out
    an error in a well-known algorithm. Finally, we provide some statistics on
    model-based testing algorithms.}
}
@inproceedings{CDK-cade09,
  address = {Montreal, Canada},
  month = aug,
  year = 2009,
  volume = {5663},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Schmidt, Renate},
  acronym = {{CADE}'09},
  booktitle = {{P}roceedings of the 22nd {I}nternational 
               {C}onference on {A}utomated {D}eduction
               ({CADE}'09)},
  author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and 
		Kremer, Steve},
  title = {Computing knowledge in security protocols under convergent
		 equational theories},
  pages = {355-370},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf},
  doi = {10.1007/978-3-642-02959-2_27},
  abstract = {In the symbolic analysis of security protocols, two classical
    notions of knowledge, deducibility and indistinguishability, yield
    corresponding decision problems. We~propose a procedure for both problems
    under arbitrary convergent equational theories. Our~procedure terminates
    on a wide range of equational theories. In~particular, we~obtain a new
    decidability result for a theory we encountered when studying electronic
    voting protocols. We~also provide a prototype implementation.}
}
@inproceedings{CHK-ciaa09,
  address = {Sydney, Australia},
  month = jul,
  year = 2009,
  volume = 5642,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Maneth, Sebastian},
  acronym = {{CIAA}'09},
  booktitle = {{P}roceedings of the 14th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'09)},
  author = {Courbis, Rom{\'e}o and H{\'e}am, Pierre-Cyrille and
                  Kouchnarenko, Olga},
  title = {{TAGED} Approximations for Veriying Temporal Patterns},
  pages = {135-144},
  doi = {10.1007/978-3-642-02979-0_17},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf},
  abstract = {This paper investigates the use of tree automata with global
    equalities and disequalities (TAGED for short) in reachability analysis
    over term rewriting systems (TRSs). The reachability problem being in
    general undecidable on non terminating TRSs, we provide TAGED-based
    construction, and then design approximation-based semi-decision procedures
    to model-check useful temporal patterns on infinite state rewriting
    graphs. To show that the above TAGED-based construction can be effectively
    carried out, complexity analysis for rewriting TAGED-definable languages
    is given.}
}
@inproceedings{HNS-ciaa09,
  address = {Sydney, Australia},
  month = jul,
  year = 2009,
  volume = 5642,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Maneth, Sebastian},
  acronym = {{CIAA}'09},
  booktitle = {{P}roceedings of the 14th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'09)},
  author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and Schmitz, Sylvain},
  title = {Random Generation of Deterministic Tree (Walking) Automata},
  pages = {115-124},
  doi = {10.1007/978-3-642-02979-0_15},
  url = {http://hal.inria.fr/inria-00408316},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-ciaa09.pdf},
  abstract = {Uniform random generators deliver a simple empirical means to
    estimate the average complexity of an algorithm. We present a general
    rejection algorithm that generates sequential letter-to-letter transducers
    up to isomorphism. We tailor this general scheme to randomly generate
    deterministic tree walking automata and deterministic top-down tree
    automata. We apply our implementation of the generator to the estimation
    of the average complexity of a deterministic tree walking automata to
    nondeterministic top-down tree automata construction we also implemented.}
}
@inproceedings{BG-dlt09,
  address = {Stuttgart, Germany},
  month = jun # {-} # jul,
  year = 2009,
  volume = {5583},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Diekert, Volker and Nowotka, Dirk},
  acronym = {{DLT}'09},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {D}evelopments in {L}anguage {T}heory
               ({DLT}'09)},
  author = {Bollig, Benedikt and Gastin, Paul},
  title = {Weighted versus Probabilistic Logics},
  pages = {18-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
  doi = {10.1007/978-3-642-02737-6_2},
  abstract = {While a mature theory around logics such as MSO, LTL, and CTL
    has been developed in the pure boolean setting of finite automata,
    weighted automata lack such a natural connection with (temporal) logic and
    related verification algorithms. In this paper, we will identify weighted
    versions of MSO and CTL that generalize the classical logics and even
    other quantitative extensions such as probabilistic CTL. We establish
    expressiveness results on our logics giving translations from weighted and
    probabilistic CTL into weighted MSO.}
}
@inproceedings{AGM-pods09,
  address = {Providence, Rhode Island, USA},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {ACM Press},
  editor = {Su, Jianwen},
  acronym = {{PODS}'09},
  booktitle = {{P}roceedings of the 28th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'09)},
  author = {Abiteboul, Serge and Gottlob, Georg and Manna, Marco},
  title = {Distributed {XML} Design},
  pages = {247-258},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf},
  doi = {10.1145/1559795.1559833},
  abstract = {A \emph{distributed XML document} is an XML document that spans
    several machines or Web repositories. We assume that a distribution design
    of the document tree is given, providing an XML tree some of whose leaves
    are {"}docking points{"}, to which XML subtrees can be attached. These
    subtrees may be provided and controlled by peers at remote locations, or
    may correspond to the result of function calls, e.g., Web services. If a
    global type~\(t\), e.g. a DTD, is specified for a distributed
    document~\(T\), it~would be most desirable to be able to break this type
    into a collection of local types, called a local typing, such that the
    document satisfies~\(t\) if and only if each peer (or~function) satisfies
    its local type. In this paper we lay out the fundamentals of a theory of
    local typing and provide formal definitions of three main variants of
    locality: local typing, maximal local typing, and perfect typing, the
    latter being the most desirable. We study the following relevant decision
    problems: (i)~given a typing for a design, determine whether it is local,
    maximal local, or perfect; (ii)~given a design, establish whether a
    (maximal) local, or perfect typing does exist. For some of these problems
    we provide tight complexity bounds (polynomial space), while for the
    others we show exponential upper bounds. A~main contribution is a
    polynomial-space algorithm for computing a perfect typing in this context,
    if it exists.}
}
@inproceedings{ABM-pods09,
  address = {Providence, Rhode Island, USA},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {ACM Press},
  editor = {Su, Jianwen},
  acronym = {{PODS}'09},
  booktitle = {{P}roceedings of the 28th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'09)},
  author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan},
  title = {Satisfiability and relevance for queries over active documents},
  pages = {87-96},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf},
  doi = {10.1145/1559795.1559810},
  abstract = {Many Web applications are based on dynamic interactions between
    Web components exchanging flows of information. Such a situation arises
    for instance in mashup systems or when monitoring distributed autonomous
    systems. This is a challenging problem that has generated recently a lot
    of attention; see~Web~2.0. For capturing interactions between Web
    components, we use active documents interacting with the rest of the world
    via streams of updates. Their input streams specify updates to the
    document (in the spirit of RSS feeds), whereas their output streams are
    defined by queries on the document. In most of the paper, the focus is on
    input streams where the updates are only insertions, although we do
    consider also deletions. \par
    We introduce and study two fundamental concepts in this setting, namely,
    satisfiability and relevance. Some fact is \emph{satisfiable} for an
    active document and a query if it has a chance to be in the result of the
    query in some future state. Given an active document and a query, a call
    in the document is \emph{relevant} if the data brought by this call has a
    chance to impact the answer to the query. We analyze the complexity of
    computing satisfiability in our core model (insertions only) and for
    extensions (e.g., with deletions). We also analyze the complexity of
    computing relevance in the core model.}
}
@inproceedings{BLPS-pods09,
  address = {Providence, Rhode Island, USA},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {ACM Press},
  editor = {Su, Jianwen},
  acronym = {{PODS}'09},
  booktitle = {{P}roceedings of the 28th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'09)},
  author = {Barcel{\'o}, Pablo and Libkin, Leonid and Poggi, Antonella and 
		Sirangelo, Cristina},
  title = {{XML} with Incomplete Information: Models, Properties, and
                  Query Answering},
  pages = {237-246},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf},
  doi = {10.1145/1559795.1559832},
  abstract = {We study models of incomplete information for XML, their
    computational properties, and query answering. While our approach is
    motivated by the study of relational incompleteness, incomplete
    information in XML documents may appear not only as null values but also
    as missing structural information. Our goal is to provide a classification
    of incomplete descriptions of XML documents, and separate features---or
    groups of features---that lead to hard computational problems from those
    that admit efficient algorithms. Our classification of incomplete
    information is based on the combination of null values with partial
    structural descriptions of documents. The key computational problems we
    consider are consistency of partial descriptions, representability of
    complete documents by incomplete ones, and query answering. We show how
    factors such as schema information, the presence of node ids, and missing
    structural information affect the complexity of these main computational
    problems, and find robust classes of incomplete XML descriptions that
    permit tractable query evaluation.}
}
@inproceedings{fig-pods09,
  address = {Providence, Rhode Island, USA},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {ACM Press},
  editor = {Su, Jianwen},
  acronym = {{PODS}'09},
  booktitle = {{P}roceedings of the 28th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'09)},
  author = {Figueira, Diego},
  title = {Satisfiability of Downward {XP}ath with Data Equality Tests},
  pages = {197-206},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fig-pods09.ps},
  doi = {10.1145/1559795.1559827},
  abstract = {In this work we investigate the satisfiability problem for the
    logic \(\textup{XPath}(\downarrow,\downarrow^{*},=)\), that includes all
    downward axes as well as equality and inequality tests. We address this
    problem in the absence of DTDs and the sibling axis. We prove that this
    fragment is decidable, and we nail down its complexity, showing the
    problem to be ExpTime-complete. The result also holds when path
    expressions allow closure under the Kleene star operator. To obtain these
    results, we introduce a new automaton model over data trees that captures
    \(\textup{XPath}(\downarrow,\downarrow^*,=)\) and has an ExpTime emptiness
    problem. Furthermore, we give the exact complexity of several
    downward-looking fragments. }
}
@inproceedings{PS-icalp09,
  address = {Rhodes, Greece},
  month = jul,
  year = 2009,
  volume = 5556,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and 
                  Matias, Yossi and Thomas, Wolfgang},
  acronym = {{ICALP}'09},
  booktitle = {{P}roceedings of the 36th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'09)},
  author = {Place, {\relax Th}omas and Segoufin, Luc},
  title = {A decidable characterization of Locally Testable Tree Languages},
  pages = {285-296},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf},
  doi = {10.1007/978-3-642-02930-1_24},
  abstract = {A regular tree language~\(L\) is locally testable if the
                  membership of a tree into~\(L\) depends only on the presence or
                  absence of some neighborhoods in the tree. In~this paper we
                  show that it is decidable whether a regular tree language is
                  locally testable.}
}
@inproceedings{FGL-icalp09,
  address = {Rhodes, Greece},
  month = jul,
  year = 2009,
  volume = 5556,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and 
                  Matias, Yossi and Thomas, Wolfgang},
  acronym = {{ICALP}'09},
  booktitle = {{P}roceedings of the 36th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'09)},
  author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
  title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
  pages = {188-199},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
  doi = {10.1007/978-3-642-02930-1_16},
  abstract = {We~describe a simple, conceptual forward analysis procedure for
    \(\infty\)-complete WSTS~\(\mathcal{S}\). This computes the \emph{clover}
    of a state~\(s_0\) , \textit{i.e.}, a~finite description of the closure of
    the cover of~\(s_0\) . When \(S\) is the completion of a
    WSTS~\(\mathcal{X}\), the clover in~\(\mathcal{S}\) is a finite
    description of the cover in~\(\mathcal{X}\). We~show that this applies
    exactly when \(\mathcal{X}\) is an \(\omega^2\)-WSTS, a~new robust class
    of WSTS. We~show that our procedure terminates in more cases than the
    generalized Karp-Miller procedure on extensions of Petri nets. We
    characterize the WSTS where our procedure terminates as those that are
    \emph{clover-flattable}. Finally, we~apply this to well-structured counter
    systems.}
}
@inproceedings{BBBB-icalp09,
  address = {Rhodes, Greece},
  month = jul,
  year = 2009,
  volume = 5556,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and 
                  Matias, Yossi and Thomas, Wolfgang},
  acronym = {{ICALP}'09},
  booktitle = {{P}roceedings of the 36th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'09)},
  author = {Baier, Christel and Bertrand, Nathalie and Bouyer,
		 Patricia and Brihaye, {\relax Th}omas},
  title = {When are Timed Automata Determinizable?},
  pages = {43-54},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf},
  doi = {10.1007/978-3-642-02930-1_4},
  abstract = {In this paper, we propose an abstract procedure which, given a
    timed automaton, produces a language-equivalent deterministic infinite
    timed tree. We~prove that under a certain boundedness condition, the
    infinite timed tree can be reduced into a classical deterministic timed
    automaton. The boundedness condition is satisfied by several subclasses of
    timed automata, some of them were known to be determinizable (event-clock
    timed automata, automata with integer resets), but some others were not.
    We prove for instance that strongly non-Zeno timed automata can be
    determinized. As a corollary of those constructions, we get for those
    classes the decidability of the universality and of the inclusion
    problems, and compute their complexities (the inclusion problem is for
    instance EXPSPACE-complete for strongly non-Zeno timed automata).}
}
@inproceedings{BF-icalp09,
  address = {Rhodes, Greece},
  month = jul,
  year = 2009,
  volume = 5556,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and 
                  Matias, Yossi and Thomas, Wolfgang},
  acronym = {{ICALP}'09},
  booktitle = {{P}roceedings of the 36th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'09)},
  author = {Bouyer, Patricia and Forejt, Vojt{\v e}ch},
  title = {Reachability in Stochastic Timed Games},
  pages = {103-114},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
  doi = {10.1007/978-3-642-02930-1_9},
  abstract = {We define stochastic timed games, which extend two-player timed
    games with probabilities (following a recent approach by Baier
    \textit{et~al.}), and which extend in a natural way continuous-time Markov
    decision processes. We~focus on the reachability problem for these games,
    and ask whether one of the players has a strategy to ensure that the
    probability of reaching a fixed set of states is equal~to (or~below,
    resp.~above) a~certain number~\(r\), whatever the second player does.
    We~show that the problem is undecidable in general, but that it becomes
    decidable if we restrict to single-clock 1\(\frac{1}{2}\)-player games and
    ask whether the player can ensure that the probability of reaching the set
    is~\(=1\) (or~\(>0\),~\(=0\)).}
}
@inproceedings{CD-csf09,
  address = {Port Jefferson, New York, USA},
  month = jul,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{CSF}'09},
  booktitle = {{P}roceedings of the 
               22nd {IEEE} {C}omputer {S}ecurity {F}oundations
               {S}ymposium ({CSF}'09)},
  author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  title = {A~method for proving observational equivalence},
  pages = {266-276},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf},
  doi = {10.1109/CSF.2009.9},
  abstract = {Formal methods have proved their usefulness for analyzing the
    security of protocols. Most existing results focus on trace properties
    like secrecy or authentication. There are however several security
    properties, which cannot be defined (or cannot be naturally defined) as
    trace properties and require the notion of \emph{observational
    equivalence}. Typical examples are anonymity, privacy related properties
    or statements closer to security properties used in cryptography.\par
    In this paper, we consider the applied pi calculus and we show that for
    \emph{determinate} processes, observational equivalence actually coincides
    with trace equivalence, a notion simpler to reason with. We~exhibit a
    large class of determinate processes, called \emph{simple processes}, that
    capture most existing protocols and cryptographic primitives. Then, for
    simple processes without replication, we~reduce the decidability of trace
    equivalence to deciding an equivalence relation introduced by M.~Baudet.
    Altogether, this yields the first decidability result of observational
    equivalence for a general class of equational theories.}
}
@inproceedings{CDK-forte09,
  address = {Lisbon, Portugal},
  month = jun,
  year = 2009,
  volume = {5522},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Lee, David and Lopes, Ant{\'o}nia and Poetzsch-Heffter, Arnd},
  acronym = {{FMOODS/FORTE}'09},
  booktitle = {{P}roceedings of {IFIP} {I}nternational {C}onference on {F}ormal
                  {T}echniques for {D}istributed {S}ystems ({FMOODS/FORTE}'09)},
  author = {Chadha, Rohit and Delaune, St{\'e}phanie and 
		Kremer, Steve},
  title = {Epistemic Logic for the Applied Pi Calculus},
  pages = {182-197},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/cdk-forte09.ps},
  doi = {10.1007/978-3-642-02138-1_12},
  abstract = {We propose an epistemic logic for the applied pi calculus, which
    is a variant of the pi calculus with extensions for modeling cryptographic
    protocols. In such a calculus, the security guarantees are usually stated
    as equivalences. While process calculi provide a natural means to describe
    the protocols themselves, epistemic logics are often better suited for
    expressing certain security properties such as secrecy and anonymity.\par
    We intend to bridge the gap between these two approaches: using the set of
    traces generated by a process as models, we define a logic which has
    constructs for reasoning about both intruder's epistemic knowledge and the
    set of messages in possession of the intruder. As an example we consider
    two formalizations of privacy in electronic voting and study the
    relationship between them.}
}
@inproceedings{BHKL-ijcai2009,
  address = {Pasadena, California, USA},
  month = jul,
  year = 2009,
  publisher = {AAAI Press},
  editor = {Boutilier, Craig},
  acronym = {{IJCAI}'09},
  booktitle = {{P}roceedings of the 21st {I}nternational {J}oint 
               {C}onference on {A}rtificial {I}ntelligence
               ({IJCAI}'09)},
  author = {Bollig, Benedikt and Habermehl, Peter and Kern, Carsten and
                  Leucker, Martin},
  title = {Angluin-Style Learning of~{NFA}},
  pages = {1004-1009},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
  abstract = {We introduce NL\(^{*}\), a learning algorithm for inferring
    non-deterministic finite-state automata using membership and equivalence
    queries. More specifically, residual finite-state automata (RFSA) are
    learned similarly as in Angluin's popular L\(^{*}\) algorithm, which,
    however, learns deterministic finite-state automata~(DFA). Like in a~DFA,
    the~states of an RFSA represent residual languages. Unlike a~DFA, an~RFSA
    restricts to prime residual languages, which cannot be described as the
    union of other residual languages. In~doing~so, RFSA can be exponentially
    more succinct than~DFA. They are, therefore, the preferable choice for
    many learning applications. The implementation of our algorithms is
    applied to a collection of examples and confirms the expected advantage of
    NL\(^{*}\) over L\(^{*}\).}
}
@inproceedings{BCDDH-tacas09,
  address = {York, UK},
  month = mar,
  year = 2009,
  volume = {5505},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kowalewski, Stefan and Philippou, Anna},
  acronym = {{TACAS}'09},
  booktitle = {{P}roceedings of the 15th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'09)},
  author = {Berwanger, Dietmar and Chatterjee, Krishnendu and
		 De{~}Wulf, Martin and Doyen, Laurent and 
		 Henzinger, {\relax Th}omas~A.},
  title = {Alpaga: A~Tool for Solving Parity Games with Imperfect
                  Information},
  pages = {58-61},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf},
  doi = {10.1007/978-3-642-00768-2_7},
  abstract = {Alpaga is a solver for two-player parity games with imperfect
                  information. Given the description of a game, it~determines
                  whether the first player can ensure to win and, if~so,
                  it~constructs a winning strategy. The~tool provides a
                  symbolic implementation of a recent algorithm based on
                  antichains.}
}
@inproceedings{BCL-rta09,
  address = {Bras{\'\i}lia, Brazil},
  month = jun # {-} # jul,
  year = 2009,
  volume = 5595,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Treinen, Ralf},
  acronym = {{RTA}'09},
  booktitle = {{P}roceedings of the 20th {I}nternational
               {C}onference on {R}ewriting {T}echniques
               and {A}pplications
               ({RTA}'09)},
  author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert},
  title = {Protocol security and algebraic properties: decision results
                  for a bounded number of sessions},
  pages = {133-147},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf},
  doi = {10.1007/978-3-642-02348-4_10},
  abstract = {We consider the problem of deciding the security of
    cryptographic protocols for a bounded number of sessions, taking into
    account some algebraic properties of the security primitives, for instance
    Abelian group properties. We propose a general method for deriving
    decision algorithms, splitting the task into 4 properties of the rewriting
    system describing the intruder capabilities: locality, conservativity,
    finite variant property and decidability of one-step deducibility
    constraints. We illustrate this method on a non trivial example, combining
    several Abelian Group properties, exponentiation and a homomorphism,
    showing a decidability result for this combination. }
}
@inproceedings{GJ-rta09,
  address = {Bras{\'\i}lia, Brazil},
  month = jun # {-} # jul,
  year = 2009,
  volume = 5595,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Treinen, Ralf},
  acronym = {{RTA}'09},
  booktitle = {{P}roceedings of the 20th {I}nternational
               {C}onference on {R}ewriting {T}echniques
               and {A}pplications
               ({RTA}'09)},
  author = {Godoy, Guillem and Jacquemard, Florent},
  title = {Unique Normalization for Shallow {TRS}},
  pages = {63-77},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf},
  doi = {10.1007/978-3-642-02348-4_5},
  abstract = {Computation with a term rewrite system (TRS) consists in
                  the application of its rules from a given starting
                  term until a normal form is reached, which is
                  considered the result of the computation. 
		  The unique normalization (UN) property for a TRS~\(R\) 
		  states that
                  any starting term can reach at most one normal form
                  when \(R\) is used, i.e. that the computation with R is 
		  unique.  \par
		  We study the decidability of this property
                  for classes of TRS defined by syntactic restrictions
                  such as linearity (variables can occur only once in
                  each side of the rules), flatness (sides of the
                  rules have depth at most one) and shallowness
                  (variables occur at depth at most one in the rules).\par
		  We prove that UN is decidable in polynomial time for
                  shallow and linear TRS, using tree automata
                  techniques. This result is very near to the limits
                  of decidability, since this property is known
                  undecidable even for very restricted classes like
                  right-ground TRS, flat TRS and also right-flat and
                  linear TRS.  We also show that that UN is even
                  undecidable for flat and right-linear TRS.  The
                  latter result is in contrast with the fact that many
                  other natural properties like reachability,
                  termination, confluence, weak normalization... are
                  decidable for this class of TRS.}
}
@inproceedings{BCD-rta09,
  address = {Bras{\'\i}lia, Brazil},
  month = jun # {-} # jul,
  year = 2009,
  volume = 5595,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Treinen, Ralf},
  acronym = {{RTA}'09},
  booktitle = {{P}roceedings of the 20th {I}nternational
               {C}onference on {R}ewriting {T}echniques
               and {A}pplications
               ({RTA}'09)},
  author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Delaune,
                  St{\'e}phanie},
  title = {{YAPA}: A~generic tool for computing intruder knowledge},
  pages = {148-163},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf},
  doi = {10.1007/978-3-642-02348-4_11},
  abstract = {Reasoning about the knowledge of an attacker is a necessary step
    in many formal analyses of security protocols. In the framework of the
    applied pi calculus, as in similar languages based on equational logics,
    knowledge is typically expressed by two relations: deducibility and static
    equivalence. Several decision procedures have been proposed for these
    relations under a variety of equational theories. However, each theory has
    its particular algorithm, and none has been implemented so~far.\par
    We provide a generic procedure for deducibility and static equivalence
    that takes as input any convergent rewrite system. We show that our
    algorithm covers all the existing decision procedures for convergent
    theories. We also provide an efficient implementation, and compare it
    briefly with the more general tool ProVerif.}
}
@article{BHR-fi09,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Undecidability Results for Timed Automata with Silent
		   Transitions},
  year = 2009,
  volume = 92,
  number = {1-2},
  pages = {1-25},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2007-12.ps},
  abstract = {In this work, we study decision problems related to timed
    automata with silent transitions (TA-epsilon) which strictly extend the
    expressiveness of timed automata~(TA). First, we answer negatively a
    central question raised by the introduction of silent transitions: can we
    decide whether the language recognized by a TA-epsilon can be recognized
    by some TA? Then we establish in the framework of TA-epsilon some old open
    conjectures that O.~Finkel has recently solved for~TA. Its proofs follow a
    generic scheme which relies on the fact that only a finite number of
    configurations can be reached by a TA while reading a timed word. This
    property does not hold for TA-epsilon, the proofs in the framework of
    TA-epsilon thus require more elaborated arguments. We~establish
    undecidability of complementability, minimization of the number of clocks,
    and closure under shuffle. We~also show these results in the framework of
    infinite timed languages.}
}
@techreport{LSV:09:02,
  author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert},
  title = {Protocols, insecurity decision and combination of equational theories},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = feb,
  type = {Research Report},
  number = {LSV-09-02},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf},
  note = {43~pages},
  abstract = {We consider the problem of finding attacks for a bounded number
    of sessions of security protocols. We~contribute to this field, showing
    how to decompose the problem into pieces for a class of equational
    theories, which includes the hierarchical combinations, as well as
    non-hierarchical ones. We apply this result to an electronic purse case
    study: we~show the decidability in co-NP of the insecurity problem for a
    complex equational theory mixing three Abelian groups, exponentiation and
    homomorphism properties.\par
    The main technical contributions rely on equational logic, term rewriting
    and combination of theories.}
}
@article{BS-tocl08,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Benedikt, Michael and Segoufin, Luc},
  title = {Regular tree languages definable in {FO} and in {FO}\(_{\textit{mod}}\)},
  volume = 11,
  number = 1,
  nopages = {},
  month = oct,
  year = 2009,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf},
  doi = {10.1145/1614431.1614435},
  abstract = {We~consider regular languages of labeled trees. We~give an
    effective characterization of the regular languages over such trees that
    are definable in first-order logic in the language of labeled graphs.
    These languages are the analog on trees of the {"}locally threshold
    testable{"} languages on strings. We~show that this characterization yields
    a decision procedure for determining whether a regular tree language is
    first-order definable: the~procedure is polynomial time in the minimal
    automaton presenting the regular language. We~also provide an algorithm
    for deciding whether a regular language is definable in first-order logic
    supplemented with modular quantifiers.}
}
@misc{Quasimodo-3.1,
  author = {Bouyer, Patricia and Katoen, Joost-Pieter and
		Langerak, Rom and Laroussinie, Fran{\c{c}}ois and
		Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
  title = {Transfer of correctness from models to implementation},
  howpublished = {Deliverable QUASIMODO~3.1 (ICT-FP7-STREP-214755)},
  year = 2009,
  month = jan
}
@inproceedings{JKV-lata09,
  address = {Tarragona, Spain},
  month = apr,
  year = 2009,
  volume = 5457,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dediu, Adrian Horia and Mihai Ionescu, Armand and Mart{\'\i}n-Vide, Carlos},
  acronym = {{LATA}'09},
  booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {L}anguage 
	    and {A}utomata {T}heory and {A}pplications ({LATA}'09)},
  author = {Jacquemard, Florent and Klay, Francis and Vacher, Camille},
  title = {Rigid Tree Automata},
  pages = {446-457},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf},
  doi = {10.1007/978-3-642-00982-2_38},
  abstract = {We introduce the class of Rigid Tree Automata (RTA), an
    extension of standard bottom-up automata on ranked trees with
    distinguished states called rigid. Rigid states define a restriction on
    the computation of RTA on trees: RTA can test for equality in subtrees
    reaching the same rigid state. RTA are able to perform local and global
    tests of equality between subtrees, non-linear tree pattern matching, and
    restricted disequality tests as well. Properties like determinism, pumping
    lemma, boolean closure, and several decision problems are studied in
    detail. In particular, the emptiness problem is shown decidable in linear
    time for RTA whereas membership of a given tree to the language of a given
    RTA is NP-complete. Our main result is the decidability of whether a given
    tree belongs to the rewrite closure of a RTA language under a restricted
    family of term rewriting systems, whereas this closure is not a RTA
    language. This result, one of the first on rewrite closure of languages of
    tree automata with constraints, is enabling the extension of model
    checking procedures based on finite tree automata techniques. Finally, a
    comparison of RTA with several classes of tree automata with local and
    global equality tests, and with dag automata is also provided.}
}
@phdthesis{bouyer-hab2009,
  author = {Bouyer, Patricia},
  title = {From Qualitative to Quantitative Analysis of Timed Systems},
  school = {Universit{\'e} Paris~7, Paris, France},
  type = {M{\'e}moire d'habilitation},
  year = 2009,
  month = jan,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf}
}
@incollection{GMN-pct08,
  futureaddress = {},
  month = jan,
  year = 2009,
  series = {IARCS-Universities},
  publisher = {Universities Press},
  booktitle = {Perspectives in Concurrency Theory},
  editor = {Lodaya, Kamal and Mukund, Madhavan and
		 Ramanujam, R.},
  author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title = {Reachability and boundedness in time-constrained {MSC} graphs},
  pages = {157-183},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
  abstract = {Channel boundedness is a necessary condition for a
    message-passing system to exhibit regular, finite-state behaviour at the
    global level. For Message Sequence Graphs~(MSGs), the most basic form of
    High-level Message Sequence Charts~(HMSCs), channel boundedness can be
    characterized in terms of structural conditions on the underlying graph.
    We consider MSGs enriched with timing constraints between events. These
    constraints restrict the global behaviour and can impose channel
    boundedness even when it is not guaranteed by the graph structure of the
    MSG. We~show that we can use MSGs with timing constraints to simulate
    computations of a two-counter machine. As~a consequence, even the more
    fundamental problem of reachability, which is trivial for untimed MSGs,
    becomes undecidable when we add timing constraints. Different forms of
    channel boundedness also then turn out to be undecidable, using reductions
    from the reachability problem.}
}
@incollection{BP-pct08,
  futureaddress = {},
  month = jan,
  year = 2009,
  series = {IARCS-Universities},
  publisher = {Universities Press},
  booktitle = {Perspectives in Concurrency Theory},
  editor = {Lodaya, Kamal and Mukund, Madhavan and
		 Ramanujam, R.},
  author = {Bouyer, Patricia and Petit, Antoine},
  title = {On extensions of timed automata},
  pages = {35-63},
  abstract = {Since their definition in the early nineties, timed automata have
   been one of the most used and widely studied models for
   representing and analyzing real-time systems. In their seminal
   paper, Alur and Dill proved the probably most important property
   of timed automata: checking emptiness of the language accepted by
   a timed automaton, or equivalently checking a reachability
   property in a timed automaton, is decidable. This result relies on
   the construction of the so-called region automaton, which
   abstracts behaviours of a timed automaton into behaviours of a
   finite automaton. Since then, symbolic algorithms have been
   developed to solve that problem, several model-checkers have been
   implemented, and numerous case studies have been verified.\par
   Lots of works have naturally aimed at proposing extensions of
   timed automata with new features, while preserving the
   above-mentioned fundamental decidability result. The motivation
   for these extensions is basically twofold. First it can increase the
   expressiveness of timed automata, allowing to model larger classes
   of systems. Then it can improve the conciseness (and hence the
   readability) of models by constructing more compact
   representations for a given system.\par
   In this paper, we discuss and compare some of the most important
   extensions of timed automata that have been considered in the
   literature.}
}
@inproceedings{BBL-Fossacs09,
  address = {York, UK},
  month = mar,
  year = 2009,
  volume = 5504,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {de Alfaro, Luca},
  acronym = {{FoSSaCS}'09},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'09)},
  author = {Bansal, Kshitij and Brochenin, R{\'e}mi and
		 Lozes, {\'E}tienne},
  title = {Beyond Shapes: Lists with Ordered Data},
  pages = {425-439},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf},
  doi = {10.1007/978-3-642-00596-1_30},
  abstract = {Standard analysis on recursive data structures restrict their
    attention to shape properties (for instance, a program that manipulates a
    list returns a list), excluding properties that deal with the actual
    content of these structures. For instance, these analysis would not
    establish that the result of merging two ordered lists is an ordered list.
    Separation logic, one of the prominent framework for these kind of
    analysis, proposed a heap model that could represent data, but, to our
    knowledge, no predicate dealing with data has ever been integrated to the
    logic while preserving decidability. We~establish decidability for
    (first-order) separation logic with a predicate that allows to compare two
    successive data in a list. We~then consider the extension where two data
    in arbitrary positions may be compared, and establish the undecidability
    in general. We~define a guarded fragment that turns out to be both
    decidable and sufficiently expressive to prove the preservation of the
    loop invariant of a standard program merging ordered lists. We~finally
    consider the extension with the magic-wand and prove that, by constrast
    with the data-free case, even a very restricted use of the magic wand
    already introduces undecidability.}
}
@article{GSZ-fmsd09,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
  title = {Distributed synthesis for well-connected
		 architectures},
  volume = 34,
  number = 3,
  pages = {215-237},
  month = jun,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
  doi = {10.1007/s10703-008-0064-7},
  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 output
    variables are totally ordered by their knowledge of input variables. 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{KP-secco2008,
  title = {{P}roceedings of the 6th {I}nternational {W}orkshop on
	  {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)},
  booktitle = {{P}roceedings of the 6th {I}nternational {W}orkshop on
	  {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)},
  editor = {Kremer, Steve and Panangaden, Prakash},
  publisher = {Elsevier Science Publishers},
  doi = {10.1016/j.entcs.2009.07.077},
  url = {http://www.sciencedirect.com/science/journal/15710661/242/3},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = 242,
  number = 3,
  year = 2009,
  month = aug,
  address = {Toronto, Canada}
}
@article{BCK-IC09,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer, Steve},
  title = {Computationally Sound Implementations of Equational Theories
		 against Passive Adversaries},
  year = {2009},
  month = apr,
  volume = 207,
  number = 4,
  pages = {496-520},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf},
  doi = {10.1016/j.ic.2008.12.005},
  abstract = {In~this paper we study the link between formal and cryptographic
    models for security protocols in the presence of passive adversaries.
    In~contrast to other works, we~do not consider a fixed set of primitives
    but aim at results for arbitrary equational theories. We~define a
    framework for comparing a cryptographic implementation and its
    idealization with respect to various security notions. In~particular, we
    concentrate on the computational soundness of static equivalence, a
    standard tool in cryptographic pi calculi. We~present a soundness
    criterion, which for many theories is not only sufficient but also
    necessary. Finally, to~illustrate our framework, we~establish the
    soundness of static equivalence for the exclusive OR and a theory of
    ciphers and lists.}
}
@inproceedings{BH-Fossacs09,
  address = {York, UK},
  month = mar,
  year = 2009,
  volume = 5504,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {de Alfaro, Luca},
  acronym = {{FoSSaCS}'09},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'09)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge},
  title = {Interrupt Timed Automata},
  pages = {197-211},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
  doi = {10.1007/978-3-642-00596-1_15},
  abstract = {In this work, we introduce the class of Interrupt Timed Automata
    (ITA), which are well suited to the description of multi-task systems with
    interruptions in a single processor environment. This model is a subclass
    of hybrid automata. While reachability is undecidable for hybrid automata
    we show that in ITA the reachability problem is in 2EXPSPACE and in PSPACE
    when the number of clocks is fixed, with a procedure based on a
    generalized class graph. Furthermore we consider a subclass ITA\(_{-}\)
    which still describes usual interrupt systems and for which the
    reachability problem is in NEXPTIME and in NP when the number of clocks is
    fixed (without any class graph). There exist languages accepted by an
    ITA\(_{-}\) but neither by timed automata nor by controlled real-time
    automata (CRTA), another extension of timed automata. However we
    conjecture that CRTA is not contained in ITA. So, we combine ITA with CRTA
    in a model which encompasses both classes and show that the reachability
    problem is still decidable.}
}
@inproceedings{BGH-Fossacs09,
  address = {York, UK},
  month = mar,
  year = 2009,
  volume = 5504,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {de Alfaro, Luca},
  acronym = {{FoSSaCS}'09},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'09)},
  author = {Bollig, Benedikt and Grindei, Manuela-Lidia and
	        Habermehl, Peter},
  title = {Realizability of Concurrent Recursive Programs},
  pages = {410-424},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
  doi = {10.1007/978-3-642-00596-1_29},
  abstract = {We define and study an automata model of concurrent recursive
  programs. An~automaton consists of a finite number of pushdown systems
  running in parallel and communicating via shared actions. Actually, we
  combine multi-stack visibly pushdown automata and Zielonka's asynchronous
  automata towards a model with an undecidable emptiness problem. However, a
  reasonable restriction allows us to lift Zielonka's Theorem to this
  recursive setting and permits a logical characterization in terms of a
  suitable monadic second-order logic. Building on results from Mazurkiewicz
  trace theory and work by La~Torre, Madhusudan, and Parlato, we thus develop
  a framework for the specification, synthesis, and verification of concurrent
  recursive processes.}
}
@inproceedings{FGL-stacs2009,
  address = {Freiburg, Germany},
  month = feb,
  year = 2009,
  volume = 3,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Albers, Susanne and Marion, Jean-Yves},
  acronym = {{STACS}'09},
  booktitle = {{P}roceedings of the 26th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'09)},
  author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
  title = {Forward Analysis for~{WSTS}, Part~{I}: Completions},
  pages = {433-444},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
  abstract = {Well-structured transition systems provide the right foundation
    to compute a finite basis of the set of predecessors of the upward closure
    of a state. The~dual problem, to compute a finite representation of the
    set of successors of the downward closure of a state, is~harder: Until
    now, the theoretical framework for manipulating downward-closed sets was
    missing. We~answer this problem, using insights from domain theory (dcpos
    and ideal completions), from topology (sobrifications), and shed new light
    on the notion of adequate domains of limits.}
}
@inproceedings{CGS-sofsem09,
  address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
  month = jan,
  year = 2009,
  volume = 5404,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro
                  Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma,
                  Petr and Valencia, Franck},
  acronym = {{SOFSEM}'09},
  booktitle = {{P}roceedings of the 35th International Conference on 
		Current Trends in Theory and Practice of 
		Computer Science ({SOFSEM}'09)},
  author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie},
  title = {Natural Specifications Yield Decidability for Distributed
		Synthesis of Asynchronous Systems},
  pages = {141-152},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
  doi = {10.1007/978-3-540-95891-8_16},
  abstract = {We study the synthesis problem in an asynchronous distributed
    setting: a finite set of processes interact locally with an uncontrollable
    environment and communicate with each other by sending signals---actions
    that are immediately received by the target process. The synthesis problem
    is to come up with a local strategy for each process such that the
    resulting behaviours of the system meet a given specification. We consider
    external specifications over partial orders. External means that
    specifications only relate input and output actions from and to the
    environment and not signals exchanged by processes. We also ask for some
    closure properties of the specification. We present this new setting for
    studying the distributed synthesis problem, and give decidability results:
    the non-distributed case, and the subclass of networks where communication
    happens through a strongly connected graph. We believe that this framework
    for distributed synthesis yields decidability results for many more
    architectures.}
}
@inproceedings{BDLM-lfcs09,
  address = {Deerfield Beach, Florida, USA},
  month = jan,
  year = 2009,
  volume = 5407,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  notefortitle = {6th edition of the conference},
  acronym = {{LFCS}'09},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'09)},
  author = {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and
                  Laroussinie, Fran{\c{c}}ois and 
		  Markey, Nicolas},
  title = {{ATL}~with Strategy Contexts and Bounded Memory},
  pages = {92-106},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf},
  doi = {10.1007/978-3-540-92687-0_7},
  abstract = {We extend the alternating-time temporal logics ATL 
	and ATL\textsuperscript{*} with \emph{strategy contexts} and 
	\emph{memory constraints}: the first extension make strategy 
	quantifiers to not {"}forget{"} the strategies being executed by 
	the other players. The second extension allows strategy 
	quantifiers to restrict to memoryless or bounded-memory 
	strategies.\par
	We first consider expressiveness issues. We show that our logics 
	can express important properties such as equilibria, and we 
	formally compare them with other similar formalisms (ATL, 
	ATL\textsuperscript{*}, Game Logic, Strategy Logic,~...).  
	We~then address the problem of model-checking for our logics, 
	providing a PSPACE algoritm for the sublogics involving only 
	memoryless strategies and an EXPSPACE algorithm for the 
	bounded-memory case.}
}
@inproceedings{steel-escar09,
  address = {D{\"u}sseldorf, Germany},
  month = nov,
  year = 2009,
  editor = {Paar, Christof and Wollinger, Thomas},
  acronym = {{ESCAR}'09},
  booktitle = {{P}roceedings of the 7th 
           {C}onference on {E}mbedded {S}ecurity in {C}ars
           ({ESCAR}'09)},
  author = {Steel, Graham},
  title = {Towards a Formal Analysis of the {S}e{V}e{C}o{M}~{API}},
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf}
}
@inproceedings{steel-fcc09,
  address = {Port Jefferson, New York, USA},
  month = jul,
  year = 2009,
  editor = {K{\"u}sters, Ralf},
  acronym = {{FCC}'09},
  booktitle = {{P}roceedings of the 5th {W}orkshop on {F}ormal and
		 {C}omputational {C}ryptography ({FCC}'09)},
  author = {Steel, Graham},
  title = {Computational Soundness for {API}s},
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf}
}
@inproceedings{LS-DL09,
  address = {Oxford, UK},
  month = jul,
  year = 2009,
  volume = 477,
  series = {CEUR Workshop Proceedings},
  publisher = {RWTH Aachen, Germany},
  editor = {Cuenca Grau, Bernardo and Horrocks, Ian and Motik, Boris and Sattler, Ulrike },
  acronym = {{DL}'09},
  booktitle = {{P}roceedings of the 22nd {I}nternational
           {W}orkshop {D}escription {L}ogic ({DL}'09)},
  author = {Libkin, Leonid and Sirangelo, Cristina},
  title = {Open and closed world assumptions in data exchange},
  pages = {1-6},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf}
}
@inproceedings{BFCH-dsn09,
  address = {Estoril, Portugal},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{DSN}'09},
  booktitle = {{P}roceedings of the 39th {A}nnual {IEEE}{\slash}{IFIP}
                  {I}nternational {C}onference on {D}ependable {S}ystems and
                  {N}etworks ({DSN}'09)},
  author = {Beccuti, Marco and Franceschinis, Giuliana and
                  Codetta{-}Raiteri, Daniele and Haddad, Serge},
  title = {Parametric {NdRFT} for the derivation of optimal repair
                  strategies},
  pages = {399-408},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
  doi = {10.1109/DSN.2009.5270312},
  abstract = {Non deterministic Repairable Fault Trees~(NdRFT) are a recently
    proposed modeling formalism for the study of optimal repair strategies:
    they are based on the widely adopted Fault Tree formalism, but in addition
    to the failure modes, NdRFTs allow to define possible repair actions. In a
    previous pa per the formalism has been introduced together with an
    analysis method and a tool allowing to automatically derive the best
    repair strategy to be applied in each state. The analysis technique is
    based on the generation and solution of a Markov Decision Process. In this
    paper we present an extension, ParNdRFT, that allows to exploit the
    presence of redundancy to reduce the complexity of the model and of the
    analysis. It is based on the translation of the ParNdRFT in to a Markov
    Decision Well-Formed Net, i.e. a model specified by means of an High Level
    Petri Net formalism. The translated model can be efficiently solved thanks
    to existing algorithms that generate a reduced state space automatically
    exploiting the model symmetries.}
}
@article{ASV-tods09,
  publisher = {ACM Press},
  journal = {ACM Transactions on Database Systems},
  author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor},
  title = {Static Analysis of {A}ctive {XML} Systems},
  volume = 34,
  number = 4,
  month = dec,
  year = 2009,
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf},
  doi = {10.1145/1620585.1620590},
  abstract = {Active XML is a high-level specification language tailored to
    data-intensive, distributed, dynamic Web services. Active XML is based on
    XML documents with embedded function calls. The state of a document
    evolves depending on the result of internal function calls (local
    computations) or external ones (interactions with users or other
    services). Function calls return documents that may be active, and so may
    activate new subtasks. The focus of this article is on the verification of
    temporal properties of runs of Active XML systems, specified in a
    tree-pattern-based temporal logic, Tree-LTL, which allows expressing a
    rich class of semantic properties of the application. The main results
    establish the boundary of decidability and the complexity of automatic
    verification of Tree-LTL properties.}
}
@article{BMSS-jacm09,
  publisher = {ACM Press},
  journal = {Journal of the~{ACM}},
  author = {Boja{\'n}czyk, Miko{\l}aj and Muscholl, Anca and
		Schwentick, {\relax Th}omas and Segoufin, Luc},
  title = {Two-variable logic on data trees and applications to {XML}
                  reasoning},
  volume = 56,
  number = 3,
  month = may,
  year = 2009,
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf},
  doi = {10.1145/1516512.1516515},
  abstract = {Motivated by reasoning tasks for XML languages, the
    satisfiability problem of logics on \emph{data trees} is investigated. The
    nodes of a data tree have a \emph{label} from a finite set and a
    \emph{data value} from a possibly infinite set. It is shown that
    satisfiability for two-variable first-order logic is decidable if the tree
    structure can be accessed only through the \emph{child} and the \emph{next
    sibling} predicates and the access to data values is restricted to
    equality tests. From this main result, decidability of satisfiability and
    containment for a data-aware fragment of XPath and of the implication
    problem for unary key and inclusion constraints is concluded.}
}
@article{BS-jsl09,
  publisher = {Association for Symbolic Logic},
  journal = {Journal of Symbolic Logic},
  author = {Benedikt, Michael and Segoufin, Luc},
  title = {Towards a Characterization of Order-Invariant Queries over
                  Tame Structures},
  volume = 74,
  number = 1,
  pages = {168-186},
  month = mar,
  year = 2009,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf},
  doi = {10.2178/jsl/1231082307},
  abstract = {This work deals with the expressive power of logics on finite
    graphs with access to an additional {"}arbitrary{"} linear order. The
    queries that can be expressed this way are the \emph{order-invariant
    queries} for the logic. For the standard logics used in computer science,
    such as first-order logic, it is known that access to an arbitrary linear
    order increases the expressiveness of the logic. However, when we look at
    the separating examples, we find that they have satisfying models whose
    Gaifman Graph is complex---unbounded in valence and in treewidth. We thus
    explore the expressiveness of order-invariant queries over well-behaved
    graphs. We prove that first-order order-invariant queries over strings and
    trees have no additional expressiveness over first-order logic in the
    original signature. We also prove new upper bounds on order-invariant
    queries over bounded treewidth and bounded valence graphs. Our results
    make use of a new technique of independent interest: the application of
    algebraic characterizations of definability to show collapse results.}
}
@incollection{DBBetal-CES09,
  author = {David, Alexandre and Behrmann, Gerd and Bulychev, Peter and
		Byg, Joakin and Chatain, {\relax Th}omas and Larsen, Kim G.
                  and
		Pettersson, Paul and Rasmussen, Jacob Illum and 
                Srba, Ji{\v{r}}{\'\i} and
		Yi, Wang and Joergensen, Kenneth Y. and Lime, Didier and
		Magnin, Morgan and Roux, Olivier H. and Traonouez, Louis-Marie},
  title = {Tools for Model-Checking Timed Systems},
  booktitle = {Communicating Embedded Systems~-- Software and Design},
  editor = {Jard, Claude and Roux, Olivier H.},
  publisher = {Wiley-ISTE},
  year = 2009,
  month = oct,
  pages = {165-225},
  chapter = 6,
  url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  isbn = {9781848211438}
}
@misc{avote-D21,
  nocontributor = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune,
                  St{\'e}phanie and Kremer, Steve},
  author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Cortier, V{\'e}ronique},
  title = {Algorithmes pour l'{\'e}quivalence statique},
  year = 2009,
  month = sep,
  type = {Contract Report},
  howpublished = {Deliverable AVOTE~2.1 (ANR-07-SESU-002)},
  note = {17~pages},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf}
}
@inproceedings{BBJ-iscc09,
  address = {Sousse, Tunisia},
  month = jul,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{ISCC}'09},
  booktitle = {{P}roceedings of the 14th {IEEE} {S}ymposium on {C}omputers and
		{C}ommunications ({ISCC}'09)},
  author = {Ben Youssef, Nihel and Bouhoula, Adel and Jacquemard,
		Florent},
  title = {Automatic Verification of Conformance of Firewall
		Configurations to Security Policies},
  pages = {526 - 531},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf},
  doi = {10.1109/ISCC.2009.5202309},
  abstract = {The configuration of firewalls is highly error prone and
                  automated solution are needed in order to analyze its
                  correctness. We propose a formal and automatic method for
                  checking whether a firewall reacts correctly with respect to
                  a security policy given in an high level declarative
                  language. When errors are detected, some feedback is
                  returned to the user in order to correct the firewall
                  configuration. Furthermore, the procedure verifies that no
                  conflicts exist within the security policy. We show that our
                  method is both correct and complete. Finally, it has been
                  implemented in a prototype of verifier based on a
                  satisfiability solver modulo theories (SMT). Experiment
                  conducted on relevant case studies demonstrate the
                  efficiency and scalability of the approach.}
}
@misc{averiles09-f2.2,
  author = {LIAFA and CRIL and EDF and LSV and Verimag},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F2.2~: Algorithmes de
                  v{\'e}rification~-- Rapport final},
  year = 2009,
  month = nov,
  type = {Contract Report},
  note = {25~pages},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf}
}
@inproceedings{haar-cdcccc09,
  address = {Shanghai, China},
  month = dec,
  year = 2009,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC/CCC}'09},
  booktitle = {{P}roceedings of the Joint 48th {IEEE} {C}onference on {D}ecision 
		and {C}ontrol ({CDC}'09) and 28th {C}hinese {C}ontrol {C}onference ({CCC}'09)},
  author = {Haar, Stefan},
  title = {Qualitative Diagnosability of Labeled {P}etri Nets Revisited},
  pages = {1248-1253},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
  doi = {10.1109/CDC.2009.5400917},
  abstract = {In recent years, classical discrete event fault diagnosis
    techniques have been extended to Petri Net system models under partial
    order semantics. In~a recent paper, we showed how to take further
    advantage of the partial order representation of concurrent processes, by
    decomposing the unfolding into 'facets', formed by subnets whose events
    either all occur eventually, or none of them occurs. A~notion of
    \emph{q(ualitative)}-diagnosability was proposed based on this
    decomposition. The present paper corrects the definition of
    q-diagnosability and develops its properties. Sufficient and necessary
    criteria, on the transition labeling, for q-diagnosability are shown; for
    their verification, and diagnosis itself, compact data structures are
    sufficient.}
}
@misc{Quasimodo-3.5,
  author = {Laroussinie, Fran{\c{c}}ois and Vaandrager, Frits and
                  Neuh{\"a}u{\ss}er, Martin},
  title = {Extended timed automata for scheduling},
  howpublished = {Deliverable QUASIMODO~3.5 (ICT-FP7-STREP-214755)},
  year = 2009,
  month = jul
}
@misc{Quasimodo-2.2,
  author = {Markey, Nicolas and Berendsen, Jasper
		and David, Alexandre and Han, Tingting and
		    Hermanns, Holger and Larsen, Kim G. and Neuh{\"a}u{\ss}er, Martin},
  title = {Symbolic data structures and analysis of models
		with multiple quantitative aspects},
  howpublished = {Deliverable QUASIMODO~2.2 (ICT-FP7-STREP-214755)},
  year = 2009,
  month = jul
}
@inproceedings{ABGM-time09,
  address = {Brixen-Bressanone, Italy},
  month = jul,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {Lutz, Carsten and Raskin, Jean-Fran{\c{c}}ois},
  acronym = {{TIME}'09},
  booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'09)},
  title = {The {AXML} Artifact Model},
  author = {Abiteboul, Serge and Bourhis, Pierre and Galland, Alban and
                  Marinoiu, Bogdan},
  pages = {11-17},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf},
  abstract = {Towards a data-centric workflow approach, we introduce an
    \emph{artifact model} to capture data and workflow management activities
    in distributed settings. The model is built on Active XML, \textit{i.e.},
    XML trees including Web service calls. We argue that the model captures
    the essential features of business artifacts as described informally in
    [Nigam and Caswell~(2003)] or discussed in [Hull~(2008)]. To illustrate,
    we briefly consider the \emph{monitoring} of distributed systems and the
    \emph{verification} of temporal properties for them.}
}
@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.