@article{CD-jar10, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Decidability and combination results for two notions of knowledge in security protocols}, volume = 48, number = {4}, pages = {441-487}, month = apr, year = 2012, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-jar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-jar10.pdf}, doi = {10.1007/s10817-010-9208-8}, abstract = {In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive~or,~...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties~(AC).\par In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called \emph{monoidal}) of equational theories involving AC operators.\par As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.} }

@article{KMT-jar10, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf}, title = {Reducing Equational Theories for the Decision of Static Equivalence}, year = 2012, month = feb, pages = {197-217}, number = 48, volume = 2, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KMT-jar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KMT-jar10.pdf}, doi = {10.1007/s10817-010-9203-0}, 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 for a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows us 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{CDK-jar10, publisher = {Springer}, journal = {Journal of Automated Reasoning}, 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}, year = 2012, month = feb, pages = {219-262}, number = 2, volume = 48, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-jar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-jar10.pdf}, doi = {10.1007/s10817-010-9197-7}, abstract = {The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modeled by a term algebra equipped with an equational theory axiomatizing the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems.\par We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, 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.} }

@article{FG-lmcs12, journal = {Logical Methods in Computer Science}, author = {Finkel, Alain and Goubault{-}Larrecq, Jean}, title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}}, year = 2012, month = sep, volume = 8, number = {3:28}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf}, doi = {10.2168/LMCS-8(3:28)2012}, abstract = {We describe a simple, conceptual forward analysis procedure for \(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called \emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when \(\mathfrak{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 and on lossy channel systems. We characterize the WSTS where our procedure terminates as those that are \emph{clover-flattable}. Finally, we apply this to well-structured counter systems.} }

@article{JGL-lmcs12, journal = {Logical Methods in Computer Science}, author = {Goubault{-}Larrecq, Jean}, title = {{QRB}-Domains and the Probabilistic Powerdomain}, year = 2012, volume = 8, number = {1:14}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf}, doi = {10.2168/LMCS-8(1:14)2012}, abstract = {Is there any Cartesian-closed category of continuous domains that would be closed under Jones and Plotkin's probabilistic powerdomain construction? This is a major open problem in the area of denotational semantics of probabilistic higher-order languages. We relax the question, and look for quasi-continuous dcpos instead.\par We introduce a natural class of such quasi-continuous dcpos, the omega-QRB-domains. We show that they form a category omega-QRB with pleasing properties: omega-QRB is closed under the probabilistic powerdomain functor, under finite products, under taking bilimits of expanding sequences, under retracts, and even under so-called quasi-retracts. But... omega-QRB is not Cartesian closed. We conclude by showing that the QRB domains are just one half of an FS-domain, merely lacking control.} }

@article{BGGLP-comp11, publisher = {Springer}, journal = {Computing}, author = {Bouissou, Olivier and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean and Putot, Sylvie}, title = {A Generalization of {P}-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs}, year = 2012, month = mar, volume = 94, number = {2-4}, pages = {189-201}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf}, doi = {10.1007/s00607-011-0182-8}, abstract = {We often need to deal with information that contains both interval and probabilistic uncertainties. P-boxes and Dempster-Shafer structures are models that unify both kind of information, but they suffer from the main defect of intervals, the wrapping effect. We present here a new arithmetic that mixes, in a guaranteed manner, interval uncertainty with probabilities, while using some information about variable dependencies, hence limiting the loss from not accounting for correlations. This increases the precision of the result and decreases the computation time compared to standard p-box arithmetic.} }

@inproceedings{BC-post12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7215}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua D.}, acronym = {{POST}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, author = {Bana, Gergei and Comon{-}Lundh, Hubert}, title = {Towards Unconditional Soundness: Computationally Complete Symbolic Attacker}, pages = {189-208}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf}, doi = {10.1007/978-3-642-28641-4_11}, abstract = {We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.} }

@inproceedings{CCS-post12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7215}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua D.}, acronym = {{POST}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume}, title = {Security proof with dishonest keys}, pages = {149-168}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf}, doi = {10.1007/978-3-642-28641-4_9}, abstract = {Symbolic and computational models are the two families of models for rigorously analysing security protocols. Symbolic models are abstract but offer a high level of automation while computational models are more precise but security proof can be tedious. Since the seminal work of Abadi and Rogaway, a new direction of research aims at reconciling the two views and many soundness results establish that symbolic models are actually sound w.r.t. computational models.\par This is however not true for the prominent case of encryption. Indeed, all existing soundness results assume that the adversary only uses honestly generated keys. While this assumption is acceptable in the case of asymmetric encryption, it is clearly unrealistic for symmetric encryption. In this paper, we provide with several examples of attacks that do not show-up in the classical Dolev-Yao model, and that do not break the IND-CPA nor INT-CTXT properties of the encryption scheme.\par Our main contribution is to show the first soundness result for symmetric encryption and arbitrary adversaries. We consider arbitrary indistinguishability properties and an unbounded number of sessions. This result relies on an extension of the symbolic model, while keeping standard security assumptions: IND-CPA and IND-CTXT for the encryption scheme.} }

@inproceedings{CDD-post12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7215}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua D.}, acronym = {{POST}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, author = {Cortier, V{\'e}ronique and Degrieck, Jan and Delaune, St{\'e}phanie}, title = {Analysing routing protocols: four nodes topologies are sufficient}, pages = {30-50}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post12.pdf}, doi = {10.1007/978-3-642-28641-4_3}, abstract = {Routing protocols aim at establishing a route between nodes on a network. Secured versions of routing protocols have been proposed in order to provide more guarantees on the resulting routes. Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, existing results and tools do not apply to routing protocols. This is due in particular to the fact that all possible topologies (infinitely many) have to be considered.\par In this paper, we propose a simple reduction result: when looking for attacks on properties such as the validity of the route, it is sufficient to consider topologies with only four nodes, resulting in a number of just five distinct topologies to consider. As an application, we analyse the SRP applied to DSR and the SDMSR protocols using the ProVerif tool.} }

@inproceedings{BHP-tacas12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7214}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Flanagan, Cormac and K{\"o}nig, Barbara}, acronym = {{TACAS}'12}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'12)}, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine}, title = {Coupling and Importance Sampling for Statistical Model Checking}, pages = {331-346}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf}, doi = {10.1007/978-3-642-28756-5_23}, abstract = {Statistical model-checking is an alternative verification technique applied on stochastic systems whose size is beyond numerical analysis ability. Given a model (most often a Markov chain) and a formula, it provides a confidence interval for the probability that the model satisfies the formula. One of the main limitations of the statistical approach is the computation time explosion triggered by the evaluation of very small probabilities. In order to solve this problem we develop a new approach based on importance sampling and coupling. The corresponding algorithms have been implemented in our tool cosmos. We present experimentation on several relevant systems, with estimated time reductions reaching a factor of~\(10^{120}\).} }

@inproceedings{CMV-tacas12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7214}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Flanagan, Cormac and K{\"o}nig, Barbara}, acronym = {{TACAS}'12}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'12)}, author = {Chadha, Rohit and Madhusudan, P. and Viswanathan, Mahesh}, title = {Reachability under Contextual Locking}, pages = {437-450}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CMV-tacas12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CMV-tacas12.pdf}, doi = {10.1007/978-3-642-28756-5_30}, abstract = {The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion) synchronize only using a finite set of locks. Popular programming paradigms that limit the lock usage patterns have been identified under which the pairwise reachability problem becomes decidable. In this paper, we consider a new natural programming paradigm, called contextual locking, which ties the lock usage to calling patterns in each thread: we assume that locks are released in the same context that they were acquired and that every lock acquired by a thread in a procedure call is released before the procedure returns. Our main result is that the pairwise reachability problem is polynomial-time decidable for this new programming paradigm as well.} }

@inproceedings{BCGK-fossacs12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = 7213, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Birkedal, Lars}, acronym = {{FoSSaCS}'12}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'12)}, author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.}, title = {Model Checking Languages of Data Words}, pages = {391-405}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf}, doi = {10.1007/978-3-642-28729-9_26}, abstract = {We consider the model-checking problem for data multi-pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.} }

@inproceedings{BBMU-fossacs12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = 7213, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Birkedal, Lars}, acronym = {{FoSSaCS}'12}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'12)}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {Concurrent games with ordered objectives}, pages = {301-315}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf}, doi = {10.1007/978-3-642-28729-9_20}, abstract = {We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or B{\"u}chi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).\par We study two fundamental problems in that setting: (1)~the \emph{value problem}, which aims at deciding the existence of a strategy that ensures a given payoff; (2)~the \emph{Nash equilibrium problem}, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.} }

@article{haar-deds11, publisher = {Springer}, journal = {Discrete Event Dynamic Systems: Theory and Applications}, author = {Haar, Stefan}, title = {What topology tells us about diagnosability in partial order semantics}, pages = {383-402}, volume = 22, number = 4, year = {2012}, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf}, doi = {10.1007/s10626-011-0121-z}, abstract = {From a partial observation of the behaviour of a labeled Discrete Event System, \emph{fault diagnosis} strives to determine whether or not a given {"}invisible{"} fault event has occurred. The \emph{diagnosability problem} can be stated as follows: does the labeling allow for an outside observer to determine the occurrence of the fault, no later than a bounded number of events after that unobservable occurrence? When this problem is investigated in the context of concurrent systems, partial order semantics adds to the difficulty of the problem, but also provides a richer and more complex picture of observation and diagnosis. In particular, it is crucial to clarify the intuitive notion of {"}\emph{time after fault occurrence}{"}. To this end, we will use a unifying metric framework for event structures, providing a general topological description of diagnosability in both sequential and nonsequential semantics for Petri nets.} }

@inproceedings{CD-lopstr11, address = {Odense, Denmark}, year = 2012, volume = {7225}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Vidal, Germ{\'a}n}, acronym = {{LOPSTR}'11}, booktitle = {{P}roceedings of the 21st {I}nternational {W}orkshop on {L}ogic {P}rogram {S}ynthesis and {T}ransformation ({LOPSTR}'11)}, author = {Cabalar, Pedro and Demri, St{\'e}phane}, title = {Automata-Based Computation of Temporal Equilibrium Models}, pages = {57-72}, doi = {10.1007/978-3-642-32211-2_5}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf}, abstract = {Temporal Equilibrium Logic~(TEL) is a formalism for temporal logic programming that generalizes the paradigm of Answer Set Programming~(ASP) introducing modal temporal operators from standard Linear-time Temporal Logic~(LTL). In this paper we solve some problems that remained open for TEL like decidability, bounds for computational complexity as well as computation of temporal equilibrium models for arbitrary theories. We propose a method for the latter that consists in building a B{\"u}chi automaton that accepts exactly the temporal equilibrium models of a given theory, providing an automata-based decision procedure and illustrating the \(\omega\)-regularity of such sets. We show that TEL satisfiability can be solved in exponential space and it is hard for polynomial space. Finally, given two theories, we provide a decision procedure to check if they have the same temporal equilibrium models.} }

@article{BJ-jal11, publisher = {Elsevier Science Publishers}, journal = {Journal of Applied Logic}, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Sufficient completeness verification for conditional and constrained~{TRS}}, year = {2012}, month = mar, volume = {10}, number = {1}, pages = {127-143}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-jal11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-jal11.pdf}, doi = {10.1016/j.jal.2011.09.001}, abstract = {We present a procedure for checking sufficient completeness of conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership,~...). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is integrated into a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form.\par The procedure is presented by an inference system which is shown sound and complete. A~precondition of one inference of this system refers to a (undecidable) property called strong ground reducibility which is discharged to the above inductive theorem proving system. We have successfully applied our method to several examples, yielding readable proofs and, in case of negative answer, a counter-example suggesting how to complete the specification. Moreover, we show that it is a decision procedure when the TRS is unconditional but constrained, for an expressive class of constrained constructor axioms.} }

@article{DDG-jlc11, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, author = {Demri, St{\'e}phane and D'Souza, Deepak and Gascon, R{\'e}gis}, title = {Temporal Logics of Repeating Values}, year = {2012}, month = oct, volume = 22, number = 5, pages = {1059-1096}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf}, doi = {10.1093/logcom/exr013}, abstract = {Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The paper also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.} }

@inproceedings{DDS-tosca11, address = {Saarbr{\"u}cken, Germany}, month = jan, year = 2012, volume = 6993, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {M{\"o}dersheim, Sebastian A. and Palamidessi, Catuscia}, acronym = {{TOSCA}'11}, booktitle = {{R}evised {S}elected {P}apaers of the {W}orkshop on {T}heory of {S}ecurity and {A}pplications ({TOSCA}'11)}, author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham}, title = {Formal Analysis of Privacy for Anonymous Location Based Services}, pages = {98-112}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf}, doi = {10.1007/978-3-642-27375-9_6}, abstract = {We propose a framework for formal analysis of privacy in location based services such as anonymous electronic toll collection. We give a formal definition of privacy, and apply it to the VPriv scheme for vehicular services. We analyse the resulting model using the ProVerif tool, concluding that our privacy property holds only if certain conditions are met by the implementation. Our analysis includes some novel features such as the formal modelling of privacy for a protocol that relies on interactive zero-knowledge proofs of knowledge and list permutations. } }

@inproceedings{JLTV-tosca11, address = {Saarbr{\"u}cken, Germany}, month = jan, year = 2012, volume = 6993, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {M{\"o}dersheim, Sebastian A. and Palamidessi, Catuscia}, acronym = {{TOSCA}'11}, booktitle = {{R}evised {S}elected {P}apaers of the {W}orkshop on {T}heory of {S}ecurity and {A}pplications ({TOSCA}'11)}, author = {Jacquemard, Florent and Lozes, {\'E}tienne and Treinen, Ralf and Villard, Jules}, title = {Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus}, pages = {166-185}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLTV-tosca11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLTV-tosca11.pdf}, doi = {10.1007/978-3-642-27375-9_10}, abstract = {We investigate the problem of deciding first-order theories of finite trees with several distinguished congruence relations, each of them given by some equational axioms. We give an automata-based solution for the case where the different equational axiom systems are linear and variable-disjoint (this includes the case where all axioms are ground), and where the logic does not permit to express tree relations \(x=f(y,z)\). We~show that the problem is undecidable when these restrictions are relaxed. As motivation and application, we show how to translate the model-checking problem of \(A\pi\mathcal{L}\), a~spatial equational logic for the applied pi-calculus, to the validity of first-order formulas in term algebras with multiple congruence relations.} }

@incollection{DG-iis09, author = {Demri, St{\'e}phane and Gastin, Paul}, title = {Specification and Verification using Temporal Logics}, booktitle = {Modern applications of automata theory}, editor = {D'Souza, Deepak and Shankar, Priti}, series = {IISc Research Monographs}, volume = 2, publisher = {World Scientific}, chapter = 15, pages = {457-494}, year = 2012, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf}, abstract = {This chapter illustrates two aspects of automata theory related to linear-time temporal logic LTL used for the verification of computer systems. First, we present a translation from LTL formulae to B{\"u}chi automata. The aim is to design an elementary translation which is reasonably efficient and produces small automata so that it can be easily taught and used by hand on real examples. Our translation is in the spirit of the classical tableau constructions but is optimized in several ways. Secondly, we recall how temporal operators can be defined from regular languages and we explain why adding even a single operator definable by a context-free language can lead to undecidability.} }

@inproceedings{CU-fsttcs12, address = {Hyderabad, India}, month = dec, year = 2012, volume = 18, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, acronym = {{FSTTCS}'12}, booktitle = {{P}roceedings of the 32nd {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'12)}, author = {Chadha, Rohit and Ummels, Michael}, title = {The complexity of quantitative information flow in recursive programs}, pages = {534-545}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-15.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2012.534}, abstract = {Information-theoretic measures based upon mutual information can be employed to quantify the information that an \emph{execution} of a program reveals about its \emph{secret inputs}. The \emph{information leakage bounding problem} asks whether the information leaked by a program does not exceed a certain amount. We consider this problem for two scenarios: a)~the \emph{outputs} of the program are revealed, and b)~the \emph{timing} (measured in the number of execution steps) of the program is revealed. For both scenarios, we establish complexity results in the context of deterministic boolean programs, both for programs with and without recursion. In particular, we prove that for recursive programs the information leakage bounding problem is no harder than checking reachability.} }

@inproceedings{ASV-www12comp, address = {Lyon, France}, month = apr, year = 2012, publisher = {ACM Press}, editor = {Mille, Alain and Gandon, Fabien L. and Misselis, Jacques and Rabinovich, Michael and Staab, Steffen}, acronym = {{WWW}'12}, booktitle = {{P}roceedings of the 21st {W}orld {W}ide {W}eb {C}onference ({WWW}'12)~-- {C}ompanion {V}olume}, author = {Abiteboul, Serge and Senellart, Pierre and Vianu, Victor}, title = {The {ERC} webdam on foundations of web data management}, pages = {211-214}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-www12comp.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-www12comp.pdf}, abstract = {The Webdam ERC grant is a five-year project that started in December~2008. The goal is to develop a formal model for Web data management that would open new horizons for the development of the Web in a well-principled way, enhancing its functionality, performance, and reliability. Specifically, the goal is to develop a universally accepted formal framework for describing complex and flexible interacting Web applications featuring notably data exchange, sharing, integration, querying, and updating. We also propose to develop formal foundations that will enable peers to concurrently reason about global data management activities, cooperate in solving specific tasks, and support services with desired quality of service. Although the proposal addresses fundamental issues, its goal is to serve as the basis for future software development for Web data management.} }

@inproceedings{ABD-webdb12, address = {Scottsdale, Arizona, USA}, month = may, year = 2012, editor = {Ives, Zachary G. and Velegrakis, Yannis}, acronym = {({W}eb{DB}'12)}, booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop on the {W}eb and {D}atabases ({W}eb{DB}'12)}, author = {Abiteboul, Serge and Bienvenu, Meghyn and Deutch, Daniel}, title = {Deduction in the Presence of Distribution and Contradictions}, pages = {31-36}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABD-webdb12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABD-webdb12.pdf}, abstract = {We study deduction, captured by \emph{datalog}-style rules, in the presence of contradictions, captured by \emph{functional dependency} (FD) violation. We propose a simple non-deterministic semantics for datalog with FDs based on inferring facts one at a time, never violating the FDs. We present a novel \emph{proof theory} for this semantics. We also discuss a set-at-a-time semantics, where at each iteration, all facts that can be inferred are added to the database, and then choices are made between contradicting facts. We then build upon a distributed datalog idiom, namely \emph{Webdamlog}, to define a semantics for the \emph{distributed setting}. Observe that contradictions naturally arise in such a setting, with different peers having conflicting information or opinions. We study different semantics for this setting.} }

@inproceedings{AAMS-sigmod12, address = {Scottsdale, Arizona, USA}, month = may, year = 2012, publisher = {ACM Press}, editor = {Candan, K. Sel{\c{c}}uk and Chen, Yi and Snodgrass, Richard T. and Gravano, Luis and Fuxman, Ariel}, acronym = {{SIGMOD}'12}, booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal {C}onference on {M}anagement of {D}ata ({SIGMOD}'12)}, author = {Abiteboul, Serge and Amsterdamer, Yael and Milo, Tova and Senellart, Pierre}, title = {Auto-completion learning for~{XML}}, pages = {669-672}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMS-sigmod12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMS-sigmod12.pdf}, doi = {10.1145/2213836.2213928}, abstract = {Editing an XML document manually is a complicated task. While many XML editors exist in the market, we argue that some important functionalities are missing in all of them. Our goal is to makes the editing task simpler and faster. We~present ALEX (Auto-completion Learning Editor for~XML), an editor that assists the users by providing intelligent autocompletion suggestions. These suggestions are adapted to the user needs, simply by feeding ALEX with a set of example XML documents to learn from. The~suggestions are also guaranteed to be compliant with a given XML schema, possibly including integrity constraints. To~fulfill this challenging goal, we rely on novel, theoretical foundations by us and others, which are combined here in a system for the first time.} }

@inproceedings{ABV-icdt12, address = {Berlin, Germany}, month = mar, year = 2012, publisher = {ACM Press}, editor = {Deutsch, Alin}, acronym = {{ICDT}'12}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'12)}, author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor}, title = {Highly expressive query languages for unordered data trees}, pages = {46-60}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt12.pdf}, doi = {10.1145/2274576.2274583}, abstract = {We study highly expressive query languages for unordered data trees, using as formal vehicles Active XML and extensions of languages in the while family. All languages may be seen as adding some form of control on top of a set of basic pattern queries. The results highlight the impact and interplay of different factors: the expressive power of basic queries, the embedding of computation into data (as~in Active~XML), and the use of deterministic vs. nondeterministic control. All languages are Turing complete, but not necessarily query complete in the sense of Chandra and Harel. Indeed, we show that some combinations of features yield serious limitations, analogous to \(FO^{k}\) definability in the relational context. On the other hand, the limitations come with benefits such as the existence of powerful normal forms. Other languages are {"}almost{"} complete, but fall short because of subtle limitations reminiscent of the copy elimination problem in object databases.} }

@inproceedings{AADMS-icdt12, address = {Berlin, Germany}, month = mar, year = 2012, publisher = {ACM Press}, editor = {Deutsch, Alin}, acronym = {{ICDT}'12}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'12)}, author = {Abiteboul, Serge and Amsterdamer, Yael and Deutch, Daniel and Milo, Tova and Senellart, Pierre}, title = {Finding optimal probabilistic generators for {XML} collections}, pages = {127-139}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-icdt12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-icdt12.pdf}, doi = {10.1145/2274576.2274591}, abstract = {We study the problem of, given a corpus of XML documents and its schema, finding an optimal (generative) probabilistic model, where optimality here means maximizing the likelihood of the particular corpus to be generated. Focusing first on the structure of documents, we present an efficient algorithm for finding the best generative probabilistic model, in the absence of constraints. We further study the problem in the presence of integrity constraints, namely key, inclusion, and domain constraints. We study in this case two different kinds of generators. First, we consider a continuation-test generator that performs, while generating documents, tests of schema satisfiability; these tests prevent from generating a document violating the constraints but, as we will see, they are computationally expensive. We also study a restart generator that may generate an invalid document and, when this is the case, restarts and tries again. Finally, we consider the injection of data values into the structure, to obtain a full XML document. We study different approaches for generating these values.} }

@inproceedings{AAS-icde12, address = {Washington, D.C., USA}, month = apr, year = 2012, publisher = {{IEEE} Computer Society Press}, editor = {Kementsietsidis, Anastasios and Vaz{~}Salles, Marcos Antonio}, acronym = {{ICDE}'12}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'12)}, author = {Abiteboul, Serge and Antoine, {\'E}milien and Stoyanovich, Julia}, title = {Viewing the Web as a Distributed Knowledge Base}, pages = {1-4}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAS-icde12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAS-icde12.pdf}, doi = {10.1109/ICDE.2012.150}, abstract = {This papers addresses the challenges faced by everyday Web users, who interact with inherently heterogeneous and distributed information. Managing such data is currently beyond the skills of casual users. We describe ongoing work that has as its goal the development of foundations for declarative distributed data management. In this approach, we see the Web as a knowledge base consisting of distributed logical facts and rules. Our objective is to enable automated reasoning over this knowledge base, ultimately improving the quality of service and of data. For this, we use Webdamlog, a Datalog-style language with rule delegation. We outline ongoing efforts on the WebdamExchange platform that combines Webdamlog evaluation with communication and security protocols.} }

@inproceedings{SA-dl12, address = {Rome, Italy}, month = jun, year = 2012, volume = 846, series = {CEUR Workshop Proceedings}, publisher = {RWTH Aachen, Germany}, editor = {Kazakov, Yevgeny and Lembo, Domenico and Wolter, Frank }, acronym = {{DL}'12}, booktitle = {{P}roceedings of the 2012 {I}nternational {W}orkshop {D}escription {L}ogic ({DL}'09)}, author = {Abiteboul, Serge}, title = {Viewing the Web as a Distributed Knowledge Base}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-dl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-dl12.pdf} }

@inproceedings{SA-csl12, address = {Fontainebleau, France}, month = sep, year = 2012, volume = 16, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {C{\'e}gielski, Patrick and Durand, Arnaud}, acronym = {{CSL}'12}, booktitle = {{P}roceedings of the 21st {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'12)}, author = {Abiteboul, Serge}, title = {Sharing Distributed Knowledge on the Web (Invited Talk)}, pages = {6-8}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-csl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-csl12.pdf}, doi = {10.4230/LIPIcs.CSL.2012.6}, abstract = {To share information, we propose to see the Web as a knowledge base consisting of distributed logical facts and rules. Our objective is to help Web users finding information, as well as controlling their own, using automated reasoning over this knowledge base towards improving the quality of service and of data. For this, we introduce Webdamlog, a Datalog-style language with rule delegation. We~mention the implementation of a system to support this language as well as standard communications and security protocols.} }

@article{ABV-tods12, publisher = {ACM Press}, journal = {ACM Transactions on Database Systems}, author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor}, title = {Comparing workflow specification languages: A~matter of views}, volume = 37, number = {2:10}, nopages = {}, year = 2012, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tods12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tods12.pdf}, doi = {10.1145/2188349.2188352}, abstract = {We address the problem of comparing the expressiveness of workflow specification formalisms using a notion of view of a workflow. Views allow to compare widely different workflow systems by mapping them to a common representation capturing the observables relevant to the comparison. Using this framework, we compare the expressiveness of several workflow specification mechanisms, including automata, temporal constraints, and pre-and-post conditions, with XML and relational databases as underlying data models. One surprising result shows the considerable power of static constraints to simulate apparently much richer workflow control mechanisms.} }

@article{BSS-lmcs12, journal = {Logical Methods in Computer Science}, author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Straubing, Howard}, title = {Piecewise testable tree languages}, volume = 8, number = {3:26}, nopages = {}, year = 2012, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BSS-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BSS-lmcs12.pdf}, doi = {10.2168/LMCS-8(3:26)2012}, abstract = {This paper presents a decidable characterization of tree languages that can be defined by a boolean combination of \(\Sigma_{1}\) sentences. This is a tree extension of the Simon theorem, which says that a string language can be defined by a boolean combination of \(\Sigma_{1}\) sentences if and only if its syntactic monoid is \(\mathcal{J}\)-trivial.} }

@article{AMSS-siamjc12, publisher = {SIAM}, journal = {SIAM Journal on Computing}, author = {Anderson, Matthew and van Melkebeek, Dieter and Schweikardt, Nicole and Segoufin, Luc}, title = {Locality from Circuit Lower Bounds}, volume = 41, number = 6, pages = {1481-1523}, year = {2012}, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-siamjc12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-siamjc12.pdf}, doi = {10.1137/110856873}, abstract = {We study the locality of an extension of first-order logic that captures graph queries computable in \(\textsf{AC}^{0}\), i.e., by families of polynomial-size constant-depth circuits. The extension considers first-order formulas over relational structures which may use arbitrary numerical predicates in such a way that their truth value is independent of the particular interpretation of the numerical predicates. We refer to such formulas as Arb-invariant first-order. We consider the two standard notions of locality, Gaifman and Hanf locality. Our main result gives a Gaifman locality theorem: An Arb-invariant first-order formula cannot distinguish between two tuples that have the same neighborhood up to distance \((\log n)^{c}\), where \(n\) represents the number of elements in the structure and \(c\) is a constant depending on the formula. When restricting attention to string structures, we achieve the same quantitative strength for Hanf locality. In both cases we show that our bounds are tight. We also present an application of our results to the study of regular languages. Our proof exploits the close connection between first-order formulas and the complexity class \(\textsf{AC}^{0}\) and hinges on the tight lower bounds for parity on constant-depth circuits.} }

@phdthesis{benzina-phd2012, author = {Benzina, Hedi}, title = {Enforcing Virtualized Systems Security}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2012, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-these12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-these12.pdf} }

@phdthesis{balaguer-phd2012, author = {Balaguer, Sandie}, title = {La concurrence dans les syst{\`e}mes distribu{\'e}s temps-r{\'e}el}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2012, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/balaguer-these12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/balaguer-these12.pdf} }

@book{SA-bookCDF, author = {Abiteboul, Serge}, title = {Sciences des donn{\'e}es: De la logique du premier ordre {\`a} la Toile}, publisher = {Fayard}, year = {2012}, series = {Le{\c{c}}ons inaugurales du {C}oll{\`e}ge de {F}rance} }

@techreport{rr-lsv-12-25, author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and Revol, Bertrand and Soulat, Romain}, title = {Correct-by-Design Control of 5-level and 7-level Power Converters}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = dec, type = {Research Report}, number = {LSV-12-25}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-25-v1.pdf, 20121205}, note = {8~pages}, abstract = {High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesise a correct-by-design control that guarantees that the power converter will always stay within a predened safe zone of variations for its input parameters. Our method nds local invariants by decomposing the safety space into smaller zones. The method is applied in order to synthesize correct-by-design controls for a 5-level and 7-level power converters. We check the validity of our approach by numerical simulations and physical experimentations done with a prototype built by SATIE laboratory.} }

@techreport{rr-lsv-12-24, author = {Fribourg, Laurent and Soulat, Romain}, title = {Controlled Recurrent Subspaces for Sampled Switched Linear Systems}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = dec, type = {Research Report}, number = {LSV-12-24}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-24-v1.pdf, 20121205}, note = {11~pages}, abstract = {Sampled switched linear systems are governed by piecewise linear dynamics that are periodically sampled with a given period~\(\tau\). At each sampling time, the {"}mode{"} of the system, i.e., the parameters of the linear dynamics, are switched according to a control rule. We give here a procedure for showing that a given area~\(R\) of the state space has a {"}\(k\)-recurrent decomposition: such a decomposition induces a control that makes every trajectory starting from~\(R\) go back to~\(R\) within at most \(k\) steps (i.e, \(k\tau\)\ time). We can then determine an extended zone that contains all the trajectories issued from~\(R\); this allows us to check safety properties of the system. We show the practical interest of our approach on several examples of the literature. We also give a geometrical condition on~\(R\) that ensures the existence of a \(k\)-recurrent decomposition.} }

@techreport{rr-lsv-12-23, author = {Vester, Steen}, title = {Symmetric {N}ash equilibria}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = dec, type = {Research Report}, number = {LSV-12-23}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-23.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-23.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-23-v1.pdf, 20121204}, note = {51~pages} }

@mastersthesis{m2-chretien, author = {Chr{\'e}tien, R{\'e}my}, title = {Trace equivalence of protocols for an unbounded number of sessions}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2012}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-22.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-22.pdf}, note = {30~pages}, abstract = {The problem of deciding reachability for cryptographic protocols has been thoroughly studied for an unbounded number of sessions and proven to be undecidable in general. Nevertheless some fragments were shown to be decidable, either by tagging or by restricting the number of blind-copies. On the other hand, trace equivalenc has only been proven to be decidable for a bounded number of sessions. The objective of this talk is to provide the first results of decidability of trace equivalence for an unbounded number of sessions by lifting the approach followed by Comon-Lundh and Cortier to trace equivalence.\par Trace equivalence for a first class of protocols was shown undecidable under scarce restrictions one variable and symmetric encryption are indeed enough. Consequently, we restrained our class of protocols a step further by making the protocols deterministic in some sense and preventing it from disclosing secret keys. This tighter class of protocols was then shown to be decidable after reduction to an equivalence between deterministic pushdown automata.} }

@phdthesis{brenguier-phd2012, author = {Brenguier, Romain}, title = {{\'E}quilibres de {N}ash dans les Jeux Concurrents~-- {A}pplication aux Jeux Temporis{\'e}s}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2012, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/brenguier-these12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/brenguier-these12.pdf} }

@phdthesis{cheval-phd2012, author = {Cheval, Vincent}, title = {Automatic verification of cryptographic protocols: privacy-type properties}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2012, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cheval-these12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cheval-these12.pdf} }

@article{CFM-ijfcs12, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {Bounded {P}arikh automata}, year = 2012, month = dec, volume = {23}, number = {8}, pages = {1691-1710}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf}, doi = {10.1142/S0129054112400709}, abstract = {The Parikh finite word automaton model~(PA) was introduced and studied by Klaedtke and Rue{\ss}. Here, we present some expressiveness properties of a restriction of the deterministic affine PA recently introduced, and use them as a tool to show that the bounded languages recognized by PA are the same as those recognized by deterministic PA. Moreover, this class of languages is shown equal to the class of bounded languages with a semilinear iteration set.} }

@article{CFM-rairo12, address = {Les Ulis, France}, publisher = {EDP Sciences}, journal = {RAIRO Informatique Th{\'e}orique et Applications}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {Affine {P}arikh automata}, year = 2012, month = oct, volume = 46, number = 4, pages = {511-545}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf}, doi = {10.1051/ita/2012013}, abstract = {The Parikh finite word automaton (PA) was introduced and studied in 2003 by Klaedtke and Rue\ss. Natural variants of the PA arise from viewing a PA equivalently as an automaton that keeps a count of its transitions and semilinearly constrains their numbers. Here we adopt this view and define the affine PA, that extends the PA by having each transition induce an affine transformation on the PA registers, and the PA on letters, that restricts the PA by forcing any two transitions on the same letter to affect the registers equally. Then we report on the expressiveness, closure, and decidability properties of such PA variants. We note that deterministic PA are strictly weaker than deterministic reversal-bounded counter machines.} }

@inproceedings{CFM-dlt12, address = {Taipei, Taiwan}, month = aug, year = 2012, volume = 7410, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Yen, Hsu-Chun and Ibarra, Oscar H.}, acronym = {{DLT}'12}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'12)}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {Unambiguous Constrained Automata}, pages = {239-250}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf}, doi = {10.1007/978-3-642-31653-1_22}, abstract = {The class of languages captured by Constrained Automata~(CA) that are unambiguous is shown to possess more closure properties than the provably weaker class captured by deterministic~CA. Problems decidable for deterministic CA are nonetheless shown to remain decidable for unambiguous CA, and testing for \emph{regularity} is added to this set of decidable problems. Unambiguous CA are then shown incomparable with deterministic reversal-bounded machines in terms of expressivity, and a \emph{deterministic} model equivalent to unambiguous CA is identified.} }

@article{DDMM-lmcs12, journal = {Logical Methods in Computer Science}, author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and Meyer, Roland and Morvan, {\relax Ch}ristophe}, title = {{P}etri Net Reachability Graphs: Decidability Status of {FO} Properties}, volume = 8, number = {4:9}, nopages = {}, month = oct, year = 2012, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf}, doi = {10.2168/LMCS-8(4:9)2012}, abstract = {We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.} }

@techreport{AGL-arxiv12, author = {Adj{\'e}, Assal{\'e} and Goubault{-}Larrecq, Jean}, title = {Concrete Semantics of Programs with Non-Deterministic and Random Inputs}, year = {2012}, month = oct, type = {Research Report}, institution = {Computing Research Repository}, number = {cs.LO/1210.2605}, url = {http://arxiv.org/abs/1210.2605}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGL-arxiv12.pdf}, originalpdf = {http://arxiv.org/pdf/1210.2605}, note = {19~pages}, abstract = {This document gives semantics to programs written in a C-like programming language, featuring interactions with an external environment with noisy and imprecise data.} }

@inproceedings{BHP-simul12, address = {Lisbon, Portugal}, month = nov, year = 2012, publisher = {XPS}, editor = {Dini, Petre and Lorenz, Pascal}, acronym = {{SIMUL}'12}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {A}dvances in {S}ystem {S}imulation ({SIMUL}'12)}, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine}, title = {Importance Sampling for Model Checking of Continuous Time {M}arkov Chains}, pages = {30-35}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf}, abstract = {Model checking real time properties on probabilistic systems requires computing transient probabilities on continuous time Markov chains. Beyond numerical analysis ability, a probabilistic framing can only be obtained using simulation. This statistical approach fails when directly applied to the estimation of very small probabilities. Here combining the uniformization technique and extending our previous results, we design a method which applies to continuous time Markov chains and formulas of a timed temporal logic. The corresponding algorithm has been implemented in our tool \textsc{cosmos}. We present experimentations on a relevant system, with drastic time reductions with respect to standard statistical model checking.} }

@misc{verydic-d2, author = {Iosif, Radu and Habermehl, Peter and Labbe, Sebastien and Lozes, {\'E}tienne and Yakobowski, Boris}, title = {Concurrent Programs with Simple Data Structures {{\slash}} Sequential Programs with Composite Data Structures}, howpublished = {Deliverable VERIDYC D~2 (ANR-09-SEGI-016)}, month = mar, year = {2012}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/veridyc-d2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/veridyc-d2.pdf} }

@inproceedings{LV-wsfm11, address = {Clermont-Ferrand, France}, year = 2012, volume = 7176, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Carbone, Marco and Petit, Jean-Marc}, acronym = {{WS-FM}'11}, booktitle = {{R}evised {S}elected {P}apers of the 8th {I}nternational {W}orkshop on {W}eb {S}ervices and {F}ormal {M}ethods ({WS}-{FM}'11)}, author = {Lozes, {\'E}tienne and Villard, Jules}, title = {Reliable Contracts for Unreliable Half-Duplex Communications}, pages = {2-16}, doi = {10.1007/978-3-642-29834-9_2}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-wsfm11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-wsfm11.pdf}, abstract = {Recent trends in formal models of web services description languages and session types focus on the asynchronicity of communications. In this paper, we study a core of these models that arose from our modelling of the Sing\# programming language, and demonstrate correspondences between Sing\# contracts, asynchronous session behaviors, and the subclass of communicating automata with two participants that satisfy the half-duplex property. This correspondence better explains the criteria proposed by Stengel and Bultan for Sing\# contracts to be reliable, and possibly indicate useful criteria for the design of WSDL. We moreover establish a polynomial-time complexity for the analysis of communication contracts under arbitrary models of asynchronicity, and we investigate the model-checking problems against LTL formulas.} }

@inproceedings{LL-fics12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = 77, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Miller, Dale and {\'E}sik, Zolt{\'a}n}, acronym = {{FICS}'12}, booktitle = {{P}roceedings of the 8th {W}orkshop on {F}ixed {P}oints in {C}omputer {S}cience ({FICS}'12)}, author = {Lange, Martin and Lozes, {\'E}tienne}, title = {Model-Checking the Higher-Dimensional Modal \(\mu\)-Calculus}, pages = {39-46}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fics12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fics12.pdf}, doi = {10.4204/EPTCS.77.6}, abstract = {The higher-dimensional modal \(\mu\)-calculus is an extension of the \(\mu\)-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in polynomial time, and conversely every polynomial-time decidable problem that has a bisimulation-invariant encoding into labeled transition systems can also be defined in the higher-dimensional modal \(\mu\)-calculus. We exemplify the latter connection by giving several examples of decision problems which reduce to model checking of the higher-dimensional modal \(\mu\)-calculus for some fixed formulas. This way generic model checking algorithms for the logic can then be used via partial evaluation in order to obtain algorithms for theses problems which may benefit from improvements that are well-established in the field of program verification, namely on-the-fly and symbolic techniques. The aim of this work is to extend such techniques to other fields as well, here exemplarily done for process equivalences, automata theory, parsing, string problems, and games.} }

@inproceedings{CD-lics12, address = {Dubrovnik, Croatia}, month = jun, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'12}, booktitle = {{P}roceedings of the 27th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'12)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Partial-Observation Stochastic Games: How to Win when Belief Fails}, pages = {175-184}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lics12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lics12.pdf}, doi = {10.1109/LICS.2012.28}, abstract = {We consider two-player stochastic games played on finite graphs with reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability~\(1\)), or positively (i.e., with positive probability), no matter the strategy of the second player.\par We classify such games according to the information and the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a)~player~1, or (b)~player~2 having partial observation (and the other player has perfect observation), or two-sided with (c)~both players having partial observation. On the basis of randomization, the players (a)~may not be allowed to use randomization (pure strategies), or (b)~may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c)~may use full randomization.\par Our main results for pure strategies are as follows. (1)~For one-sided games with player~1 having partial observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player~1 is EXPTIME-complete. (2)~For one-sided games with player~2 having partial observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3)~We~show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required.\par We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.} }

@article{CD-tcs12, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Energy parity games}, volume = 458, year = 2012, month = nov, pages = {49-60}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tcs12.pdf}, doi = {10.1016/j.tcs.2012.07.038}, abstract = {Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objectives. Our main results are as follows: (a)~exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b)~the~problem of deciding the winner in energy parity games can be solved in \(\textsf{NP} \cap \textsf{coNP}\); and (c)~we~give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is logspace-equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in \(\textsf{NP} \cap \textsf{coNP}\). As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.} }

@misc{impro-D4.1, author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan}, title = {Concurrent semantics for timed distributed systems}, howpublished = {Deliverable ImpRo D~4.1 (ANR-2010-BLAN-0317)}, year = 2012, month = mar, url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf} }

@misc{impro-D2.1, author = {Akshay, S. and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Haar, Stefan and Haddad, Serge and Jard, Claude and Lime, Didier and Markey, Nicolas and Reynier, Pierre-Alain and Sankur, Ocan and Thierry-Mieg, Yann}, title = {Overview of Robustness in Timed Systems}, howpublished = {Deliverable ImpRo D~2.1 (ANR-2010-BLAN-0317)}, year = 2012, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf} }

@inproceedings{KS-stm12, address = {Pisa, Italy}, month = sep, year = 2012, volume = 7783, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {J{\o}sang, Audun and Samarati, Pierangela and Petrocchi, Marinella}, acronym = {{STM}'12}, booktitle = {{R}evised {S}elected {P}apers of the 8th {W}orkshop on {S}ecurity and {T}rust {M}anagement ({STM}'12)}, author = {K{\"u}nnemann, Robert and Steel, Graham}, title = {{Y}ubi{S}ecure? Formal Security Analysis Results for the {Y}ubikey and {Y}ubi{HSM}}, pages = {257-272 }, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-stm12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-stm12.pdf}, doi = {10.1007/978-3-642-38004-4_17}, abstract = {The Yubikey is a small hardware device designed to authenticate a user against network-based services. Despite its widespread adoption (over a million devices have been shipped by Yubico to more than 20~000 customers including Google and Microsoft), the Yubikey protocols have received relatively little security analysis in the academic literature. In the first part of this paper, we give a formal model for the operation of the Yubikey one-time password (OTP) protocol. We prove security properties of the protocol for an unbounded number of fresh OTPs using a protocol analysis tool, tamarin.\par In the second part of the paper, we analyze the security of the protocol with respect to an adversary that has temporary access to the authentication server. To address this scenario, Yubico offers a small Hardware Security Module (HSM) called the YubiHSM, intended to protect keys even in the event of server compromise. We show if the same YubiHSM configuration is used both to set up Yubikeys and run the authentication protocol, then there is inevitably an attack that leaks all of the keys to the attacker. Our discovery of this attack lead to a Yubico security advisory in February 2012. For the case where separate servers are used for the two tasks, we give a configuration for which we can show using the same verification tool that if an adversary that can compromise the server running the Yubikey-protocol, but not the server used to set up new Yubikeys, then he cannot obtain the keys used to produce one-time passwords.} }

@article{BGKR-tcs12, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Berwanger, Dietmar and Gr{\"a}del, Erich and Kaiser, {\L}ukasz and Rabinovich, Roman}, title = {Entanglement and the complexity of directed graphs}, volume = 463, year = 2012, month = dec, pages = {2-25}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGKR-tcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGKR-tcs12.pdf}, doi = {10.1016/j.tcs.2012.07.010}, abstract = {Entanglement is a parameter for the complexity of finite directed graphs that measures to which extent the cycles of the graph are intertwined. It is defined by way of a game similar in spirit to the cops and robber games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width.\par Entanglement is intimately related with the computational and descriptive complexity of the modal \(\mu\)-calculus. The number of fixed-point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the \(\mu\)-calculus is strict.\par We study complexity issues for entanglement and compare it to other structural parameters of directed graphs. One of our main results is that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of subgames induced by a winning strategy.\par Furthermore, we discuss the case of graphs of entanglement two. While graphs of entanglement zero and one are very simple, graphs of entanglement two allow arbitrary nesting of cycles, and they form a sufficiently rich class for modelling relevant classes of structured systems. We provide characterisations of this class, and propose decomposition notions similar to the ones for tree width, DAG-width, and Kelly-width.} }

@inproceedings{BKL-mfcs12, address = {Bratislava, Slovakia}, month = aug, year = 2012, volume = 7464, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Rovan, Branislav and Sassone, Vladimiro and Widmayer, Peter}, acronym = {{MFCS}'12}, booktitle = {{P}roceedings of the 37th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'12)}, author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Le{\ss}enich, Simon}, title = {Solving Counter Parity Games}, pages = {160-171}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKL-mfcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKL-mfcs12.pdf}, doi = {10.1007/978-3-642-32589-2_17}, abstract = {We study a class of parity games equipped with counters that evolve according to arbitrary non-negative affine functions. These games capture several cost models for dynamic systems from the literature. We present an elementary algorithm for computing the exact value of a counter parity game, which both generalizes previous results and improves their complexity. To this end, we introduce a class of \(\omega\)-regular games with imperfect information and imperfect recall, solve them using automata-based techniques, and prove a correspondence between finite-memory strategies in such games and strategies in counter parity games.} }

@proceedings{rp2012-FLP, title = {{P}roceedings of the 6th {I}nternational {W}okshop on {R}eachability {P}roblems ({RP}'12)}, booktitle = {{P}roceedings of the 6th {I}nternational {W}okshop on {R}eachability {P}roblems ({RP}'12)}, acronym = {{RP}'12}, editor = {Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 7550, year = 2012, month = sep, address = {Bordeaux, France}, doi = {10.1007/978-3-642-33512-9}, url = {http://www.springerlink.com/content/978-3-642-33511-2/} }

@article{BDHKO-jctB12, publisher = {Elsevier Science Publishers}, journal = {Journal of Combinatorial Theory, Series~B}, author = {Berwanger, Dietmar and Dawar, Anuj and Hunter, Paul and Kreutzer, Staphan and Obdrz{\'a}lek, Jan}, title = {The {DAG}-width of directed graphs}, volume = 102, number = 4, year = 2012, month = jul, pages = {900-923}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDHKO-jctB12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDHKO-jctB12.pdf}, doi = {10.1016/j.jctb.2012.04.004}, abstract = {Tree-width is a well-known metric on undirected graphs that measures how tree-like a graph is and gives a notion of graph decomposition that proves useful in algorithm design. Tree-width can be characterised by a graph searching game where a number of cops attempt to capture a robber. We consider the natural adaptation of this game to directed graphs and show that monotone strategies in the game yield a measure, called DAG-width, that can be seen to describe how close a directed graph is to a directed acyclic graph (DAG). We also provide an associated decomposition and show how it is useful for developing algorithms on directed graphs. In particular, we show that the problem of determining the winner of a parity game is solvable in polynomial time on graphs of bounded DAG-width. We also consider the relationship between DAG-width and other connectivity measures such as directed tree-width and path-width. A consequence we obtain is that certain NP-complete problems such as Hamiltonicity and disjoint paths are polynomial-time computable on graphs of bounded DAG-width.} }

@article{FLC-rts12, publisher = {Springer}, journal = {Real-Time Systems}, author = {Faggioli, Dario and Lipari, Giuseppe and Cucinotta, Tommaso}, title = {Analysis and Implementation of the Multiprocessor Bandwidth Inheritance Protocol}, volume = {48}, number = {6}, year = {2012}, month = nov, pages = {789-825}, doi = {10.1007/s11241-012-9162-0}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLC-rts12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLC-rts12.pdf}, abstract = {The Multiprocessor Bandwidth Inheritance (M-BWI) protocol is an extension of the Bandwidth Inheritance (BWI) protocol for symmetric multiprocessor systems. Similar to Priority Inheritance, M-BWI lets a task that has locked a resource execute in the resource reservations of the blocked tasks, thus reducing their blocking time. The protocol is particularly suitable for open systems where different kinds of tasks dynamically arrive and leave, because it guarantees temporal isolation among independent subsets of tasks without requiring any information on their temporal parameters. Additionally, if the temporal parameters of the interacting tasks are known, it is possible to compute an upper bound to the interference suffered by a task due to other interacting tasks. Thus, it is possible to provide timing guarantees for a subset of interacting hard real-time tasks. Finally, the M-BWI protocol is neutral to the underlying scheduling policy: it can be implemented in global, clustered and semi-partitioned scheduling.\par After introducing the M-BWI protocol, in this paper we formally prove its isolation properties, and propose an algorithm to compute an upper bound to the interference suffered by a task. Then, we describe our implementation of the protocol for the LITMUS\textsuperscript{RT} real-time testbed, and measure its overhead. Finally, we compare M-BWI against FMLP and OMLP, two other protocols for resource sharing in multiprocessor systems.} }

@article{SLBC-rts12, publisher = {Springer}, journal = {Real-Time Systems}, author = {Santos, Rodrigo M. and Lipari, Giuseppe and Bini, Enrico and Cucinotta, Tommaso}, title = {On-line schedulability tests for adaptive reservations in fixed priority scheduling}, volume = {48}, number = {5}, year = {2012}, month = sep, pages = {601-634}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLBC-rts12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLBC-rts12.pdf}, doi = {10.1007/s11241-012-9156-y}, abstract = {Adaptive reservation is a real-time scheduling technique in which each application is associated a fraction of the computational resource (a reservation) that can be dynamically adapted to the varying requirements of the application by using appropriate feedback control algorithms. An adaptive reservation is typically implemented by using an aperiodic server (e.g. sporadic server) algorithm with fixed period and variable budget. When the feedback law demands an increase of the reservation budget, the system must run a schedulability test to check if there is enough spare bandwidth to accommodate such increase. The schedulability test must be very fast, as it may be performed at each budget update, i.e. potentially at each instance of a task; yet, it must be as efficient as possible, to maximize resource usage.\par In this paper, we tackle the problem of performing an efficient on-line schedulability test for adaptive resource reservations in fixed priority schedulers. In the literature, a number of algorithms have been proposed for on-line admission control in fixed priority systems. We describe four of these tests, with increasing complexity and performance. In addition, we propose a novel on-line test, called Spare-Pot algorithm, which has been specifically designed for the problem at hand, and which shows a good cost/performance ratio compared to the other tests.} }

@proceedings{atpn2012-HP, title = {{P}roceedings of the 33rd {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({ICATPN}'12)}, booktitle = {{P}roceedings of the 33rd {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({ICATPN}'12)}, acronym = {{ICATPN}'12}, editor = {Haddad, Serge and Pomello, Lucia}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 7347, year = 2012, month = jun, address = {Hamburg, Germany}, doi = {10.1007/978-3-642-31131-4}, url = {http://www.springer.com/978-3-642-31131-4} }

@inproceedings{FGL-pn12, address = {Hamburg, Germany}, month = jun, year = 2012, volume = 7347, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Haddad, Serge and Pomello, Lucia}, acronym = {{PETRI~NETS}'12}, booktitle = {{P}roceedings of the 33rd {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'12)}, author = {Finkel, Alain and Goubault{-}Larrecq, Jean}, title = {The~Theory of~{WSTS}: The~Case of Complete~{WSTS}}, pages = {3-31}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf}, doi = {10.1007/978-3-642-31131-4_2}, abstract = {We describe a simple, conceptual forward analysis procedure for \(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called \emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite description of the downward closure of the reachability set. We show that such completions are \(\infty\)-complete exactly when \(\mathfrak{X}\) is an \emph{\(\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 Presburger counter systems.} }

@inproceedings{BFP-fsttcs12, address = {Hyderabad, India}, month = dec, year = 2012, volume = 18, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, acronym = {{FSTTCS}'12}, booktitle = {{P}roceedings of the 32nd {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'12)}, author = {Bonnet, R{\'e}mi and Finkel, Alain and Praveen, M.}, title = {Extending the {R}ackoff technique to affine nets}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2012.301}, abstract = {We study the possibility of extending the Rackoff technique to Affine nets, which are Petri nets extended with affine functions. The Rackoff technique has been used for establishing \textsc{Expspace} upper bounds for the coverability and boundedness problems for Petri nets. We show that this technique can be extended to strongly increasing Affine nets, obtaining better upper bounds compared to known results. The possible copies between places of a strongly increasing Affine net make this extension non-trivial. One cannot expect similar results for the entire class of Affine nets since coverability is Ackermann-hard and boundedness is undecidable. Moreover, it can be proved that model checking a logic expressing generalized coverability properties is undecidable for strongly increasing Affine nets, while it is known to be \textsc{Expspace}-complete for Petri nets.} }

@article{bs-ipl12, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Berwanger, Dietmar and Serre, Olivier}, title = {Parity games on undirected graphs}, volume = 112, number = 23, year = 2012, month = dec, pages = {928-932}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bs-ipl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bs-ipl12.pdf}, doi = {10.1016/j.ipl.2012.08.021}, abstract = {We examine the complexity of solving parity games in the special case when the underlying game graph is undirected. For strictly alternating games, that is, when the game graph is bipartite between the players, we observe that the solution can be computed in linear time. In contrast, when the assumption of strict alternation is dropped, we show that the problem is as hard in the undirected case as it is in the general, directed, case.} }

@article{bbckrs-tcs12, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea and K{\"o}nig, Barbara and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan}, title = {Efficient unfolding of contextual {P}etri nets}, volume = 449, number = 1, year = 2012, month = aug, pages = {2-22}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf}, doi = {10.1016/j.tcs.2012.04.046}, abstract = {A contextual net is a Petri net extended with read arcs, which allows transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially more compact than those of a corresponding Petri net. A constructive but abstract procedure for generating those unfoldings was proposed in previous work. However, it remained unclear whether the approach was useful in practice and which data structures and algorithms would be appropriate to implement it. Here, we address this question. We provide two concrete methods for computing contextual unfoldings, with a view to efficiency. We report on experiments carried out on a number of benchmarks. These show that not only are contextual unfoldings more compact than Petri net unfoldings, but they can be computed with the same or better efficiency, in particular with respect to alternative approaches based on encodings of contextual nets into Petri nets.} }

@inproceedings{BFKSST-crypto12, address = {Santa Barbara, California, USA}, month = aug, year = 2012, volume = 7417, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Safavi-Naini, Reihaneh and Canetti, Ran}, acronym = {{CRYPTO}'12}, booktitle = {{P}roceedings of the 32nd {A}nnual {I}nternational {C}ryptology {C}onference ({CRYPTO}'12)}, author = {Bardou, Romain and Focardi, Riccardo and Kawamoto, Yusuke and Simionato, Lorenzo and Steel, Graham and Tsay, Joe-Kai}, title = {Efficient Padding Oracle Attacks on Cryptographic Hardware}, pages = {608-625}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFKSST-crypto12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFKSST-crypto12.pdf}, doi = {10.1007/978-3-642-32009-5_36}, abstract = {We show how to exploit the encrypted key import functions of a variety of different cryptographic devices to reveal the imported key. The attacks are padding oracle attacks, where error messages resulting from incorrectly padded plaintexts are used as a side channel. In the asymmetric encryption case, we modify and improve Bleichenbacher's attack on RSA PKCS\#1v1.5 padding, giving new cryptanalysis that allows us to carry out the 'million message attack' in a mean of 49 000 and median of 14 500 oracle calls in the case of cracking an unknown valid ciphertext under a 1024 bit key (the original algorithm takes a mean of 215 000 and a median of 163 000 in the same case). We show how implementation details of certain devices admit an attack that requires only 9 400 operations on average (3 800 median). For the symmetric case, we adapt Vaudenay's CBC attack, which is already highly efficient. We demonstrate the vulnerabilities on a number of commercially available cryptographic devices, including security tokens, smartcards and the Estonian electronic ID card. The attacks are efficient enough to be practical: we give timing details for all the devices found to be vulnerable, showing how our optimisations make a qualitative difference to the practicality of the attack. We give mathematical analysis of the effectiveness of the attacks, extensive empirical results, and a discussion of countermeasures.} }

@article{GS-ipl12, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Gastin, Paul and Sznajder, Nathalie}, title = {Decidability of well-connectedness for distributed synthesis}, pages = {963-968}, volume = {112}, number = {24}, month = dec, year = 2012, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf}, doi = {10.1016/j.ipl.2012.08.018}, abstract = {Although the synthesis problem is often undecidable for distributed, synchronous systems, it becomes decidable for the subclass of uniformly well-connected (UWC) architectures, provided that only robust specifications are considered. It is then an important issue to be able to decide whether a given architecture falls in this class. This is the problem addressed in this paper: we establish the decidability and precise complexity of checking this property. This problem is in EXPSPACE and NP-hard in the general case, but falls into PSPACE when restricted to a natural subclass of architectures.} }

@inproceedings{BDF-cdc12, address = {Maui, Hawaii, USA}, month = dec, year = 2012, publisher = {{IEEE} Control System Society}, acronym = {{CDC}'12}, booktitle = {{P}roceedings of the 51st {IEEE} {C}onference on {D}ecision and {C}ontrol ({CDC}'12)}, author = {Bu{\v{s}}i{\'c}, Ana and Djafri, Hilal and Fourneau, Jean-Michel}, title = {Bounded state space truncation and censored {M}arkov chains}, pages = {5828-5833}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-cdc12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-cdc12.pdf}, doi = {10.1109/CDC.2012.6426156}, abstract = {Censored Markov chains (CMC) allow to represent the conditional behavior of a system within a subset of observed states. They provide a theoretical framework to study the truncation of a discrete-time Markov chain when the generation of the state-space is too hard or when the number of states is too large. However, the stochastic matrix of a CMC may be difficult to obtain. Dayar \emph{et~al.} (2006) have proposed an algorithm, called DPY, that computes a stochastic bounding matrix for a CMC with a smaller complexity with only a partial knowledge of the chain. We prove that this algorithm is optimal for the information they take into account. We also show how some additional knowledge on the chain can improve stochastic bounds for~CMC.} }

@inproceedings{jks-ifiptcs12, address = {Amsterdam, The Netherlands}, month = sep, year = 2012, volume = {7604}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baeten, Jos and Ball, Tom and de~Boer, Frank}, acronym = {{IFIP~TCS}'12}, booktitle = {{P}roceedings of the 7th {IFIP} {I}nternational {C}onference on {T}heoretical {C}omputer {S}cience ({IFIP~TCS}'12)}, author = {Jan\v{c}ar, Petr and Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {Unidirectional channel systems can be tested}, pages = {149-163}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-ifiptcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-ifiptcs12.pdf}, doi = {10.1007/978-3-642-33475-7_11}, abstract = {{"}Unidirectional channel systems{"} (Chambart~\& Schnoebelen, CONCUR~2008) are systems where one-way communication from a sender to a receiver goes via one reliable and one unreliable (unbounded fifo) channel. Equipping these systems with the possibility of testing regular properties on the contents of channels makes verification undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on a series of reductions eventually allowing us to take advantage of recent results on Post's Embedding Problem.} }

@techreport{rr-lsv-12-16, author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and Revol, Bertrand and Soulat, Romain}, title = {Numerical simulation and physical experimentation of a 5-level and 7-level power converter under a control designed by a formal method}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = jul, type = {Research Report}, number = {LSV-12-16}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-16-v1.pdf, 20120727}, note = {18~pages}, abstract = {High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. There is no formal guarantee of correctness in zones around nominal values. In [3], we have applied a backward-oriented formal method to guarantee the good behavior of the systems within predefined zones of variations for the input parameters. Here, for numerical stability reasons, we choose to use a forward-oriented method. We apply this method to a 5-level and 7-level power converters. We check the correctness of our approach by numerical simulations and physical experimentations.} }

@article{AGG-lmcs12, journal = {Logical Methods in Computer Science}, author = {Adj{\'e}, Assal{\'e} and Gaubert, St{\'e}phane and Goubault, {\'E}ric}, title = {Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis}, year = 2012, month = jan, volume = {8}, number = {1:1}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGG-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGG-lmcs12.pdf}, doi = {10.2168/LMCS-8(1:01)2012}, abstract = {We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, generalizes the domain of linear {"}templates{"} introduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic templates, we use Shor's semi-definite relaxation to derive computable yet precise abstractions of semantic functionals, and we show that the abstract fixpoint equation can be solved accurately by coupling policy iteration and semi-definite programming. We demonstrate the interest of our approach on a series of examples (filters, integration schemes) including a degenerate one (symplectic scheme).} }

@article{Fig-lmcs12, journal = {Logical Methods in Computer Science}, author = {Figueira, Diego}, title = {Alternating register automata on finite words and trees}, year = 2012, volume = {8}, number = {1:22}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lmcs12.pdf}, doi = {10.2168/LMCS-8(1:22)2012}, abstract = {We study alternating register automata on data words and data trees in relation to logics. A data word (resp. data tree) is a word (resp. tree) whose every position carries a label from a finite alphabet and a data value from an infinite domain. We investigate one-way automata with alternating control over data words or trees, with one register for storing data and comparing them for equality. This is a continuation of the study started by Demri, Lazi{\'c} and Jurdzi{\'n}ski. From the standpoint of register automata models, this work aims at two objectives: (1)~simplifying the existent decidability proofs for the emptiness problem for alternating register automata; and (2)~exhibiting decidable extensions for these models. From the logical perspective, we show that (a)~in~the case of data words, satisfiability of LTL with one register and quantification over data values is decidable; and (b)~the~satisfiability problem for the so-called forward fragment of XPath on XML documents is decidable, even in the presence of DTDs and even of key constraints. The decidability is obtained through a reduction to the automata model introduced. This fragment contains the child, descendant, next-sibling and following-sibling axes, as well as data equality and inequality tests.} }

@article{BFLZ-lmcs12, journal = {Logical Methods in Computer Science}, author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Zeitoun, Marc}, title = {Model Checking Vector Addition Systems with one zero-test}, year = 2012, volume = {8}, number = {2:11}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf}, doi = {10.2168/LMCS-8(2:11)2012}, abstract = {We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these systems, open until now, such as place-boundedness or LTL model-checking. The proof techniques to handle the zero-test are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zero-test), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zero-test.} }

@phdthesis{lozes-HDR12, author = {Lozes, {\'E}tienne}, title = {Separation Logic: Expressiveness and Copyless Message-Passing}, year = 2012, month = jul, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-el12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-el12.pdf} }

@techreport{rr-lsv-12-14, author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and Lefebvre, St{\'e}phane and Revol, Bertrand and Soulat, Romain}, title = {Control of Multilevel Power Converters using Formal Methods}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = jun, type = {Research Report}, number = {LSV-12-14}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-14-v1.pdf, 20120626}, note = {14~pages}, abstract = {High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. There is no formal guarantee of correctness in zones around nominal values. It is therefore interesting to apply formal methods to guarantee the good behavior of the systems within predefined zones of variations for the input parameters. As far as we know, such formal methods have been applied only to small electronic power devices (like DC-DC boost converters) containing one switching cell. We show in this paper that one can apply formal methods to more complicated systems, such as multi-level converters containing several pairs of switching cells.} }

@inproceedings{GM-ciaa12, address = {Porto, Portugal}, month = jul, year = 2012, volume = {7381}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Moreira, Nelma and Reis, Rog{\'e}rio}, acronym = {{CIAA}'12}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'12)}, author = {Gastin, Paul and Monmege, Benjamin}, title = {Adding Pebbles to Weighted Automata}, pages = {28-51}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf}, doi = {10.1007/978-3-642-31606-7_4}, abstract = {We extend weighted automata and weighted rational expressions with 2-way moves and (reusable) pebbles. We show with examples from natural language modeling and quantitative model-checking that weighted expressions and automata with pebbles are more expressive and allow much more natural and intuitive specifications than classical ones.\par We extend Kleene-Sch{\"u}tzenberger theorem showing that weighted expressions and automata with pebbles have the same expressive power. We focus on an efficient translation from expressions to automata.\par We also prove that the evaluation problem for weighted automata can be done very efficiently if the number of (reusable) pebbles is low.} }

@inproceedings{BGMZ-atva12, address = {Thiruvananthapuram, India}, month = oct, year = {2012}, volume = {7561}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Mukund, Madhavan and Chakraborty, Supratik}, acronym = {{ATVA}'12}, booktitle = {{P}roceedings of the 10th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'12)}, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc}, title = {A Probabilistic {K}leene Theorem}, pages = {400-415}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf}, doi = {10.1007/978-3-642-33386-6_31}, abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata over finite words. Probabilistic automata generalize deterministic finite automata and assign to a word an acceptance probability. We provide probabilistic expressions with probabilistic choice, guarded choice, concatenation, and a star operator. We prove that probabilistic expressions and probabilistic automata are expressively equivalent. Our result actually extends to two-way probabilistic automata with pebbles and corresponding expressions.} }

@phdthesis{djafri-phd2011, author = {Djafri, Hilal}, title = {Approches num{\'e}riques et statistiques pour le model checking des processus stochastiques}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2012, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/djafri-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/djafri-these11.pdf} }

@inproceedings{CD-aiml12, address = {Copenhagen, Denmark}, month = aug, year = 2012, publisher = {College Publications}, editor = {Bolander, Thomas and Bra{\"u}ner, Torben and Ghilardi, Silvio and Moss, Lawrence}, acronym = {{AiML}'12}, booktitle = {{S}elected {P}apers from the 9th {W}orkshop on {A}dvances in {M}odal {L}ogics ({AiML}'12)}, author = {Carreiro, Facundo and Demri, St{\'e}phane}, title = {Beyond Regularity for {P}resburger Modal Logics}, pages = {161-182}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf}, abstract = {Satisfiability problem for modal logic~K with quantifier-free Presburger and regularity constraints~(EML) is known to be pspace-complete. In this paper, we consider its extension with nonregular constraints, and more specifically those expressed by visibly pushdown languages~(VPL). This class of languages behaves nicely, in particular when combined with Propositional Dynamic Logic~(PDL). By extending EML, we show that decidability is preserved if we allow at most one positive VPL-constraint at each modal depth. However, the presence of two VPL-contraints or the presence of a negative occurrence of a single VPL-constraint leads to undecidability. These results contrast with the decidability of PDL augmented with VPL-constraints.} }

@inproceedings{PHL-tap12, address = {Prague, Czech Republic}, month = may # {-} # jun, year = 2012, volume = 7305, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Brucker, Achim D. and Julliand, Jacques}, acronym = {{TAP}'12}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {T}ests and {P}roofs ({TAP}'12)}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine}, title = {Conformance Relations for Labeled Event Structures}, pages = {83-98}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf}, doi = {10.1007/978-3-642-30473-6_8}, abstract = {We propose a theoretical framework for testing concurrent systems from true concurrency models like Petri nets or networks of automata. The underlying model of computation of such formalisms are labeled event structures, which allow to represent concurrency explicitly. The activity of testing relies on the definition of a conformance relation that depends on the observable behaviors on the system under test, which is given for sequential systems by ioco type relations. However, these relations are not capable of capturing and exploiting concurrency of non sequential behavior. We~study different conformance relations for labeled event structures, relying on different notions of observation, and investigate their properties and connections.} }

@inproceedings{HSS-lics2012, address = {Dubrovnik, Croatia}, month = jun, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'12}, booktitle = {{P}roceedings of the 27th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'12)}, author = {Haddad, Serge and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {The Ordinal-Recursive Complexity of Timed-Arc {P}etri Nets, Data Nets, and Other Enriched Nets}, pages = {355-364}, url = {http://hal.archives-ouvertes.fr/hal-00793811}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lics12.pdf}, doi = {10.1109/LICS.2012.46}, abstract = {We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of the main decidable properties (safety, termination, regular simulation,~etc.) of these models. Since these new lower bounds match the upper bounds that one can derive from wqo theory, they precisely characterise the computational power of these so-called {"}enriched{"} nets.} }

@inproceedings{DDS-ijcar12, address = {Manchester, UK}, month = jun, year = 2012, volume = {7364}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli}, acronym = {{IJCAR}'12}, booktitle = {{P}roceedings of the 6th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'12)}, author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud}, title = {Taming Past {LTL} and Flat Counter Systems}, pages = {179-193}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf}, doi = {10.1007/978-3-642-31365-3_16}, abstract = {Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. Other complexity results are proved, for instance for restricted classes of flat counter systems.} }

@inproceedings{RS-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan}, title = {Verification of {P}etri Nets with Read Arcs}, pages = {471-485}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf}, doi = {10.1007/978-3-642-32940-1_33}, abstract = {Recent work studied the unfolding construction for contextual nets, i.e. nets with read arcs. Such unfoldings are more concise and can usually be constructed more efficiently than for Petri nets. However, concrete verification algorithms exploiting these advantages were lacking so far. We address this question and propose SAT-based verification algorithms for deadlock and reachability of contextual nets. Moreover, we study optimizations of the SAT encoding and report on experiments.} }

@inproceedings{CGN-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.}, title = {{MSO} Decidability of Multi-Pushdown Systems via Split-Width}, pages = {547-561}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf}, doi = {10.1007/978-3-642-32940-1_38}, abstract = {Multi-threaded programs with recursion are naturally modeled as multi-pushdown systems. The behaviors are represented as multiply nested words (MNWs), which are words enriched with additional binary relations for each stack matching a push operation with the corresponding pop operation. Any MNW can be decomposed by two basic and natural operations: shuffle of two sequences of factors and merge of consecutive factors of a sequence. We say that the split-width of a MNW is~\(k\) if it admits a decomposition where the number of factors in each sequence is at most~\(k\). The MSO theory of MNWs with split-width~\(k\) is decidable. We introduce two very general classes of MNWs that strictly generalize known decidable classes and prove their MSO decidability via their split-width and obtain comparable or better bounds of tree-width of known classes.} }

@inproceedings{BGS-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {Brenguier, Romain and G{\"o}ller, Stefan and Sankur, Ocan}, title = {A~Comparison of Succinctly Represented Finite-State Systems}, pages = {147-161}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-concur12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-concur12.pdf}, doi = {10.1007/978-3-642-32940-1_12}, abstract = {We study the succinctness of different classes of succinctly presented finite transition systems with respect to bisimulation equivalence. Our results show that synchronized product of finite automata, hierarchical graphs, and timed automata are pairwise incomparable in this sense. We moreover study the computational complexity of deciding simulation preorder and bisimulation equivalence on these classes.} }

@inproceedings{BHSS-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu and Sznajder, Nathalie}, title = {Concurrent Games on~{VASS} with Inhibition}, pages = {39-52}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf}, doi = {10.1007/978-3-642-32940-1_5}, abstract = {We propose to study concurrent games on a new extension of Vector Addition Systems with States, where inhibition conditions are added for modeling purposes. Games are a well-suited framework to solve control problems, and concurrent semantics reflect realistic situations where the environment can always produce a move before the controller, although it is never required to do so. This is in contrast with previous works, which focused mainly on turn-based semantics. Moreover, we consider asymmetric games, where environment and controller do not have the same capabilities, although they both have restricted power. In this setting, we investigate reachability and safety objectives, which are not dual to each other anymore, and we prove that (i)~reachability games are undecidable for finite targets, (ii)~they are 2-EXPTIME-complete for upward-closed targets and (iii)~safety games are co-NP-complete for finite, upward-closed and semi-linear targets. Moreover, for the decidable cases, we build a finite representation of the corresponding controllers.} }

@inproceedings{BC-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas}, title = {Avoiding Shared Clocks in Networks of Timed Automata}, pages = {100-114}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf}, doi = {10.1007/978-3-642-32940-1_9}, abstract = {Networks of timed automata~(NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA \(A_{1} \parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\), does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively build \(A'_{1} \parallel A'_{2}\) when it exists.} }

@inproceedings{DLM-concur12, address = {Newcastle, UK}, month = sep, year = 2012, volume = 7454, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Koutny, Maciej and Ulidowski, Irek}, acronym = {{CONCUR}'12}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Quantified {CTL}: expressiveness and model checking}, pages = {177-192}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur12.pdf}, doi = {10.1007/978-3-642-32940-1_14}, abstract = {While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.} }

@inproceedings{FLMS-time12, address = {Leicester, UK}, month = sep, year = 2012, publisher = {{IEEE} Computer Society Press}, editor = {Reynolds, Mark and Terenziani, Paolo and Moszkowski, Ben}, acronym = {{TIME}'12}, booktitle = {{P}roceedings of the 19th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'12)}, author = {Fribourg, Laurent and Lesens, David and Moro, Pierre and Soulat, Romain}, title = {Robustness Analysis for Scheduling Problems using the Inverse Method}, pages = {73-80}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf}, doi = {10.1109/TIME.2012.10}, abstract = {Given a Parametric Timed Automaton (PTA)~\(\mathcal{A}\) and a tuple~\(\pi_{0}\) of reference valuations for timings, the \emph{Inverse Method~(IM)} synthesizes a constraint around~\(\pi_{0}\) where \(\mathcal{A}\) behaves in the same time-abstract manner. This provides us with a quantitative measure of robustness of the behavior of~\(\mathcal{A}\) around~\(\pi_{0}\). We~show in this paper how \textit{IM} can be applied in a specific way to treat the robustness of scheduling systems. We also explain how to use the method in order to synthesize large zones of the timing parameter space where the system is guaranteed to be schedulable. We illustrate the method on several examples of the literature as well as a case study originating from an industrial design project.} }

@inproceedings{AFKS12, address = {Paris, France}, month = aug, year = 2012, volume = {7436}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Giannakopoulou, Dimitra and M{\'e}ry, Dominique}, acronym = {{FM}'12}, booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium on {F}ormal {M}ethods ({FM}'12)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain}, title = {{IMITATOR}~2.5: A~Tool for Analyzing Robustness in Scheduling Problems}, pages = {33-36}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf}, doi = {10.1007/978-3-642-32759-9_6}, abstract = {The tool \textsc{Imitator} implements the \emph{Inverse Method~(IM)} for Timed Automata~(TAs). Given a TA~\(\mathcal{A}\) and a tuple~\(\pi_{0}\) of reference valuations for timings, \textit{IM} synthesizes a constraint around~\(\pi_{0}\) where \(\mathcal{A}\) behaves in the same discrete manner. This provides us with a quantitative measure of robustness of the behavior of~\(\mathcal{A}\) around~\(\pi_{0}\). The new version \textsc{Imitator}~2.5 integrates the new features of stopwatches (in~addition to standard clocks) and updates (in addition to standard clock resets), as well as powerful algorithmic improvements for state space reduction. These new features make the tool well-suited to analyze the robustness of solutions in several classes of preemptive scheduling problems.} }

@inproceedings{AMH-safep12, address = {Mexico City, Mexico}, month = aug, year = 2012, publisher = {IFAC}, acronym = {{SAFEPROCESS}'12}, booktitle = {{P}roceedings of the 8th {IFAC} {S}ymposium on {F}ault {D}etection, {S}upervision and {S}afety for {T}echnical {P}rocesses ({SAFEPROCESS}'12)}, author = {Agarwal, Anoopam and Madalinski, Agnes and Haar, Stefan}, title = {Effective Verification of Weak Diagnosability}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf}, doi = {10.3182/20120829-3-MX-2028.00083}, abstract = {The \emph{diagnosability} problem can be stated as follows: does a given labeled Discrete Event System allow for an outside observer to determine the occurrence of the {"}invisible{"} fault, no later than a bounded number of events after that unobservable occurrence, and based on the partial observation of the behaviour? When this problem is investigated in the context of concurrent systems, partial order semantics induces a separation between classical or strong diagnosability on the one hand, and \emph{weak diagnosability} on the other hand. The present paper presents the first solution for checking weak diagnosability, via a \emph{verifier} construction.} }

@inproceedings{BBJM-qest12, address = {London, UK}, month = sep, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'12}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'12)}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Jurdzi{\'n}ski, Marcin and Menet, Quentin}, title = {Almost-Sure Model-Checking of Reactive Timed Automata}, pages = {138-147}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf}, doi = {10.1109/QEST.2012.10}, abstract = {We consider the model of stochastic timed automata, a model in which both delays and discrete choices are made probabilistically. We are interested in the almost-sure model-checking problem, which asks whether the automaton satisfies a given property with probability~\(1\). While this problem was shown decidable for single-clock automata few years ago, it was also proven that the algorithm for this decidability result could not be used for general timed automata. In this paper we describe the subclass of reactive timed automata, and we prove decidability of the almost-sure model-checking problem under that restriction. Decidability relies on the fact that this model is almost-surely fair. As a desirable property of real systems, we show that reactive automata are almost-surely non-Zeno. Finally we show that the almost-sure model-checking problem can be decided for specifications given as deterministic timed automata.} }

@inproceedings{BLM-qest12, address = {London, UK}, month = sep, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'12}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'12)}, author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas}, title = {Lower-Bound Constrained Runs in Weighted Timed Automata}, pages = {128-137}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf}, doi = {10.1109/QEST.2012.28}, noontract = {}, abstract = {We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer \textit{et~al.}, {"}Infinite runs in weighted timed automata with energy constraints{"}, FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is---for us somewhat unexpectedly---undecidable for weighted timed automata with four or more clocks.\par This undecidability result assumes a fixed and know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. Finally, we prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.} }

@article{BMOSW-fac12, publisher = {Springer}, journal = {Formal Aspects of Computing}, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and Worrell, James}, title = {On Termination and Invariance for Faulty Channel Systems}, year = 2012, month = jul, volume = 24, number = {4-6}, pages = {595-607}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf}, doi = {10.1007/s00165-012-0234-7}, abstract = {A~\emph{channel machine} consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with \emph{insertion errors}, i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.} }

@inproceedings{BDL-tase12, address = {Beijing, China}, month = jul, year = 2012, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{TASE}'12}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {T}heoretical {A}spects of {S}oftware {E}ngineering ({TASE}'12)}, author = {Bollig, Benedikt and Decker, Normann and Leucker, Martin}, title = {Frequency Linear-time Temporal Logic}, pages = {85-92}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf}, doi = {10.1109/TASE.2012.43}, abstract = {We propose fLTL, an extension to linear-time temporal logic (LTL) that allows for expressing relative frequencies by a generalization of temporal operators. This facilitates the specification of requirements such as the deadlines in a real-time system must be met in at least~\(95\%\) of all cases. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of LTL by allowing, e.g., to express non-context-free properties.} }

@inproceedings{IL-pairing12, address = {Cologne, Germany}, month = may, year = 2012, volume = 7708, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abdalla, Michel and Lange, Tanja}, acronym = {{PAIRING}'12}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {P}airing-Based {C}ryptography ({PAIRING}'12)}, author = {Izabach{\`e}ne, Malika and Libert, Beno{\^\i}t}, title = {Divisible E-Cash in the Standard Model}, pages = {314-332}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/IL-pairing12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/IL-pairing12.pdf}, doi = {10.1007/978-3-642-36334-4_20}, abstract = {Off-line e-cash systems are the digital analogue of regular cash. One of the main desirable properties is anonymity: spending a coin should not reveal the identity of the spender and, at the same time, users should not be able to double-spend coins without being detected. Compact e-cash systems make it possible to store a wallet of \(O(2^{L})\) coins using \(O(L + \lambda)\) bits, where \(\lambda\) is the security parameter. They are called \emph{divisible} whenever the user has the flexibility of spending an amount of~\(2^{\ell}\), for some \(\ell\leq L\), more efficiently than by repeatedly spending individual coins. This paper presents the first construction of divisible e-cash in the standard model (i.e., without the random oracle heuristic). The scheme allows a user to obtain a wallet of~\(2^{L}\) coins by running a withdrawal protocol with the bank. Our construction is built on the traditional binary tree approach, where the wallet is organized in such a way that the monetary value of a coin depends on how deep the coin is in the tree.} }

@inproceedings{BMS-icalp12, address = {Warwick, UK}, month = jul, year = 2012, volume = {7392}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger}, acronym = {{ICALP}'12}, booktitle = {{P}roceedings of the 39th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'12)~-- {P}art~{II}}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Reachability in Timed Automata: A~Game-based Approach}, pages = {128-140}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf}, doi = {10.1007/978-3-642-31585-5_15}, abstract = {Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing {"}robust{"} strategies for ensuring reachability of a location in a timed automaton; with {"}robust{"}, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete.} }

@incollection{topnoc12-ehh, year = 2012, volume = 6900, series = {Lecture Notes in Computer Science}, editor = {Jensen, Kurt and Donatelli, Susanna and Kleijn, Jetty}, publisher = {Springer}, booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{V}}, author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf}, title = {Refinement and Asynchronous Composition of Modal {P}etri Nets}, pages = {96-120}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf}, doi = {10.1007/978-3-642-29072-5_4}, abstract = {We propose a framework for the specification of infinite state systems based on Petri nets with distinguished \emph{may}- and \emph{must}-transitions (called modalities) which specify the allowed and the required behavior of refinements and hence of implementations. For any modal Petri net, we define its generated modal language specification which abstracts away silent transitions. On this basis we consider refinements of modal Petri nets by relating their generated modal language specifications. We show that this refinement relation is decidable if the underlying modal Petri nets are weakly deterministic. We also show that the membership problem for the class of weakly deterministic modal Petri nets is decidable. As an important application scenario of our approach we consider I/O-Petri nets and their asynchronous composition which typically leads to an infinite state system.} }

@inproceedings{benzina-dictap12, address = {Bangkok, Thailand}, month = may, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{DICTAP}'12}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {D}igital {I}nformation and {C}ommunication {T}echnology and its {A}pplication ({DICTAP}'12)}, author = {Benzina, Hedi}, title = {Towards Designing Secure Virtualized Systems}, pages = {250-255}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HB-dictap12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HB-dictap12.pdf}, doi = {10.1109/DICTAP.2012.6215385}, abstract = {Virtual machine technology is rapidly gaining acceptance as a fundamental building block in enterprise data centers. It is most known for improving efficiency and ease of management. However, it also provides a compelling approach to enhancing system security, offering new ways to rearchitect todays systems and opening the door for a wide range of future security technologies. While this technology is meant to enhance the security of computer systems, some recent attacks show that virtual machine technology has many weaknesses and becomes exposed to many security threats. In this paper we present some of these threats and show how we protect these systems through intrusion detection and security policies mechanisms.} }

@article{jcss12-DJLL, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, 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}, year = {2012}, volume = 79, number = 1, pages = {23-38}, month = feb, url = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf}, doi = {10.1016/j.jcss.2012.04.002}, abstract = {The covering and boundedness problems for branching vector addition systems are shown complete for doubly-exponential time.} }

@inproceedings{ACD-csf12, address = {Cambridge Massachusetts, USA}, month = jun, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'12}, booktitle = {{P}roceedings of the 25th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'12)}, author = {Arapinis, Myrto and Cheval, Vincent and Delaune, St{\'e}phanie}, title = {Verifying privacy-type properties in a modular way}, pages = {95-109}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf12.pdf}, doi = {10.1109/CSF.2012.16}, abstract = {Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlinkability) that play an important role in many modern applications are formalised using a notion of equivalence.\par In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches.\par As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.} }

@inproceedings{benzina-iscc12, address = {Nev{\c{s}}ehir, Turkey}, month = jul, year = 2012, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{ISCC}'12}, booktitle = {{P}roceedings of the 17th {IEEE} {S}ymposium on {C}omputers and {C}ommunications ({ISCC}'12)}, author = {Benzina, Hedi}, title = {A~Network Policy Model for Virtualized Systems}, pages = {680-683}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iscc12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iscc12.pdf}, doi = {10.1109/ISCC.2012.6249376}, abstract = {Modern hypervisors offer the ability to build virtual networks between virtual machines. These networks are very useful in both personal and professional activities since they offer the same opportunities as physical networks, but in a much lower cost in terms of hardware and time. On the other hand, these networks are facing many security threats due to the absence of rigourous security policies that protect the sensitive ressources of the network. In this paper, we propose a multilevel security policy model for these networks, this policy covers not only network operations, but also operations related to the management of the virtual architecture.} }

@inproceedings{DKP-ijcar12, address = {Manchester, UK}, month = jun, year = 2012, volume = {7364}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli}, acronym = {{IJCAR}'12}, booktitle = {{P}roceedings of the 6th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'12)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Pasail{\u{a}}, Daniel}, title = {Security protocols, constraint systems, and group theories}, pages = {164-178}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-ijcar12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-ijcar12.pdf}, doi = {10.1007/978-3-642-31365-3_15}, abstract = {When formally analyzing security protocols it is often important to express properties in terms of an adversary's inability to distinguish two protocols. It has been shown that this problem amounts to deciding the equivalence of two constraint systems, i.e., whether they have the same set of solutions. In this paper we study this equivalence problem when cryptographic primitives are modeled using a group equational theory, a special case of monoidal equational theories. The results strongly rely on the isomorphism between group theories and rings. This allows us to reduce the problem under study to the problem of solving systems of equations over rings.\par We provide several new decidability and complexity results, notably for equational theories which have applications in security protocols, such as exclusive or and Abelian groups which may additionally admit a unary, homomorphic symbol.} }

@inproceedings{KS-csr12, address = {Nizhni Novgorod, Russia}, month = jul, year = 2012, volume = {7353}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hirsch, Edward A. and Karhum{\"a}ki, Juhani and Lepist{\"o}, Arto and Prilutskii, Michail}, acronym = {{CSR}'12}, booktitle = {{P}roceedings of the 7th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'12)}, author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {Cutting Through Regular {P}ost Embedding Problems}, pages = {229-240}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf}, doi = {10.1007/978-3-642-30642-6_22}, abstract = {The Regular Post Embedding Problem extended with partial (co)directness is shown decidable. This extends to universal and{\slash}or counting versions. It is also shown that combining directness and codirectness in Post Embedding problems leads to undecidability.} }

@phdthesis{doyen-HDR11, author = {Doyen, Laurent}, title = {Games and Automata: From Boolean to Quantitative Verification}, year = 2012, month = mar, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-ld.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-ld.pdf}, noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/hdr-ld-slides.pdf} }

@techreport{rr-lsv-12-05, author = {Soulat, Romain}, title = {Scheduling with {IMITATOR}: Some Case Studies}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = mar, type = {Research Report}, number = {LSV-12-05}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-05.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-05-v1.pdf, 20120313}, note = {13~pages}, abstract = {The tool IMITATOR implements the \emph{Inverse Method (IM)} for Timed Automata (TAs). Given a TA~\(\mathcal{A}\) and a tuple~\(\pi_0\) of reference valuations for timings, IM synthesizes a constraint around pi0 where A behaves in the same discrete manner. This provides us with a quantitative measure of robustness of the behavior of~\(\mathcal{A}\) around~\(\pi_0\).\par The new version IMITATOR~2.5 integrates the new features of stopwatches (in addition to standard clocks) and updates (in addition to standard clock resets), as well as powerful algorithmic improvements for state space reduction. We illustrate on several case studies of preemptive scheduling problems how such features make the tool well-suited to analyze robustness.} }

@article{BCH-fmsd12, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan}, title = {A~Concurrency-Preserving Translation from Time {P}etri Nets to Networks of Timed Automata}, year = 2012, month = jun, volume = 40, number = 3, pages = {330-355}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf}, doi = {10.1007/s10703-012-0146-4}, abstract = {Several formalisms to model distributed real-time systems coexist in the literature. This naturally induces a need to compare their expressiveness and to translate models from one formalism to another when possible. The first formal comparisons of the expressiveness of these models focused on the preservation of the sequential behavior of the models, using notions like timed language equivalence or timed bisimilarity. They do not consider preservation of concurrency. In~this paper we define timed traces as a partial order representation of executions of our models for real-time distributed systems. Timed traces provide an alternative to timed words, and take the distribution of actions into account. We propose a translation between two popular formalisms that describe timed concurrent systems: \(1\)-bounded time Petri nets~(TPN) and networks of timed automata~(NTA). Our translation preserves the distribution of actions, that is we require that if the TPN represents the product of several components (called processes), then each process should have its counterpart as one timed automaton in the resulting~NTA.} }

@techreport{rr-lsv-12-04, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine}, title = {Importance Sampling for Model Checking of Time-Bounded Until}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2012}, month = feb, type = {Research Report}, number = {LSV-12-04}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04-v1.pdf, 20120227}, note = {14~pages}, abstract = {Statistical model-checking is an alternative verification technique applied on stochastic systems whose size is beyond numerical analysis ability. Given a model (most often a Markov chain) and a formula, it provides a confidence interval for the probability that the model satisfies the formula. In a previous contribution, we have overtaken the main limitation of the statistical approach, i.e. the computation time explosion associated with the evaluation of very small probabilities. This method was valid only for the standard ``Until'' of temporal logics. We establish a similar validity condition which applies to the ``Bounded Until'', using more elaborate arguments. We also address the problem of additional memory requirements necessary to apply the method and we design several algorithms depending on the intended trade-off between time and memory. The corresponding algorithms have been implemented in our tool Cosmos. We present experimentations on several relevant systems, with drastic time reductions w.r.t. standard statistical model checking.} }

@inproceedings{AFS-nfm12, address = {Norfolk, Virginia, USA}, month = apr, year = 2012, volume = 7226, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Goodloe, Alwyn and Person, Suzette}, acronym = {{NFM}'12}, booktitle = {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods {S}ymposium ({NFM}'12)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat, Romain}, title = {Enhancing the Inverse Method with State Merging}, pages = {100-105}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf}, doi = {10.1007/978-3-642-28891-3_10}, abstract = {Keeping the state space small is essential when verifying real-time systems using Timed Automata~(TA). In~the model-checker Uppaal, the merging operation has been used extensively in order to reduce the number of states. Actually, Uppaal's merging technique applies within the more general setting of Parametric Timed Automata (PTA). The \emph{Inverse Method~(IM)} for a PTA~\(\mathcal{A}\) is a procedure that synthesizes a zone around a given point~\(\pi^{0}\) (parameter valuation) over which \(\mathcal{A}\) is guaranteed to behave similarly. We show that the integration of merging into~\emph{IM} leads to the synthesis of larger zones around~\(\pi^{0}\). It~also often improves the performance of~\emph{IM}, both in terms of computational space and time, as shown by our experimental results.} }

@article{BHS-fmsd2012, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu}, title = {Interrupt Timed Automata: Verification and Expressiveness}, year = {2012}, month = feb, volume = {40}, number = {1}, pages = {41-87}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf}, doi = {10.1007/s10703-011-0140-2}, abstract = {We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.\par While the reachability problem is undecidable for hybrid automata we show that it is decidable for ITA. More precisely we prove that the untimed language of an ITA is regular, by building a finite automaton as a generalized class graph. We then establish that the reachability problem for ITA is in NEXPTIME and in PTIME when the number of clocks is fixed. To prove the first result, we define a subclass ITA\(_{-}\) of ITA, and show that (1)~any ITA can be reduced to a language-equivalent automaton in ITA\(_{-}\) and (2)~the reachability problem in this subclass is in NEXPTIME (without any class graph).\par In the next step, we investigate the verification of real time properties over ITA. We prove that model checking SCL, a fragment of a timed linear time logic, is undecidable. On the other hand, we give model checking procedures for two fragments of timed branching time logic.\par We also compare the expressive power of classical timed automata and ITA and prove that the corresponding families of accepted languages are incomparable. The result also holds for languages accepted by controlled real-time automata (CRTA), that extend timed automata. We finally combine ITA with CRTA, in a model which encompasses both classes and show that the reachability problem is still decidable. Additionally we show that the languages of ITA are neither closed under complementation nor under intersection.} }

@article{BK-jal12, publisher = {Elsevier Science Publishers}, journal = {Journal of Applied Logic}, author = {Bollig, Benedikt and Kuske, Dietrich}, title = {An optimal construction of {H}anf sentences}, year = {2012}, month = jun, volume = {10}, number = {2}, pages = {179-186}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf}, doi = {10.1016/j.jal.2012.01.002}, abstract = {We give a new construction of formulas in Hanf normal form that are equivalent to first-order formulas over structures of bounded degree. This is the first algorithm whose running time is shown to be elementary. The triply exponential upper bound is complemented by a matching lower bound.} }

@article{GMM-fmsd2012, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Ganty, Pierre and Majumdar, Rupak and Monmege, Benjamin}, title = {Bounded underapproximations}, year = {2012}, month = apr, volume = {40}, number = {2}, pages = {206-231}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GMM-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GMM-fmsd12.pdf}, doi = {10.1007/s10703-011-0136-y}, abstract = {We show a new and constructive proof of the following language-theoretic result: for every context-free language~\(L\), there is a bounded context-free language \(L'\subseteq L\) which has the same Parikh (commutative) image as~\(L\). Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form \(w_{1}^{*}w_{2}^{*}\cdots w_{m}^{*}\) for some \(w_1,\cdots,w_{m}\in \Sigma^{*}\). In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, we give a new construction that shows that each context free language~\(L\) has a subset~\(L_{N}\) that has the same Parikh image as~\(L\) and that can be represented as a sequence of substitutions on a linear language. Second, we inductively construct a Parikh-equivalent bounded context-free subset of~\(L_{N}\).\par We show two applications of this result in model checking: to underapproximate the reachable state space of multithreaded procedural programs and to underapproximate the reachable state space of recursive counter programs. The bounded language constructed above provides a decidable underapproximation for the original problems. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word~\(w\in L\) is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.} }

@inproceedings{CCK-esop12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7211}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Seidl, Helmut}, acronym = {{ESOP}'12}, booktitle = {{P}rogramming {L}anguages and {S}ystems~--- {P}roceedings of the 22nd {E}uropean {S}ymposium on {P}rogramming ({ESOP}'12)}, author = {Chadha, Rohit and Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Kremer, Steve}, title = {Automated verification of equivalence properties of cryptographic protocols}, pages = {108-127}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCK-esop12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCK-esop12.pdf}, doi = {10.1007/978-3-642-28869-2_6}, abstract = {Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those which can be modeled by an optimally reducing convergent rewrite system. Although, we were unable to prove its termination, it has been implemented in a prototype tool and has been effectively tested on examples, some of which were outside the scope of existing tools.} }

@article{BDL-icomp12, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne}, title = {On the Almighty Wand}, year = {2012}, volume = 211, pages = {106-137}, month = feb, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf}, doi = {10.1016/j.ic.2011.12.003}, abstract = {We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called~\texttt{SL}) and its fragments. \texttt{SL}~can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as \texttt{SL} and as a by-product we get undecidability of~\texttt{SL}. This is refined by showing that \texttt{SL} without the separating conjunction is as expressive as~\texttt{SL}, whence undecidable too. As a consequence, in \texttt{SL} the separating implication (also known as the magic wand) can simulate the separating conjunction. By~contrast, we establish that \texttt{SL} without the magic wand is decidable, and we~prove a non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. This result is extended with a bounded use of the magic wand that appears in Hoare-style rules. As a generalisation, it~is shown that~\(k\texttt{SL}\), the separation logic over heaps with \(k\geq 1\) record fields, is equivalent to~\(k\texttt{SO}\), the second-order logic over heaps with \(k\) record fields.} }

@inproceedings{BLLJKFSFR-revet12, address = {Hammamet, Tunisia}, month = mar, year = 2012, publisher = {{IEEE} Power~\& Energy Society}, editor = {Neji, Rafik}, acronym = {{REVET}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {R}enewable {E}nergies and {VE}hicular {T}echnology ({REVET}'12)}, author = {Belkacem, Ghania and Labrousse, Denis and Lefebvre, St{\'e}phane and Joubert, Pierre-Yves and K{\"u}hne, Ulrich and Fribourg, Laurent and Soulat, Romain and Florentin, {\'E}ric and Rey, {\relax Ch}ristian}, title = {Distributed and Coupled Electrothermal Model of Power Semiconductor Devices}, pages = {84-89}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf}, doi = {10.1109/REVET.2012.6195253}, abstract = {Electro-thermal model of power semiconductor devices are of key importance in order to optimize their thermal design and increase their reliability. The development of such an electro-thermal model for power MOSFET transistors (COOLMOS\textsuperscript{(TM)}) based on the coupling between two computation softwares (Matlab and Cast3M) is described in the paper. The elaborated 2D electro-thermal model is able to predict i)~the~temperature distribution on chip surface well as in volume, ii)~the~effect of the temperature on the distribution of the current flowing within the die and iii)~the~effects of the ageing of the metallization layer on the current density and the temperature. In the paper, the used electrical and thermal models are described as well as the implemented coupling scheme.} }

@inproceedings{SVMM-sbbd2012, address = {S{\~a}o~Paulo, Brazil}, month = oct, year = 2012, editor = {Casanova, Marco A.}, publisher = {Sociedade Brasileira de Computa{\c{c}}{\~a}o}, acronym = {{SBBD}'12}, booktitle = {{P}roceedings of the 27th {B}razilian {S}ymposium on {D}atabases ({SBBD}'12)}, author = {Sim{\~o}es{ }De{~}Sousa, Diego V. and Viana, Henrique and Markey, Nicolas and de Mac{\^e}do, Jose Ant{\^o}nio F.}, title = {Querying Trajectories through Model Checking based on Timed Automata}, pages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SVMM-sbbd2012.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SVMM-sbbd2012.pdf}, abstract = {The popularization of geographical position devices (e.g.~GPS) creates new opportunities for analyzing behavior of moving objects. However, such analysis are hindered by a lack of semantic information associated to the basic information provided by~GPS. Previous works propose semantic enrichment of trajectories. Through the semantic enrichment, we~could check which trajectories have a given moving sequence in an application. Often, this~sequence is expressed according to the semantic application, using the approach of semantic trajectories proposed in the literature. This~trajectory can be represented as a sequence of predicates that holds in some time interval. However, the solutions for querying moving sequence proposed by previous works have a high computational cost. In~this paper, we~propose an expressive query language to semantic trajectories that allows temporal constraints. To~evaluate a query we will use model checking based on timed automata, that can be performed in polynomial time. As~this model checking algorithm is not implemented yet, we propose to use UPPAAL tool, that can be more expensive theoretically, but we expected that will be ecient for our approach. In addition, we will present a query example that demonstrates the expressive power of our language. Although in this paper we will focus on semantic trajectories data, our approach is general enough for being applied to other purposes.} }

@incollection{CD-nato12, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Formal Security Proofs}, booktitle = {Software Safety and Security}, pages = {26-63}, editor = {Nipkow, Tobias and Grumberg, Orna and Hauptmann, Benedikt}, series = {NATO Science for Peace and Security Series~-- D:~Information and Communication Security}, volume = {33}, publisher = {{IOS} Press}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf}, year = 2012, month = may }

@inproceedings{CLHKS-ispec12, address = {Hangzhou, China}, year = 2012, month = apr, volume = 7232, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ryan, Mark D. and Smyth, Ben and Wang, Guilin}, acronym = {{ISPEC}'12}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {I}nformation {S}ecurity {P}ractice and {E}xperience ({ISPEC}'12)}, author = {Comon{-}Lundh, Hubert and Hagiya, Masami and Kawamoto, Yusuke and Sakurada, Hideki}, title = {Computational Soundness of Indistinguishability Properties without Computable Parsing}, pages = {63-79}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf}, doi = {10.1007/978-3-642-29101-2_5}, abstract = {We provide a symbolic model for protocols using public-key encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there is an attack in the symbolic (abstract) model. Our original contribution is that we deal with the security properties, such as anonymity, which cannot be described using a single execution trace, while considering an unbounded number of sessions of the protocols in the presence of active and adaptive adversaries. Our soundness proof is different from all existing studies in that it does not require a computable parsing function from bit strings to terms. This allows us to deal with more cryptographic primitives, such as a preimage-resistant and collision-resistant hash function whose input may have different lengths.} }

@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.", }}

@misc{AG:anr-cpp12, author = {Adj{\'e}, Assal{\'e} and Goubault-Larrecq, Jean}, howpublished = {Fourniture du projet ANR CPP (Confidence, Proofs, and Probabilities), WP 2, version 1}, month = oct, title = {Concrete semantics of programs with non-deterministic and random inputs}, year = {2012}, url = {http://arxiv.org/abs/1210.2605} }

*This file was generated by
bibtex2html 1.98.*