@inproceedings{BCFL-gdv04, address = {Boston, Massachusetts, USA}, month = feb, year = {2005}, number = 1, volume = 119, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {De Alfaro, Luca}, acronym = {{GDV}'04}, booktitle = {{P}roceedings of the {W}orkshop on {G}ames in {D}esign and {V}erification ({GDV}'04)}, author = {Bouyer, Patricia and Cassez, Franck and Fleury, Emmanuel and Larsen, Kim G.}, title = {Synthesis of Optimal Strategies Using {HyTech}}, pages = {11-31}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCFL-gdv04.ps}, doi = {10.1016/j.entcs.2004.07.006}, abstract = {Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in~[BCFL04]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example. } }

@article{ComonCortier-TCS1, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Comon, Hubert and Cortier, V{\'e}ronique}, title = {Tree Automata with One Memory, Set Constraints and Cryptographic Protocols}, year = {2005}, volume = 331, number = 1, pages = {143-214}, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps}, doi = {10.1016/j.tcs.2004.09.036} }

@inproceedings{DFH-avocs2004, address = {London, UK}, month = may, year = {2005}, number = 6, volume = {128}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Huth, Michael R. A.}, acronym = {{AVoCS}'04}, booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'04)}, author = {Duflot, Marie and Fribourg, Laurent and H{\'e}rault, {\relax Th}omas and Lassaigne, Richard and Magniette, Fr{\'e}d{\'e}ric and Messika, St{\'e}phane and Peyronnet, Sylvain and Picaronny, Claudine}, title = {Probabilistic Model Checking of the {CSMA/CD} Protocol Using {PRISM} and {APMC}}, pages = {195-214}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf}, doi = {10.1016/j.entcs.2005.04.012} }

@inproceedings{DFV-avocs04, address = {London, UK}, month = may, year = {2005}, number = 6, volume = {128}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Huth, Michael R. A.}, acronym = {{AVoCS}'04}, booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'04)}, author = {Darlot, {\relax Ch}ristophe and Finkel, Alain and Van{~}Begin, Laurent}, title = {About {F}ast and {TReX} Accelerations}, pages = {87-103}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf}, doi = {10.1016/j.entcs.2005.04.006} }

@inproceedings{FGRV-express04, address = {London, UK}, month = apr, year = 2005, number = 2, volume = 128, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Baeten, Jos and Corradini, Flavio}, acronym = {{EXPRESS}'04}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'04)}, author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and Van{~}Begin, Laurent}, title = {On the Omega-Language Expressive Power of Extended {P}etri Nets}, pages = {87-101}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf}, doi = {10.1016/j.entcs.2004.11.030} }

@article{FL-IPL04, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {The Convex Hull of a Regular Set of Integer Vectors is Polyhedral and Effectively Computable}, year = {2005}, month = oct, volume = 96, number = 1, pages = {30-35}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-ipl05.ps}, doi = {10.1016/j.ipl.2005.04.004}, abstract = {Number Decision Diagrams (NDD) provide a natural finite symbolic representation for regular set of integer vectors encoded as strings of digit vectors (least or most significant digit first). The convex hull of the set of vectors represented by a~NDD is proved to be an effectively computable convex polyhedron.} }

@article{GLRV:acm, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Programming}, author = {Goubault{-}Larrecq, Jean and Roger, Muriel and Verma, Kumar N.}, title = {Abstraction and Resolution Modulo~{AC}: {H}ow to Verify {D}iffie-{H}ellman-like Protocols Automatically}, volume = 64, number = 2, pages = {219-251}, year = {2005}, month = aug, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps}, doi = {10.1016/j.jlap.2004.09.004} }

@article{JGL:val:ext, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Goubault{-}Larrecq, Jean}, title = {Extensions of Valuations}, year = {2005}, volume = 15, number = 2, pages = {271-297}, month = apr, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-17.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2002-17.rr.ps}, doi = {10.1017/S096012950400461X} }

@inproceedings{KremerRyan2004, address = {London, UK}, month = may, year = 2005, number = 5, volume = {128}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Focardi, Riccardo and Zavattaro, Gianluigi}, acronym = {{SecCo}'04}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'04)}, author = {Kremer, Steve and Ryan, Mark D.}, title = {Analysing the Vulnerability of Protocols to Produce Known-pair and Chosen-text Attacks}, pages = {84-107}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf}, doi = {10.1016/j.entcs.2004.11.043}, abstract = {In this paper we report on an analysis for finding known-pair and chosen-text attacks in protocols. As these attacks are at the level of blocks, we extend the attacker by special capabilities related to block chaining techniques. The analysis is automated using Blanchet's protocol verifier and illustrated on two well-known protocols, the Needham-Schroeder-Lowe public-key protocol as well as the Needham-Schroeder symmetric-key protocol. On the first protocol, we show how the special intruder capabilities related to chaining may compromise the secrecy of nonces and that chosen-ciphertext attacks are possible. We propose two modified versions of the protocol which strengthen its security. We then illustrate known-pair and chosen-plaintext attacks on the second protocol.} }

@inproceedings{couvreur-ciaa04, address = {Kingston, Ontario, Canada}, month = jan, year = 2005, volume = 3317, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Domaratzki, Michael and Okhotin, Alexander and Salomaa, Kai and Yu, Sheng}, acronym = {{CIAA}'04}, booktitle = {{R}evised {S}elected {P}apers of the 9th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'04)}, author = {Couvreur, Jean-Michel}, title = {A {BDD}-like Implementation of an Automata Package}, pages = {310-311}, doi = {10.1007/b105090} }

@article{ABRS-lossy, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Abdulla, Parosh Aziz and Bertrand, Nathalie and Rabinovich, Alexander and Schnoebelen, {\relax Ph}ilippe}, title = {Verification of Probabilistic Systems with Faulty Communication}, year = 2005, month = nov, volume = 202, number = 2, pages = {141-165}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-ABRS.ps}, doi = {10.1016/j.ic.2005.05.008}, abstract = {Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behavior of such protocols, \emph{Lossy Channel Systems}~(LCS's) have been proposed. In an LCS the communication channels are modeled as unbounded FIFO buffers which are unreliable in the sense that they can nondeterministically lose messages. \par Recently, several attempts have been made to study \emph{Probabilistic Lossy Channel Systems}~(PLCS's) in which the probability of losing messages is taken into account. In this article, we consider a variant of PLCS's which is more realistic than those studied previously. More precisely, we assume that during each step in the execution of the system, each message may be lost with a certain predefined probability. We show that for such systems the following model-checking problem is decidable: to verify whether a linear-time property definable by a finite-state \(\omega\)-automaton holds with probability one. We also consider other types of faulty behavior, such as corruption and duplication of messages, and insertion of new messages, and show that the decidability results extend to these models.} }

@inproceedings{baudet-ccs2005, address = {Alexandria, Virginia, USA}, month = nov, year = 2005, publisher = {ACM Press}, acronym = {{CCS}'05}, booktitle = {{P}roceedings of the 12th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'05)}, author = {Baudet, Mathieu}, title = {Deciding Security of Protocols against Off-line Guessing Attacks}, pages = {16-25}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baudet_CCS05revised.ps}, doi = {10.1145/1102120.1102125}, abstract = {We provide an effective procedure for deciding the existence of off-line guessing attacks on security protocols, for a bounded number of sessions.\par The procedure consists of a constraint solving algorithm for determining satisfiability and equivalence of a class of second-order E-unification problems, where the equational theory~E is presented by a convergent subterm rewriting system.\par To the best of our knowledge, this is the first decidability result to use the generic definition of off-line guessing attacks due to Corin~\emph{et al.} based on static equivalence in the applied pi-calculus.} }

@inproceedings{BCM05-fsttcs, address = {Hyderabad, India}, month = dec, year = 2005, volume = 3821, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ramanujam, R. and Sen, Sandeep}, acronym = {{FSTTCS}'05}, booktitle = {{P}roceedings of the 25th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'05)}, author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas}, title = {On the Expressiveness of {TPTL} and~{MTL}}, pages = {432-443}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCM-fsttcs05.ps}, doi = {10.1007/11590156_35}, abstract = {TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.} }

@inproceedings{BFLS05-atva, address = {Taipei, Taiwan}, month = oct, year = {2005}, volume = 3707, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Peled, Doron A. and Tsay, Yih-Kuen}, acronym = {{ATVA}'05}, booktitle = {{P}roceedings of the 3rd {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'05)}, author = {Bardin, S{\'e}bastien and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe}, title = {Flat acceleration in symbolic model checking}, pages = {474-488}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS05-atva.ps}, doi = {10.1007/11562948_35}, abstract = {Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called {"}acceleration techniques{"} enhance the convergence of fixpoint computations by computing the transitive closure of some transitions. In this paper we develop a new framework for symbolic model checking with accelerations. We also propose and analyze new symbolic algorithms using accelerations to compute reachability sets.} }

@inproceedings{BBGRS-ETFA05, address = {Catania, Italy}, month = sep, year = 2005, publisher = {{IEEE} Industrial Electronics Society}, editor = {Lo Bello, Lucia and Sauter, Thilo}, acronym = {{ETFA}'05}, booktitle = {{P}roceedings of the 10th {IEEE} {I}nternational {C}onference on {E}merging {T}echnologies and {F}actory {A}utomation ({ETFA}'05)}, author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Gourcuff, Vincent and Roussel, Jean-Marc and De{~}Smet, Olivier}, title = {Verification of a timed multitask system with {U}ppaal}, pages = {347-354}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ETFA05-FV.ps}, abstract = {Since it is an important issue for users and system designers, verification of PLC programs has already been studied in various contexts, mostly for untimed programs. More recently, timed features were introduced and modeled with timed automata. In this case study, we consider a part of the so-called MSS (Mecatronic Standard System) platform from Bosh Group, a framework where time aspects are combined with multitask programming. Our model for station~2 of the MSS platform is a network of timed automata, including automata for the operative part and for the control program, written in \emph{Ladder Diagram}. This model is constrained with atomicity hypotheses concerning program execution and model checking of a reaction time property is performed with the tool~{\scshape Uppaal}.} }

@inproceedings{BC-icmtd05, address = {Giens, France}, nmnote = {Informal proceedings. Selected papers to appear in a journal}, month = may, year = 2005, acronym = {{ICMTD}'05}, booktitle = {Proceedings of the 1st {I}nternational {C}onference on {M}emory {T}echnology and {D}esign ({ICMTD}'05)}, author = {Baclet, Manuel and Chevallier, R{\'e}my}, title = {Timed Verification of the {SPSMALL} Memory}, pages = {89-92}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf}, abstract = {The aim of the paper is to verify a small synchronous memory component with the real-time model checker Uppaal, taking into account the electrical propagation delays through gates and along wires.}, missingdoi = {} }

@inproceedings{BH-ICTAC05, address = {Hanoi, Vietnam}, month = oct, year = 2005, volume = 3722, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hung, Dang Van and Wirsing, Martin}, acronym = {{ICTAC}'05}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'05)}, author = {Bidoit, Michel and Hennicker, Rolf}, title = {Externalized and Internalized Notions of Behavioral Refinement}, pages = {334-350}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf}, doi = {10.1007/11560647_22}, abstract = {Many different behavioral refinement notions for algebraic specifications have been proposed in the literature but the relationship between the various concepts is still unclear. In this paper we provide a classification and a comparative study of behavioral refinements according to two directions, the externalized approach which uses an explicit behavioral abstraction operator that is applied to the specification to be implemented, and the internalized approach which uses a built-in behavioral semantics of specifications. We show that both concepts are equivalent under suitable conditions. The formal basis of our study is provided by the COL institution (constructor-based observational logic). Hence, as a side-effect of our study on internalized behavioral refinements, we introduce also a novel concept of behavioral refinement for COL-specifications.} }

@misc{bouyer-jsi05, author = {Bouyer, Patricia}, title = {Timed Automata and Extensions: Decidability Limits}, year = 2005, month = mar, howpublished = {Invited talk, 5{\`e}mes Journ{\'e}es Syst{\`e}mes Infinis ({JSI}'05), Cachan, France} }

@misc{bouyer-games05, author = {Bouyer, Patricia}, title = {Synthesis of Timed Systems}, year = 2005, month = mar, howpublished = {Invited lecture, Spring School on Infinite Games and Their Applications, Bonn, Germany} }

@misc{bouyer-gdv05, author = {Bouyer, Patricia}, title = {Partial Observation of Timed Systems}, year = 2005, month = jul, howpublished = {Invited talk, 2nd Workshop on Games in Design and Verification, Edinburgh, Scotland} }

@misc{gastin-wpv05, author = {Gastin, Paul}, title = {On the synthesis of distributed controllers}, year = 2005, month = nov, howpublished = {Invited talk, Workshop Perspectives in Verification, in honor of Wolfgang Thomas on the occasion of his Doctorate Honoris Causa, Cachan, France} }

@inproceedings{BCD-fossacs05, address = {Edinburgh, Scotland, UK}, month = apr, year = 2005, volume = 3441, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sassone, Vladimiro}, acronym = {{FoSSaCS}'05}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'05)}, author = {Bouyer, Patricia and Chevalier, Fabrice and D'Souza, Deepak}, title = {Fault Diagnosis Using Timed Automata}, pages = {219-233}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-BCD.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf}, doi = {10.1007/b106850}, abstract = {Fault diagnosis consists in observing behaviours of systems, and in detecting online whether an error has occurred or not. In the context of discrete event systems this problem has been well-studied, but much less work has been done in the timed framework. In this paper, we consider the problem of diagnosing faults in behaviours of timed plants. We focus on the problem of synthesizing fault diagnosers which are realizable as deterministic timed automata, with the motivation that such diagnosers would function as efficient online fault detectors. We study two classes of such mechanisms, the class of deterministic timed automata~(DTA) and the class of event-recording timed automata~(ERA). We show that the problem of synthesizing diagnosers in each of these classes is decidable, provided we are given a bound on the resources available to the diagnoser. We prove that under this assumption diagnosability is 2EXPTIME-complete in the case of DTA's whereas it becomes PSPACE-complete for ERA's.} }

@inproceedings{BBBL-concur2005, address = {San Francisco, California, USA}, month = aug, year = 2005, volume = 3653, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca}, acronym = {{CONCUR}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'05)}, author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois}, title = {A New Modality for Almost Everywhere Properties in Timed Automata}, pages = {110-124}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBL05-concur.ps}, doi = {10.1007/11539452_12}, abstract = {The context of this study is timed temporal logics for timed automata. In this paper, we propose an extension of the classical logic TCTL with a new Until modality, called {"}Until almost everywhere{"}. In the extended logic, it is possible, for instance, to express that a property is true at all positions of all runs, except on a negligible set of positions. Such properties are very convenient, for example in the framework of boolean program verification, where transitions result from changing variable values. We investigate the expressive power of this modality and in particular, we prove that it cannot be expressed with classical TCTL modalities. However, we show that model-checking the extended logic remains PSPACE-complete as for~TCTL.} }

@inproceedings{BCL-concur2005, address = {San Francisco, California, USA}, month = aug, year = 2005, volume = 3653, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca}, acronym = {{CONCUR}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'05)}, author = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran{\c{c}}ois}, title = {Modal Logics for Timed Control}, pages = {81-94}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCL05-concur.ps}, doi = {10.1007/11539452_10}, abstract = {In this paper we use the timed modal logic \(L_{\nu}\) to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (\(L_{\nu}^{\mathrm{\small cont}}\)) of the logic \(L_{\nu}\) with a new modality. \par More precisely we define a fragment of~\(L_{\nu}\), namely \(L_{\nu}^{\mathrm{\small det}}\), such that any control objective of~\(L_{\nu}^{\mathrm{\small det}}\) can be translated into an \(L_{\nu}^{\mathrm{\small cont}}\) formula that holds for the plant if and only if there is a controller that can enforce the control objective. \par We also show that the new modality of~\(L_{\nu}^{\mathrm{\small cont}}\) strictly increases the expressive power of~\(L_{\nu}\), while model-checking of~\(L_{\nu}^{\mathrm{\small cont}}\) remains EXPTIME-complete. } }

@inproceedings{BLR-formats2005, address = {Uppsala, Sweden}, month = nov, year = 2005, volume = 3829, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pettersson, Paul and Yi, Wang}, acronym = {{FORMATS}'05}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'05)}, author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and Reynier, Pierre-Alain}, title = {Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems}, pages = {112-126}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLR05-DBM.ps}, doi = {10.1007/11603009_10}, abstract = {Timed automata (TA) are a widely used model for real-time systems. Several tools are dedicated to this model, and they mostly implement a forward analysis for checking reachability properties. Though diagonal constraints do not add expressive power to classical~TA, the standard forward analysis algorithm is not correct for this model. In this paper we survey several approaches to handle diagonal constraints and propose a refinement-based method for patching the usual algorithm: erroneous traces found by the classical algorithm are analyzed, and used for refining the model.} }

@inproceedings{BCK-ICALP2005, address = {Lisboa, Portugal}, month = jul, year = 2005, volume = {3580}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti}, acronym = {{ICALP}'05}, booktitle = {{P}roceedings of the 32nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'05)}, author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer,Steve}, title = {Computationally Sound Implementations of Equational Theories against Passive Adversaries}, pages = {652-663}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf}, doi = {10.1007/11523468_53}, abstract = {In this paper we study the link between formal and cryptographic models for security protocols in the presence of a passive adversary. In contrast to other works, we do not consider a fixed set of primitives but aim at results for an arbitrary equational theory. We define a framework for comparing a cryptographic implementation and its idealization w.r.t.\ various security notions. In particular, we concentrate on the computationnal soundness of static equivalence, a standard tool in cryptographic \(\pi\)-calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, we establish new soundness results for the Exclusive Or, as well as a theory of ciphers and lists.} }

@book{lncs3426, editor = {Bouyssonouse, Bruno and Sifakis, Joseph}, title = {Embedded Systems Design: The {ARTIST} Roadmap for Research and Development}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = 3436, year = 2005, url = {http://www.springer.com/978-3-540-25107-3}, olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-25107-3}, isbn = {3-540-25107-3}, doi = {10.1007/b106761} }

@inproceedings{ComDel-rta2005, address = {Nara, Japan}, month = apr, year = 2005, volume = 3467, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Giesl, J{\"u}rgen}, acronym = {{RTA}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'05)}, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {The finite variant property: {H}ow to get rid of some algebraic properties}, pages = {294-307}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-CD.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf}, doi = {10.1007/b135673}, abstract = {We consider the following problem: Given a term \(t\), a rewrite system \(\mathcal{R}\), a finite set of equations \(E'\) such that \(\mathcal{R}\) is convergent modulo~\(E'\), compute finitely many instances of~\(t\): \(t_1,\ldots,t_n\) such that, for every substitution~\(\sigma\), there is an index \(i\) and a substitution~\(\theta\) such that \( t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where \(t\sigma\mathord{\downarrow}\) is the normal form of \(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par The goal of this paper is to give equivalent (resp. sufficient) conditions for the finite variant property and to systematically investigate this property for equational theories, which are relevant to security protocols verification. For instance, we prove that the finite variant property holds for Abelian Groups, and a theory of modular exponentiation and does not hold for the theory~\textit{ACUNh} (Associativity, Commutativity, Unit, Nilpotence, homomorphism).} }

@article{CF-icomp05, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain}, title = {Verification of Programs with Half-Duplex Communication}, year = 2005, month = nov, volume = 202, number = 2, pages = {166-190}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf}, doi = {10.1016/j.ic.2005.05.006}, abstract = {We consider the analysis of infinite \emph{half-duplex systems} made of finite state machines that communicate over unbounded channels. The half-duplex property for two machines and two channels (one in each direction) says that each reachable configuration has at most one channel non-empty. We prove in this paper that such half-duplex systems have a recognizable reachability set. We show how to compute, in polynomial time, a symbolic representation of this reachability set and how to use that description to solve several verification problems. Furthermore, though the model of communicating finite state machines is Turing-powerful, we prove that membership of the class of half-duplex systems is decidable. Unfortunately, the natural generalization to systems with more than two machines is Turing-powerful. We also prove that the model-checking of those systems against PLTL (Propositional Linear Temporal Logic) or CTL (Computational Tree Logic) is undecidable. Finally, we show how to apply the previous decidability results to the Regular Model Checking. We propose a new symbolic reachability semi-algorithm with accelerations which successfully terminates on half-duplex systems of two machines and some interesting non-half-duplex systems.} }

@misc{cortos05, author = {Bouyer, Patricia and others}, title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS} <<~{C}ontrol and {O}bservation of {R}eal-{T}ime {O}pen {S}ystems~>>~--- Rapport {\`a} mi-parcours}, year = 2005, month = apr, type = {Contract Report}, note = {6~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf}, missingdoi = {} }

@inproceedings{Cortos-MSR05-impl, address = {Autrans, France}, month = oct, year = 2005, publisher = {Herm{\`e}s}, editor = {Alla, Hassane and Rutten, {\'E}ric}, acronym = {{MSR}'05}, booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'05)}, author = {Altisen, Karine and Markey, Nicolas and Reynier, Pierre-Alain and Tripakis, Stavros}, title = {Impl{\'e}mentabilit{\'e} des automates temporis{\'e}s}, pages = {395-406}, nonote = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-impl.ps}, abstract = {In this paper, we present the problem of the implementability of timed automata. The theoretical semantics of timed automata can not be exactly implemented in practice, because computers are digital and more or less precise; the properties verified on a timed automaton are not necessarily preserved when implementing it. We deal with two approaches: the first one is based on the modeling of the execution platform and the second studies an enlarged semantics for timed automata that takes the imprecision into account.} }

@inproceedings{Cortos-MSR05-obs, address = {Autrans, France}, month = oct, year = 2005, publisher = {Herm{\`e}s}, editor = {Alla, Hassane and Rutten, {\'E}ric}, acronym = {{MSR}'05}, booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'05)}, author = {Bouyer, Patricia and Chevalier, Fabrice and Krichen, Moez and Tripakis, Stavros}, title = {Observation partielle des syst{\`e}mes temporis{\'e}s}, pages = {381-393}, nonote = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-obs.ps}, abstract = {In this paper, we present the partial observability constraint, which naturally appears when modeling real-time systems. We have selected three problems in which this hypothesis is fundamental but leads to more difficult problems: control of timed systems, fault diagnosis, and conformance testing. We describe methods which can be used for solving such problems. } }

@inproceedings{Cortos-MSR05-control, address = {Autrans, France}, month = oct, year = 2005, publisher = {Herm{\`e}s}, editor = {Alla, Hassane and Rutten, {\'E}ric}, acronym = {{MSR}'05}, booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'05)}, author = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and Cassez, Franck and Gardey, Guillaume}, title = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el}, pages = {367-380}, nonote = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-control.ps}, abstract = {In this paper we give a quick overview of the area of control of real-time systems.} }

@misc{demri-RSFDGrC05, author = {Demri, St{\'e}phane}, title = {On the complexity of information logics}, year = 2005, month = aug, howpublished = {Invited talk, Workshop on Logical and Algebraic Foundations of Rough Sets, Regina, Canada} }

@article{demri-JLC05, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, author = {Demri, St{\'e}phane}, title = {A reduction from {DLP} to~{PDL}}, year = 2005, month = oct, volume = 15, number = 5, pages = {767-785}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf}, doi = {10.1093/logcom/exi043}, abstract = {We present a reduction from a new logic extending van der Meyden's dynamic logic of permission~(DLP) into propositional dynamic logic (PDL), providing a 2EXPTIME decision procedure and showing that all the machinery for~PDL can be reused for reasoning about dynamic policies. As a side-effect, we establish that DLP is EXPTIME-complete. The logic we introduce extends the logic~DLP so that the policy set can be updated depending on its current value and such an update corresponds to add\slash delete transitions in the model, showing similarities with van Benthem's sabotage modal logic.} }

@article{ddn-jlli05, publisher = {Kluwer Academic Publishers}, journal = {Journal of Logic, Language and Information}, author = {Demri, St{\'e}phane and de Nivelle, Hans}, title = {Deciding Regular Grammar Logics with Converse through First-Order Logic}, volume = 14, number = 3, pages = {289-319}, year = {2005}, month = jun, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf}, oldnote = {special issue dedicated to guarded logics.}, doi = {10.1007/s10849-005-5788-9}, abstract = {We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2 , which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains.\par A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in~EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed point-operators.} }

@inproceedings{DZG05-aplas, address = {Tsukuba, Japan}, month = nov, year = 2005, volume = 3780, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Yi, Kwangkeun}, acronym = {{APLAS}'05}, booktitle = {{P}roceedings of the 3rd {A}sian {S}ymposium on {P}rogramming {L}anguages and {S}ystems ({APLAS}'05)}, author = {Dal Zilio, Silvano and Gascon, R{\'e}gis}, title = {Resource Bound Certification for a Tail-Recursive Virtual Machine}, pages = {247-263}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DZG-APLAS05.ps}, doi = {10.1007/11575467_17}, abstract = {We define a method to statically bound the size of values computed during the execution of a program as a function of the size of its parameters. More precisely, we consider bytecode programs that should be executed on a simple stack machine with support for algebraic data types, pattern-matching and tail-recursion. Our size verification method is expressed as a static analysis, performed at the level of the bytecode, that relies on machine-checkable certificates. We follow here the usual assumption that code and certificates may be forged and should be checked before execution.\par Our approach extends a system of static analyses based on the notion of quasi-interpretations that has already been used to enforce resource bounds on first-order functional programs. This paper makes two additional contributions. First, we are able to check optimized programs, containing instructions for unconditional jumps and tail-recursive calls, and remove restrictions on the structure of the bytecode that was imposed in previous works. Second, we propose a direct algorithm that depends only on solving a set of arithmetical constraints.} }

@inproceedings{DG-concur2005, address = {San Francisco, California, USA}, month = aug, year = 2005, volume = 3653, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca}, acronym = {{CONCUR}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'05)}, author = {Demri, St{\'e}phane and Gascon, R{\'e}gis}, title = {Verification of Qualitative {\(\mathbb{\MakeUppercase{Z}}\)}-Constraints}, pages = {518-532}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf}, doi = {10.1007/11539452_39}, abstract = {We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in~\(\mathbb{Z}\). The constraint language includes periodicity constraints, comparison constraints of the form \(x = y\) and \(x < y\), it is closed under Boolean operations and it admits a restricted form of existential quantification. This is the largest set of qualitative constraints over~\(\mathbb{Z}\) known so far, shown to admit a decidable LTL extension. Such constraints are those used for instance in calendar formalisms or in abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. As a by-product, LTL model-checking over integral relational automata is proved complete for polynomial space which contrasts with the known undecidability of its CTL counterpart.} }

@inproceedings{DKR-FEE2005, address = {Milan, Italy}, month = sep, year = 2005, optaddress = {}, acronym = {{FEE} 2005}, booktitle = {{P}roceedings of the {W}orkshop {F}rontiers in {E}lectronic {E}lections ({FEE} 2005)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Receipt-Freeness: Formal Definition and Fault Attacks (Extended Abstract)}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf}, preliminary-version-of = {DKR-csfw06} }

@inproceedings{DLN-time05, address = {Burlington, Vermont, USA}, month = jun, year = 2005, publisher = {{IEEE} Computer Society Press}, acronym = {{TIME}'05}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'05)}, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David}, title = {On the Freeze Quantifier in Constraint {LTL}: Decidability and Complexity}, pages = {113-121}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2005-03.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf}, doi = {10.1109/TIME.2005.28}, abstract = {Constraint LTL, a generalization of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, etc.). We show that Constraint LTL over the simple domain \(\langle \mathbb{N}, = \rangle\) augmented with the freeze operator is undecidable which is a surprising result regarding the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes \(\Sigma_{1}^{1}\)-completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are quite sharp (\emph{i.e.}~with restrictions on the number of variables) and all our complexity characterizations insure completeness with respect to some complexity class (mainly PSPACE and~EXPSPACE).} }

@inproceedings{DN-atva05, address = {Taipei, Taiwan}, month = oct, year = {2005}, volume = 3707, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Peled, Doron A. and Tsay, Yih-Kuen}, acronym = {{ATVA}'05}, booktitle = {{P}roceedings of the 3rd {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'05)}, author = {Demri, St{\'e}phane and Nowak, David}, title = {Reasoning about transfinite sequences (extended abstract)}, pages = {248-262}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-atva2005.ps}, doi = {10.1007/11562948_20}, abstract = {We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on \(\omega\)-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability problem for the logics working on \(\omega^{k}\)-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.} }

@inproceedings{FM-podc05, address = {Las Vegas, Nevada, USA}, month = jul, year = 2005, publisher = {ACM Press}, editor = {Aguilera, Marcos Kawazoe and Aspnes, James}, acronym = {{PODC}'05}, booktitle = {{P}roceedings of the {T}wenty-{F}ourth {A}nnual {ACM} {SIGACT}-{SIGOPS} {S}ymposium on {P}rinciples of {D}istributed {C}omputing ({PODC}'05)}, author = {Fribourg, Laurent and Messika, St{\'e}phane}, title = {Brief Announcement: Coupling for {M}arkov Decision Processes~--- {A}pplication to Self-Stabilization with Arbitrary Schedulers}, pages = {322}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ba173-messika.ps}, doi = {10.1145/1073814.1073875} }

@inproceedings{Gascon-m4m2005, address = {Berlin, Germany}, month = dec, year = 2005, volume = 194, series = {Informatik Bericht}, publisher = {Humboldt Universit{\"a}t zu Berlin}, editor = {Schlingloff, Holger}, acronym = {{M4M-4}}, booktitle = {{P}roceedings of the 4th {W}orkshop on {M}ethods for {M}odalities ({M4M-4})}, author = {Gascon, R{\'e}gis}, title = {Verifying qualitative and quantitative properties with~{LTL} over concrete domains}, pages = {54-61}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gascon-M4M05.ps}, abstract = {We introduce different extensions of LTL where propositional variables are replaced by constraints interpreted in~\(\mathbb{Z}\). We show different decidability and complexity results for the satisfiability and model checking problems of these logics. The extension of LTL over a wide set of qualitative constraints is shown to be PSPACE-complete. When introducing some quantitative constraints, we must consider strong restrictions to regain decidability.} }

@inproceedings{Gastin-ICALP2005, address = {Lisboa, Portugal}, month = jul, year = 2005, volume = {3580}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti}, acronym = {{ICALP}'05}, booktitle = {{P}roceedings of the 32nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'05)}, author = {Droste, Manfred and Gastin, Paul}, title = {Weighted Automata and Weighted Logics}, pages = {513-525}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/icalp05dg-final.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf}, doi = {10.1007/11523468_42}, abstract = {Weighted automata are used to describe quantitative properties in various areas such as probabilistic systems, image compression, speech-to-text processing. The behaviour of such an automaton is a mapping, called a formal power series, assigning to each word a weight in some semiring. We generalize B{\"{u}}chi's and Elgot's fundamental theorems to this quantitative setting. We introduce a weighted version of MSO~logic and prove that, for commutative semirings, the behaviours of weighted automata are precisely the formal power series definable with our weighted logic. We also consider weighted first-order logic and show that aperiodic series coincide with the first-order definable ones, if the semiring is locally finite, commutative and has some aperiodicity property.} }

@inproceedings{GLP:VMCAI, address = {Paris, France}, month = jan, year = 2005, volume = 3385, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cousot, Radhia}, acronym = {{VMCAI}'05}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'05)}, author = {Goubault{-}Larrecq, Jean and Parrennes, Fabrice}, title = {Cryptographic Protocol Analysis on Real {C}~Code}, pages = {363-379}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf}, doi = {10.1007/b105073}, abstract = {Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e.g., SSL or TLS). We describe how cryptographic protocol verification techniques based on solving clause sets can be applied to detect vulnerabilities of C programs in the Dolev-Yao model, statically. This involves integrating fairly simple pointer analysis techniques with an analysis of which messages an external intruder may collect and forge. This also involves relating concrete run-time data with abstract, logical terms representing messages. To this end, we make use of so-called trust assertions. The output of the analysis is a set of clauses in the decidable class H1, which can then be solved independently. This can be used to establish secrecy properties, and to detect some other bugs. } }

@article{JGL-ipl2005, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Goubault{-}Larrecq, Jean}, title = {Deciding {\(\mathcal{\MakeUppercase{H}}_1\)} by Resolution}, year = {2005}, volume = 95, number = 3, pages = {401-408}, month = aug, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf}, doi = {10.1016/j.ipl.2005.04.007}, abstract = {Nielson, Nielson and Seidl's class \(\mathcal{H}_1\) is a decidable class of first-order Horn clause sets, describing strongly regular relations. We give another proof of decidability, and of the regularity of the defined languages, based on fairly standard automated deduction techniques. } }

@article{VGL-dmtcs05, journal = {Discrete Mathematics \& Theoretical Computer Science}, author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean}, title = {{K}arp-{M}iller Trees for a Branching Extension of~{VASS}}, volume = 7, number = 1, pages = {217-230}, year = 2005, month = nov, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf}, secondurl = {http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGL-dmtcs05.ps}, abstract = {We study BVASS (Branching VASS) which extend VASS (Vector Addition Systems with States) by allowing addition transitions that merge two configurations. Runs in BVASS are tree-like structures instead of linear ones as for VASS. We show that the construction of Karp-Miller trees for VASS can be extended to BVASS. This entails that the coverability set for BVASS is computable. This allows us to obtain decidability results for certain classes of equational tree automata with an associative-commutative symbol. Recent independent work by de Groote \emph{et al.} implies that decidability of reachability in BVASS is equivalent to decidability of provability in MELL (multiplicative exponential linear logic), which is still an open problem. Hence our results are also a step towards answering this question in the affirmative.} }

@inproceedings{MukhamedovKremerRitter2005, address = {Roseau, The Commonwealth Of Dominica}, month = aug, year = 2005, volume = 3570, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Patrick, Andrew S. and Yung, Moti}, acronym = {{FC}'05}, booktitle = {{R}evised {P}apers from the 9th {I}nternational {C}onference on {F}inancial {C}ryptography and {D}ata {S}ecurity ({FC}'05)}, author = {Mukhamedov, Aybek and Kremer, Steve and Ritter, Eike}, title = {Analysis of a Multi-Party Fair Exchange Protocol and Formal Proof of Correctness in the Strand Space Model}, pages = {255-269}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf}, doi = {10.1007/11507840_23}, abstract = {A multi-party fair exchange protocol is a cryptographic protocol allowing several parties to exchange commodities in such a way that everyone gives an item away if and only if it receives an item in return. In this paper we discuss a multi-party fair exchange protocol originally proposed by Franklin and Tsudik, and subsequently shown to have flaws and fixed by Gonz\'alez and Markowitch. We identify flaws in the fixed version of the protocol, propose a corrected version, and give a formal proof of correctness in the strand space model.} }

@inproceedings{KremerRyan2005, address = {Edinburgh, Scotland, UK}, month = apr, year = 2005, volume = 3444, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sagiv, Mooly}, acronym = {{ESOP}'05}, booktitle = {{P}rogramming {L}anguages and {S}ystems~--- {P}roceedings of the 14th {E}uropean {S}ymposium on {P}rogramming ({ESOP}'05)}, author = {Kremer, Steve and Ryan, Mark D.}, title = {Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus}, pages = {186-200}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-esop05.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf}, doi = {10.1007/b107380}, abstract = {Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO~92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.} }

@inproceedings{GK-concur05, address = {San Francisco, California, USA}, month = aug, year = 2005, volume = 3653, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca}, acronym = {{CONCUR}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'05)}, author = {Gastin, Paul and Kuske, Dietrich}, title = {Uniform Satisfiability Problem for Local Temporal Logics over {M}azurkiewicz Traces}, pages = {533-547}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur05gk-final.ps}, doi = {10.1007/11539452_40}, abstract = {We continue our study of the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In a previous paper (CONCUR~2003), we investigated the class of local and MSO definable temporal logics that capture all known temporal logics and we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed). In this paper, we concentrate on the uniform satisfiability problem: we consider the dependence alphabet (\emph{i.e.}, the architecture of the distributed system) as part of the input. We prove lower and upper bounds for the uniform satisfiability problem that depend on the number of monadic quantifier alternations present in the chosen MSO-modalities.} }

@inproceedings{LLT-rta2005, address = {Nara, Japan}, month = apr, year = 2005, volume = 3467, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Giesl, J{\"u}rgen}, acronym = {{RTA}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'05)}, author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, title = {Intruder Deduction for {AC}-like Equational Theories with Homomorphisms}, pages = {308-322}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-LLT.ps}, doi = {10.1007/b135673}, abstract = {Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols rely on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the protocol execution. \par We focus on the intruder deduction problem, that is the vulnerability to passive attacks, in presence of several variants of \textit{AC}-like axioms (from \textit{AC} to Abelian groups, including the theory of \emph{exclusive or}) and homomorphism which are the most frequent axioms arising in cryptographic protocols. Solutions are known for the cases of \emph{exclusive or}, of Abelian groups, and of homomorphism alone. In this paper we address the combination of these \textit{AC}-like theories with the law of homomorphism which leads to much more complex decision problems.\par We prove decidability of the intruder deduction problem in all cases considered. Our decision procedure is in EXPTIME, except for a restricted case in which we have been able to get a PTIME decision procedure using a property of one-counter and pushdown automata.} }

@inproceedings{Laroussinie-m4m05, address = {Berlin, Germany}, month = dec, year = 2005, volume = 194, series = {Informatik Bericht}, publisher = {Humboldt Universit{\"a}t zu Berlin}, editor = {Schlingloff, Holger}, acronym = {{M4M-4}}, booktitle = {{P}roceedings of the 4th {W}orkshop on {M}ethods for {M}odalities ({M4M-4})}, author = {Laroussinie, Fran{\c{c}}ois}, title = {Timed modal logics for the verification of real-time systems}, pages = {293-305}, nonote = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lar-M4M05.ps}, abstract = {The timed modal logic \(L_{\nu}\) has been proposed in order to express timed properties over real-time systems modeled as (compositions of) timed automata. In this paper, we present a short survey of results about~\(L_{\nu}\): complexity of model checking, expressivity, compositional methods, relationship with strong timed bisimulation etc. We also show how \(L_{\nu}\) can be extended in order to express new properties. } }

@inproceedings{LS-fossacs05, address = {Edinburgh, Scotland, UK}, month = apr, year = 2005, volume = 3441, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sassone, Vladimiro}, acronym = {{FoSSaCS}'05}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'05)}, author = {Laroussinie, Fran{\c{c}}ois and Sproston, Jeremy}, title = {Model Checking Durational Probabilistic Systems}, pages = {140-154}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-FS.ps}, doi = {10.1007/b106850}, abstract = {We consider model-checking algorithms for durational probabilistic systems, which are systems exhibiting nondeterministic, probabilistic and discrete-timed behaviour. We present two semantics for durational probabilistic systems, and show how formulae of the probabilistic and timed temporal logic PTCTL can be verified on such systems. We also address complexity issues, in particular identifying the cases in which model checking durational probabilistic systems is harder than verifying non-probabilistic durational systems.} }

@inproceedings{LNZ-appsem05, address = {Frauenchiemsee, Germany}, month = sep, year = 2005, editor = {Hofmann, Martin and Loidl, Hans-Wolfgang}, acronym = {{APPSEM}'05}, booktitle = {{P}roceedings of the 3rd {APPSEM~II} Workshop ({APPSEM}'05)}, author = {Lasota, S{\l}awomir and Nowak, David and Zhang, Yu}, title = {On completeness of logical relations for monadic types}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf}, abstract = {Interesting properties of programs can be expressed using contextual equivalence. The latter is difficult to prove directly, hence (pre-)logical relations are often used as a tool to prove it. Whereas pre-logical relations are complete at all types, logical relations are only complete up to first-order types. We propose a notion of contextual equivalence for Moggi's computational lambda calculus, and define pre-logical and logical relations for this calculus. Monads introduce new difficulties: in particular the usual proofs of completeness up to first-order types do not go through. We prove completeness up to first order for several of Moggi's monads. In the case of the non-determinism monad we obtain, as a corollary, completness of strong bisimulation w.r.t.~contextual equivalence in lambda calculus with monadic non-determinism.} }

@techreport{rr-LSV:05:11, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Automated Induction for Complex Data Structures}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2005}, month = jul, type = {Research Report}, number = {LSV-05-11}, note = {24~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2005-11.ps}, abstract = {We develop a new approach for mechanizing induction on complex data structures (like sets, sorted lists, trees, powerlists...). The key idea is to compute a tree grammar with constraints which describes exactly the initial model of the given specification, unlike test sets or cover sets which are approximative induction schemes when the constructors are not free. This grammar is used for the generation of subgoals during the proof by induction. Our procedure is sound and refutationally complete even with constrained axioms for constructors. it subsumes all test set induction techniques, and yields very natural proofs for several examples on which other approaches failed.} }

@techreport{rr-LSV:05:17, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Automatic Verification of Sufficient Completeness for Specifications of Complex Data Structures}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2005, month = aug, type = {Research Report}, number = {LSV-05-17}, note = {14~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2005-17.ps}, abstract = {We present a new procedure for testing sufficient completeness for conditional and constrained term rewriting systems in presence of constrained axioms for constructors. Such axioms allow to specify complex data structures like e.g. sets or sorted lists. Our approach is based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form. The procedure is sound and complete and has been successfully used for checking the sufficient completeness of several specifications where related former techniques fail.} }

@techreport{LSV:05:19, author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, title = {Intruder Deduction for the Equational Theory of Exclusive-or with Distributive Encryption}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2005, month = oct, type = {Research Report}, number = {LSV-05-19}, note = {39~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2005-19.ps}, abstract = {Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol.\par We are interested in the intruder deduction problem, that is the vulnerability to passive attacks, in presence of the theory of an encryption operator which distributes over the \emph{exclusive-or}. This equational theory describes very common properties of cryptographic primitives. Solutions to the intruder deduction problem modulo an equational theory are known for the cases of \emph{exclusive-or}, of Abelian groups, of a homomorphism symbol alone, and of combinations of these theories. In this paper we consider the case where the encryption distributes over \emph{exclusive-or}. The interaction of the distributive law of the encryption with the cancellation law of \emph{exclusive-or} leads to a much more complex decision problem. We prove decidability of the intruder deduction problem for an encryption which distributes over \emph{exclusive-or} with an EXPTIME procedure and we give a PTIME decision procedure relying on prefix rewrite systems for a restricted case, the \emph{binary} case.} }

@article{LugSch-IC, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe}, title = {Decidable first-order transition logics for {PA}-processes}, year = 2005, month = nov, volume = 203, number = 1, pages = {75-113}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-C2707.ps}, doi = {10.1016/j.ic.2005.02.003}, abstract = {We show the decidability of model checking PA-processes against several first-order logics based upon the reachability predicate. The main tool for this result is the recognizability by tree automata of the reachability relation. The tree automata approach and the transition logics we use allow a smooth and general treatment of parameterized model checking for PA. This approach is extended to handle a quite general notion of costs of PA-steps. In particular, when costs are Parikh images of traces, we show decidability of a transition logic extended by some form of first-order reasoning over costs.} }

@inproceedings{Orchids-cav05, address = {Edinburgh, Scotland, UK}, month = jul, year = 2005, volume = 3576, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Etessami, Kousha and Rajamani, Sriram}, acronym = {{CAV}'05}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'05)}, author = {Olivain, Julien and Goubault{-}Larrecq, Jean}, title = {The {O}rchids Intrusion Detection Tool}, pages = {286-290}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf}, doi = {10.1007/11513988_28} }

@misc{PERSEE-RC1, author = {Bardin, S{\'e}bastien and Herbreteau, Fr{\'e}d{\'e}ric and Sighireanu, Mihaela and Sutre, Gr{\'e}goire and Vincent, Aymeric}, title = {Int{\'e}gration des outils {PERS\'EE} (Proposition d'architecture)}, howpublished = {D\'elivrable~3.1~--- Partie~1 du Projet PERS\'EE de l'ACI S\'ecurit\'e Informatique}, year = 2005, month = jun, url = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf}, pdf = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf}, note = {35~pages} }

@misc{persee-miparcours05, author = {Schnoebelen, {\relax Ph}ilippe and others}, title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~--- Rapport {\`a} mi-parcours}, year = 2005, month = nov, type = {Contract Report}, note = {8~pages} }

@techreport{Prouve:rap5, author = {Bozga, Liana and Delaune, St{\'e}phanie and Klay, Francis and Vigneron, Laurent}, title = {Retour d'exp{\'e}rience sur la validation du porte-monnaie {\'e}lectronique}, institution = {projet RNTL PROUV{\'E}}, month = mar, year = 2005, type = {Technical Report}, number = 5, note = {29~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps}, abstract = {Le domaine de la mod{\'e}lisation et de la v{\'e}rification est une activit{\'e} d{\'e}licate et importante qui a connu une v{\'e}ritable explosion dans les ann{\'e}es~1990. On dispose {\`a} l'entr{\'e}e des ann{\'e}es~2000 de toute une gamme de mod{\`e}les et de m{\'e}thodes plus ou moins avanc{\'e}s en ce qui concerne l'expressivit{\'e} et l'automatisation. \par Afin de d{\'e}finir les besoins et les priorit{\'e}s {\`a} mettre sur les outils consacr{\'e}s {\`a} la v{\'e}rification de protocoles cryptographiques qui seront d{\'e}velopp{\'e}s au sein du projet RNTL PROUV{\'E}, nous proposons de travailler en situation r{\'e}elle, sur des protocoles plut{\^o}t <<~durs~>>, en effectuant le cycle suivant: mod{\'e}lisation, formalisation puis validation dans des outils existants. Ce travail est effectu{\'e} ici pour deux versions d'un protocole de porte-monnaie {\'e}lectronique, dont l'une a {\'e}t{\'e} d{\'e}velopp{\'e}e r{\'e}cemment par une {\'e}quipe de France T{\'e}l{\'e}com. Les outils retenus pour la r{\'e}alisation de cette {\'e}tude sont ProVerif, Hermes et Casrul, en raison de leurs caract{\'e}ristiques tr{\`e}s diff{\'e}rentes.} }

@techreport{Prouve:rap6, author = {Delaune, St{\'e}phanie and Klay, Francis and Kremer, Steve}, title = {Sp{\'e}cification du protocole de vote {\'e}lectronique}, institution = {projet RNTL PROUV{\'E}}, month = nov, year = 2005, type = {Technical Report}, number = 6, note = {19~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap6.ps}, abstract = {Cette nouvelle \'etude de cas a pour but de tester les limites du langage~{\scshape Prouv\'e}. En effet, le protocole que nous avons choisi d'\'etudier est volontairement complexe tant au niveau de la mod\'elisation des propri\'et\'es de s\'ecurit\'e que de la description du protocole lui-m\^eme en raison de la manipulation de structures de donn\'ees telles que les listes.\par Notre \'etude de cas est un protocole de vote qui a \'et\'e mis au point par J.~Traor\'e, ing\'enieur de recherche chez France~T\'el\'ecom. Ce protocole est bas\'e sur le m\'ecanisme de signature en aveugle et peut \^etre consid\'er\'e comme un d\'eriv\'e du protocole de Fujioka, Okamoto et~Ohta. Ce document introduit dans un premier temps le probl\`eme du vote \'electronique en g\'en\'eral avant de d\'ecrire le protocole en lui-m\^eme et sa formalisation dans le langage~{\scshape Prouv\'e}.} }

@techreport{Prouve:rap7, author = {Kremer, Steve and Lakhnech, Yassine and Treinen, Ralf}, title = {The {P}{\scshape rouv\'e} Manual: Specifications, Semantics, and Logics}, institution = {projet RNTL PROUV{\'E}}, month = dec, year = 2005, type = {Technical Report}, number = 7, note = {49~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap7.ps}, abstract = { In this report we describe the {\scshape Prouv\'e} specification language for cryptographic protocols. A main feature of the language is that it separates the roles of a protocol, which are defined in a simple imperative programming language, from the scenario which defines how instances of the roles are created.\par We give a formal semantics of the protocol specification language, and define both an expressive logics for safety conditions of protocols and a more limited assertion language.\par This version of the report~(2.0.x) describes version~2.0 of the {\scshape Prouv\'e} language.} }

@inproceedings{PinchinatRiedweg05, address = {Portland, Oregon, USA}, month = jun, year = 2005, publisher = {IEEECSP}, editor = {Balakrishnan, S. N.}, acronym = {{ACC}'05}, booktitle = {{P}roceedings of the 24th {A}merican {C}ontrol {C}onference ({ACC}'05)}, author = {Pinchinat, Sophie and Riedweg, St{\'e}phane}, title = {You Can Always Compute Maximally Permissive Controllers Under Partial Observation When They Exist}, pages = {2287-2292}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-ACC05.ps}, abstract = {The maximal permissivity property of controllers is an optimal criterion that is often taken for granted as the result of synthesis algorithms: the algorithms are designed for frameworks where the existence and the uniqueness of a maximal permissive controller is demonstrated apart, as it fulfills sufficient hypotheses; these algorithms precisely compute this object. Still, maximally permissive solutions might exist in circumstances which do not fall into such identified frameworks, but there is no way to ensure that the algorithms deliver an optimal solution. In this paper, we propose a general synthesis procedure which always computes a maximal permissive controller when it exists.} }

@inproceedings{PR-cdc05, address = {Seville, Spain}, month = dec, year = 2005, publisher = {{IEEE} Control System Society}, acronym = {{CDC-ECC}'05}, booktitle = {{P}roceedings of the 44th {IEEE} {C}onference on Decision and Control and European Control Conference ({CDC-ECC}'05)}, author = {Pinchinat, Sophie and Riedweg, St{\'e}phane}, title = {On the Architectures in Decentralized Supervisory Control}, pages = {12-17}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-cdc05.ps}, abstract = {In this paper, we clarify the notion of architecture in decentralized control, in order to investigate the realizability problem: given a discrete-event system, a desired behavior and an architecture for a decentralized control, can the desired behavior be achieved by decentralized controllers in accordance with the given architecture? We consider the problem for any mu-calculus definable behavior and for classic architectures from the literature. The method consists in compiling in a single formula both the desired behavior and the architecture. Applications of this approach are a single synthesis algorithm of decentralized controllers (with full observation) for the whole considered family of architectures, and the development of a convenient mathematical framework for a theory of decentralized control architectures.} }

@article{PR-IPL05, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Pinchinat, Sophie and Riedweg, St{\'e}phane}, title = {A Decidable Class of Problems for Control under Partial Observation}, year = 2005, month = aug, volume = 95, number = 4, pages = {454-465}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-IPL05.ps}, doi = {10.1016/j.ipl.2005.04.011} }

@phdthesis{THESE-bardin05, author = {Bardin, S{\'e}bastien}, title = {Vers un model checking avec acc{\'e}l{\'e}ration plate de syst{\`e}mes h{\'e}t{\'e}rog{\`e}nes}, year = 2005, month = oct, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bardin-THESE.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bardin-THESE.pdf} }

@phdthesis{THESE-zhang05, author = {Zhang, Yu}, title = {Cryptographic logical relations~-- What is the contextual equivalence for cryptographic protocols and how to prove~it?}, year = 2005, month = oct, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/zy-thesis.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/zy-thesis.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/zy-thesis.ps} }

@phdthesis{THESE-baclet05, author = {Baclet, Manuel}, title = {Applications du model-checking {\`a} des probl{\`e}mes de v{\'e}rification de syst{\`e}mes sur puce}, year = 2005, month = dec, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baclet.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baclet.pdf} }

@phdthesis{treinen-hab2005, author = {Treinen, Ralf}, title = {R{\'e}solution symbolique de contraintes}, year = 2005, month = nov, type = {M{\'e}moire d'habilitation}, school = {Universit{\'e} Paris-Sud~11, Orsay, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RT-habil.ps} }

@phdthesis{FL-hab2005, author = {Laroussinie, Fran{\c{c}}ois}, title = {Model checking temporis{\'e}~--- Algorithmes efficaces et complexit{\'e}}, year = 2005, month = dec, type = {M{\'e}moire d'habilitation}, school = {Universit{\'e} Paris~7, Paris, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf} }

@mastersthesis{pinot-master, author = {Pinot, Simon}, title = {Analyse de stabilit{\'e} d'algorithme distribu{\'e}s probabilistes}, school = {{M}aster de {L}ogique {M}ath{\'e}matique et {F}ondements de l'{I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = 2005, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pinot-M2.ps} }

@mastersthesis{sznajder-master, author = {Sznajder, Nathalie}, title = {Synth{\`e}se de contr{\^o}leur pour les syst{\`e}mes distribu{\'e}s synchrones}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = 2005, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf} }

@article{FL-ACMtecs05, publisher = {ACM Press}, journal = {ACM Transactions in Embedded Computing Systems}, author = {{The Artist Education Group}}, fullauthor = {Caspi, Paul and Sangiovanni-Vincentelli, Alberto L. and Almeida Lu{\'\i}s and Benveniste, Albert and Bouyssounouse, Bruno and Buttazzo, Giorgio C. and Crnkovic, Ivica and Damm, Werner and Engblom, Jakob and Fohler, Gerhard and Garc{\'\i}a-Valls, Marisol and Kopetz, hermann and Lakhnech, Yassine and Laroussinie, Fran{\c{c}}ois and Lavagno, Luciano and Lipari, Guiseppe and Maraninchi, Florence and Peti, Philipp and Antonio de la Puente, Juan and Scaife, Norman and Sifakis, Joseph and de{ }Simone, Robert and T{\"o}rngren, Martin and Ver{\'\i}ssimo, Paulo and Wellings, Andy J. and Wilhelm, Reinhard and Willemse, Tim A. C. and Yi, Wang}, title = {Guidelines for a graduate curriculum on embedded software and systems}, volume = 4, number = 3, year = 2005, month = aug, pages = {587-611}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf}, doi = {10.1145/1086519.1086526}, abstract = {The design of embedded real-time systems requires skills from multiple specific disciplines, including, but not limited to, control, computer science, and electronics. This often involves experts from differing backgrounds, who do not recognize that they address similar, if not identical, issues from complementary angles. Design methodologies are lacking in rigor and discipline so that demonstrating correctness of an embedded design, if at all possible, is a very expensive proposition that may delay significantly the introduction of a critical product. While the economic importance of embedded systems is widely acknowledged, academia has not paid enough attention to the education of a community of high-quality embedded system designers, an obvious difficulty being the need of interdisciplinarity in a period where specialization has been the target of most education systems. This paper presents the reflections that took place in the European Network of Excellence Artist leading us to propose principles and structured contents for building curricula on embedded software and systems.} }

@techreport{FGRV-ulb05, author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and Van{~}Begin, Laurent}, title = {A counter-example the the minimal coverability tree algorithm}, institution = {Universit\'e Libre de Bruxelles, Belgium}, year = {2005}, number = {535}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf}, abstract = {In [Finkel, 1993], an~algorithm to compute a minimal coverability tree for Petri nets has been presented. This document demonstrates, thanks to a simple counter-example, that this algorithm may compute an under-approximation of a coverability tree, i.e., a~tree whose set of nodes is not sufficient to cover all the reachable markings.} }

@article{BC-JALC2005, journal = {Journal of Automata, Languages and Combinatorics}, author = {Bouyer, Patricia and Chevalier, Fabrice}, title = {On Conciseness of Extensions of Timed Automata}, year = 2005, volume = 10, number = 4, pages = {393-405}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC05-jalc.ps}, abstract = {In this paper we study conciseness of various extensions of timed automata, and prove that several features like diagonal constraints or updates lead to exponentially more concise timed models.} }

@misc{bouyer-cortos06, author = {Bouyer, Patricia}, title = {Weighted Timed Automata: Model-Checking and Games}, year = {2005}, month = aug, howpublished = {Invited talk, Workshop CORTOS'06, Bonn, Germany} }

@misc{bouyer-avocs05, author = {Bouyer, Patricia}, title = {Optimal Timed Games}, year = {2005}, month = sep, howpublished = {Invited talk, 5th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'05), Warwick, UK} }

@misc{bouyer-infinity05, author = {Bouyer, Patricia}, title = {Optimal Reachability Timed Games}, year = {2005}, month = aug, howpublished = {Invited talk, 7th {I}nternational {W}orkshop on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'05), San Francisco, USA} }

@inproceedings{bouyer-etr05, address = {Nancy, France}, month = sep, year = 2005, noeditor = {}, acronym = {{ETR}'05}, booktitle = {{A}ctes de la 4{\`e}me {\'E}cole {T}emps-{R}{\'e}el ({ETR}'05)}, author = {Bouyer, Patricia}, title = {An Introduction to Timed Automata}, pages = {111-123}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf} }

@inproceedings{bouyer-artist2-05, author = {Bouyer, Patricia}, title = {Foundations of Timed Systems}, booktitle = {Proc. of the ARTIST2 Summer School on Component \& Modelling, Testing \& Verification, and Statical Analysis of Embedded Systems}, address = {N{\"a}sslingen, Sweden}, month = sep # {-} # oct, year = {2005}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf} }

@misc{Demri0506, author = {Demri, St{\'e}phane}, title = {Temporal logics}, year = {2005}, note = {Course notes, {M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf} }

@mastersthesis{bouchy-master, author = {Bouchy, Florent}, title = {Biblioth{\`e}que de m{\'e}thodes pour la classification}, school = {{M}aster {R}echerche {I}nformatique, Tours, France}, type = {Rapport de {M}aster}, year = 2005, month = sep }

@comment{{B-arxiv16, author = Bollig, Benedikt, affiliation = aff-LSVmexico, title = One-Counter Automata with Counter Visibility, institution = Computing Research Repository, number = 1602.05940, month = feb, nmonth = 2, year = 2016, type = RR, axeLSV = mexico, NOcontrat = "", url = http://arxiv.org/abs/1602.05940, PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf", lsvdate-new = 20160222, lsvdate-upd = 20160222, lsvdate-pub = 20160222, lsv-category = "rapl", wwwpublic = "public and ccsb", note = 18~pages, abstract = "In a one-counter automaton (OCA), one can read a letter from some finite alphabet, increment and decrement the counter by one, or test it for zero. It is well-known that universality and language inclusion for OCAs are undecidable. We consider here OCAs with counter visibility: Whenever the automaton produces a letter, it outputs the current counter value along with~it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are in PSPACE, thus no harder than the corresponding problems for finite automata, which can actually be considered as a special case. In fact, we show that OCAs with counter visibility are effectively determinizable and closed under all boolean operations. As~a~strict generalization, we subsequently extend our model by registers. The general nonemptiness problem being undecidable, we impose a bound on the number of register comparisons and show that the corresponding nonemptiness problem is NP-complete.", }}

*This file was generated by
bibtex2html 1.98.*