BEGIN:VCALENDAR VERSION:2.0 CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALNAME:Events at LSV X-WR-TIMEZONE:Europe/Paris BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 TZNAME:CEST DTSTART:19700329T020000 RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET DTSTART:19701025T030000 RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU END:STANDARD END:VTIMEZONE BEGIN:VEVENT SUMMARY: 15th LSV Anniversary and Silver Medal Celebration for Jean G oubault-Larrecq STATUS:CONFIRMED DESCRIPTION: LSV organises a Festive Workshop on 6–7 February 2012 on t he occasion of the 15th Anniversary of the Laboratory and in celebration of the CNRS Silver Medal awarded to Jean Goubau lt-Larrecq. DTSTART;VALUE=DATE:20120206 DURATION:P2D URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Events/LSV15Y/ UID:LSVLSV15Y@lsv.ens-cachan.fr LOCATION:ENS Cachan (France) END:VEVENT BEGIN:VEVENT SUMMARY: Laurent Doyen defends his habilitation thesis STATUS:CONFIRMED ATTENDEE;CN="Laurent Doyen": MAILTO:no@spam.com DESCRIPTION: Games and Automata: From Boolean to Quantitative Verificati on Tuesday\, 13 March 2013\, at 14:30 Pavillon des Jardins\, ENS Cachan DTSTART;TZID=Europe/Paris:20120313T100000 DURATION:PT7H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Events/ctsv/ UID:LSVhdrLaurentD@lsv.ens-cachan.fr LOCATION:Pavillon des Jardins END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Alexander Heußner": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120410T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204101 100 UID:LSVsemLSV.201204101100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Amélie Gheerbrant": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120403T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204031 100 UID:LSVsemLSV.201204031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="David Baelde": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120322T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203221 100 UID:LSVsemLSV.201203221100@lsv.ens-cachan.fr LOCATION:Salle ? END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Cezara Drăgoi": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120320T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203201 100 UID:LSVsemLSV.201203201100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Barnaby Martin": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120312T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203121 400 UID:LSVsemLSV.201203121400@lsv.ens-cachan.fr LOCATION:Amphithéâtre 121 N (Bâtiment Léonard de Vinci) END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Tobias Heindel": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120306T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203061 400 UID:LSVsemLSV.201203061400@lsv.ens-cachan.fr LOCATION:Salle ? END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Emmanuel Filiot": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120306T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203061 100 UID:LSVsemLSV.201203061100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: (to be announced) STATUS:TENTATIVE ATTENDEE;CN="Mathieu Sassolas": MAILTO:no@spam.com DESCRIPTION: DTSTART;TZID=Europe/Paris:20120228T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202281 100 UID:LSVsemLSV.201202281100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Tolerating Transient\, Permanent\, and Intermittent Failures STATUS:CONFIRMED ATTENDEE;CN="Swan Dubois": MAILTO:no@spam.com DESCRIPTION: When the size of a distributed system gets larger or when it is deployed in hazardous environments\, the possibility tha t some elements of the system are subject to faults (failure \, memory corruption\, hacking\, ...) become impossible to e lude. Faults can be classified according to duration\, span\ , or nature. In this talk\, we focus on distributed systems that simultaneously tolerate several kinds of faults using t hree classical problems as case studies. We present first a distributed protocol simulating a single-writer multi-reader atomic register in the presence of transient faults and of permanent crash faults. This protocol relies on two re-usabl e tools: a communication primitive and a bounded timestamp s cheme. Then\, we study logical clock weak synchronization in the presence of transient faults and of intermittent Byzant ine faults. We prove several impossibility results and provi de a protocol that is optimal both with respect to impossibi lity result and with respect to recovery time. Finally\, we define three new fault tolerance schemes in distributed syst ems that are subject to transient faults and to intermittent Byzantine faults. We design a protocol constructing a wide class of spanning trees that is optimal with respect to faul t tolerance metrics defined for these three schemes. DTSTART;TZID=Europe/Paris:20120216T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202161 400 UID:LSVsemLSV.201202161400@lsv.ens-cachan.fr LOCATION:Salle ? END:VEVENT BEGIN:VEVENT SUMMARY: Better abstractions for timed automata STATUS:CONFIRMED ATTENDEE;CN="B Srivathsan": MAILTO:no@spam.com DESCRIPTION: We consider the reachability problem for timed automata. A s tandard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstracti ons preserve underlying simulation relations on the state sp ace of the automaton. For both effectiveness and efficiency reasons\, they are parametrized by the maximal lower and upp er bounds (LU-bounds) occurring in the guards of the automat on. We consider the A-lu abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets\, it has not been used in implementations. We prove tha t A-lu abstraction is the biggest abstraction with respect t o LU-bounds that is sound and complete for reachability. We also provide an efficient technique to use the A-lu abstract ion to solve the reachability problem. Joint work with Fréd éric Herbreteau and Igor Walukiewicz. DTSTART;TZID=Europe/Paris:20120214T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202141 100 UID:LSVsemLSV.201202141100@lsv.ens-cachan.fr LOCATION:Amphithéâtre Tocqueville END:VEVENT BEGIN:VEVENT SUMMARY: Counter-Example Guided Fence Insertion under TSO STATUS:CONFIRMED ATTENDEE;CN="Mohamed Faouzi Atig": MAILTO:no@spam.com DESCRIPTION: We consider the reachability problem for concurrent finite-s tate programs running under the classical TSO memory model. This model allows "write to read" relaxation corresponding t o the addition of an unbounded store buffer between each pro cessor and the main memory. We show that the reachability pr oblem for a program under TSO is decidable. Then\, we propos e a counter-example guided fence insertion procedure. The pr ocedure is augmented by a placement constraint that allows t he user to choose places inside the program where fences may be inserted. For a given placement constraint\, we automati cally infer all minimal sets of fences that ensure correctne ss. We have implemented a prototype and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing meth ods. [This talk will be based on: (1) POPL'10 paper with Ahm ed Bouajjani\, Burckhardt and Madanlal Musuvathi\, and (2) T ACAS'12 paper with Parosh Abdulla\, Yu-Fang Chen\, Carl Leon ardsson and Ahmed Rezine] DTSTART;TZID=Europe/Paris:20120131T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201311 100 UID:LSVsemLSV.201201311100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Component-based analysis of real-time systems STATUS:CONFIRMED ATTENDEE;CN="Giuseppe Lipari": MAILTO:no@spam.com DESCRIPTION: The complexity of modern embedded real-time systems is const antly increasing\, as new and more complex functionality is added to existing software. At the same time\, due to the in creasing computational power of the hardware platforms and t o the pressure to reduce the costs\, software that in the pa st was run on different computational nodes\, is now being i ntegrated onto a single node. An appealing way to reduce com plexity is to apply a component-based real-time design metho dology. A real-time system can be seen as a set of interacti ng components\, each one providing a well-defined subset of functionalities\, whose integration produces the final syste m behavior. A component-based methodology is successful only if it can effectively reduce the complexity. To achieve thi s goal\, the system designer must be able to 1) analyze and validate each component in isolation from the rest of the sy stem\, 2) summarize its properties and requirements into sim pler interfaces\, 3) perform the final integration analysis and validation on the component interfaces. In this talk\, t he author will give an overview of current techniques for co mponent-based analysis of real-time systems\, with a look at their possible use in avionics and automotive systems. Then \, a possible research agenda will be discussed\, highlighti ng the shortcomings of current analysis and how to improve o n it. DTSTART;TZID=Europe/Paris:20120124T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201241 100 UID:LSVsemLSV.201201241100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Everlasting Security through Quantum Cryptography STATUS:CONFIRMED ATTENDEE;CN="Dominique Unruh": MAILTO:no@spam.com DESCRIPTION: Cryptography is a powerful tool for processing confidential data. Cryptographic protocols are\, however\, only as secure as the underlying encryption schemes. And we do not know wh ether these might not be broken at some point in the future. This leaves us in a difficult situation: If we process high ly sensitive data using cryptographic protocols\, an attacke r might simply record all messages. Should the underlying en cryption scheme be broken in the future\, the attacker will then be able to decrypt all confidential data in retrospect. For highly confidential data (such as\, e.g.\, medical reco rds) such a situation is not acceptable. A way out is "everl asting security". A protocol with everlasting security guara ntees that all data involved in the protocol stays secure\, even if at some point in the future all the underlying encry ption schemes are broken. Unfortunately\, with traditional c ryptographic techniques\, everlasting security can only be a chieved in very limited situations. In this talk\, we explai n how everlasting security can be achieved for a wide variet y of tasks by using quantum cryptography\, i.e.\, by making use of quantum mechanical effects in the cryptographic proto col. DTSTART;TZID=Europe/Paris:20120117T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201171 100 UID:LSVsemLSV.201201171100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Cryptanalysis STATUS:CONFIRMED ATTENDEE;CN="Pierre-Alain Fouque": MAILTO:no@spam.com DESCRIPTION: Cryptanalysis is a set of methods to circumvent the security of cryptographic algorithms. It can be applied at different levels: at the assumption level\, attacking the computation ally-hard problem on which the security of a scheme is based ; at the scheme level\, attacking the scheme directly when i ts security is not based on some hard problems (this is the case when specific instances of a hard problems are used) or in symmetric cryptography; finally at the implementation le vel\, when side channel information can be used. In this tal k\, I will make a survey of some cryptanalytic techniques an d describe my contributions towards this field. DTSTART;TZID=Europe/Paris:20111129T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111291 400 UID:LSVsemLSV.201111291400@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Uniform strategies STATUS:CONFIRMED ATTENDEE;CN="Sophie Pinchinat": MAILTO:no@spam.com DESCRIPTION: Imperfect information games are becoming very popular for th eir ability to model interaction under uncertainty. Examples of this kind of situations are many\, e.g. distributed feat ures of computing systems\, attacker's dialog with a securit y system\, etc. Also\, such games naturally arise in logic\, e.g. as satisfiability games for mu-calculus formulas. Rece ntly\, some kind of imperfect information games have been us ed to provide the semantics of logics\, as for Dependence Lo gic. We propose the notion of "uniform strategy" which unifi es the aforementioned approaches\, and even provides new mod el-checking games for complex logics\, e.g. combining time a nd knowledge. Our definition relies on pairs of parameters : an equivalence relation between plays\, and a uniformity co ndition over sets of equivalent plays. Basically\, a strateg y is uniform if the equivalence class of any play induced by the strategy satisfies the uniformity condition. For exampl e\, the equivalence can arise from a player ability to obser ve and recall what happened during the play (The perfect rec all-imperfect recall spectrum lies in this parameter). Addit ionally\, the uniformity condition can express many aspects. It can capture the nature of the strategy\, e.g. that it is observation-based\, as needed in the very standard imperfec t information games setting. It can characterize non-regular properties of strategies\, e.g. that strategies maintain th e opponent's uncertainty about some secret\, as considered i n games with opacity condition. In this talk\, we will expla in and motivate our notion of uniform strategy\, and relate it to various examples from the literature: namely\, imperfe ct information games\, games with opacity condition\, emptin ess of alternating automata\, first-order dependence logic m odel-checking games\, epistemic temporal logic model-checkin g games. If time left\, we will address decidability and com plexity issues by scanning computational hypothesis one may require on the pair of parameters. DTSTART;TZID=Europe/Paris:20111129T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111291 100 UID:LSVsemLSV.201111291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: The Computational Complexity of Verifying One-Counter Proces ses STATUS:CONFIRMED ATTENDEE;CN="Stefan Göller": MAILTO:no@spam.com DESCRIPTION: A one-counter automaton is a pushdown automaton over a singl eton stack alphabet plus a bottom-of-stack symbol. I will ta lk about equivalence checking and model checking of processe s generated by one-counter automata\, so-called one-counter processes (OCPs). The goal of the talk is to present some id eas and techniques that are used for obtaining complexity bo unds for these problems. In the first part of the talk I pla n to show that it is PSPACE-complete to decide strong bisimu lation equivalence for OCPs. The previously best known upper bound for this problem was 3-EXPSPACE. The same problem tur ns out to be NL-complete when the processes are described by deterministic one-counter automata. In the second part of t he talk\, I plan to discuss a technique for proving lower bo unds by employing two known results from complexity theory: (i) Converting a natural number in Chinese remainder present ation into binary presentation is in logspace-uniform NC^1 a nd (ii) PSPACE is AC^0-serializable. With the latter one can prove that there exists a fixed CTL formula for which model checking of OCPs is PSPACE-hard. With the same technique on e can show some further lower bounds\, as for example the fo llowing one: The emptiness problem for timed automata with t wo clocks but with modulo tests is PSPACE-complete even if a ll numbers are encoded in unary. The results were obtained i n joint works with Stanislav Böhm\, Petr Jancar and Markus Lohrey. DTSTART;TZID=Europe/Paris:20111122T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111221 100 UID:LSVsemLSV.201111221100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Symbolic Methods for the Automatic Search of Attacks Against Some Block Ciphers STATUS:CONFIRMED ATTENDEE;CN="Charles Bouillaguet": MAILTO:no@spam.com DESCRIPTION: The block cipher cryptanalyst usually faces the following pr oblem: she may interact with a black box containing the bloc k cipher instantiated with a secret random key\, and her goa l is\, in most cases\, to retrieve this secret key using les s time than exhaustive search and asking less encryptions/de cryptions to the black box than the whole codebook. Several researchers had previously observed that the Advanced Encryp tion Standard (AES)\, the most widespread block cipher\, had a relatively simple algebraic description over the field wi th 256 elements\, because of its byte-oriented design. Howev er\, this property has not been harnessed by cryptanalysts t o this day. In particular the (tempting) approach consisting in writing down the equations describing the AES\, and tryi ng to solve them directly using off-the-shelf tools such as SAT-solvers\, has systematically failed to provide any resul t. In this talk\, I will present the results we obtained usi ng a slightly different method. We have designed tools that take as input a system of AES-like equations\, and that sear ch for an efficient ad hoc solving procedure. The result of these tools is the source code of a solver that can only sol ve the input system\, but which can in some cases be efficie nt (its complexity can be predicted accurately). This solver can then be compiled and run to find the actual solutions. Our tools\, which "reason" from the equations describing the AES (or similar looking symmetric primitives) are intrinsic ally symbolic\, and they are inspired by standard tools from the field of automated deduction\, such as the DPLL algorit hm for SAT\, the Knuth-Bendix completion algorithm\, or the resolution algorithm for first-order logic. These tools foun d\, nearly automatically\, the best known Low-Data-Complexit y attacks on reduced versions of the AES\, and the best know n attack on the full versions of AES-derived primitives\, su ch as the Message Authentication code Pelican-MAC\, and the stream cipher LEX. DTSTART;TZID=Europe/Paris:20111115T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111151 100 UID:LSVsemLSV.201111151100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Logico-Numerical Abstract Acceleration and Application to th e Verification of Data-Flow Programs STATUS:CONFIRMED ATTENDEE;CN="Peter Schrammel": MAILTO:no@spam.com DESCRIPTION: We are interested in the verification of safety properties a bout synchronous data-flow programs with Boolean and numeric al variables\, e.g.\, Lustre programs. We rely on reachable- state analysis for this problem. Two main techniques for ens uring the termination of such an analysis are acceleration a nd widening (within the abstract interpretation framework). Acceleration-based methods lead to exact results\, but they guarantee termination only for a restricted class of program s. Widening is less precise and less predictable but does no t have this limitation. Abstract acceleration integrates acc eleration techniques into the abstract interpretation framew ork\, such as to reduce the need for widening and thus to im prove precision. All these techniques however require the en umeration of the Boolean state-space\, which leads to a stat e-space explosion even for medium-sized Lustre programs. In this talk we propose a solution by extending numerical accel eration to logico-numerical acceleration. We define logico-n umerical abstract acceleration methods based on a partial de coupling of Boolean and numerical transitions and we show ho w well-chosen partitioning techniques make them effective. E xperimental results show that incorporating these methods in a verification tool based on abstract interpretation provid es not only significant advantage in terms of precision\, bu t also a gain in performance. DTSTART;TZID=Europe/Paris:20111108T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111081 100 UID:LSVsemLSV.201111081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Toward Machine-Checked Program Verification for Concrete Cry ptography STATUS:CONFIRMED ATTENDEE;CN="Pierre-Yves Strub": MAILTO:no@spam.com DESCRIPTION: Type systems\, relational logics\, and interactive proof ass istants are effective tools for verifying the security of pr ograms and systems that rely on cryptography. They can provi de automation\, modularity and scalability. As illustrated i n recent case studies\, they can be usefully applied to larg e security protocols and applications [Bhargavan et al.\, 20 08\, Fournet et al.\, 2009]. However\, their models traditio nally rely on abstract assumptions on the underlying cryptog raphic primitives\, expressed in symbolic models. Cryptograp hers usually reason on security assumptions in lower-level m odels that precisely account for the complexity and probabil ity of attacks. These models are more complex and realistic\ , but recent results suggest thay they are also amenable to formal automated verification [Blanchet\, 2006\, Barthe et a l.\, 2009\, Acar et al.\, 2011]. I will present our on-going work in adapting and extending our programming and verifica tion framework based on refinement types for ML programs [Be ngtson et al.\, 2008\, Bhargavan et al.\, 2010\, Fournet\, 2 011] which currently uses a combination of automated proofs (using Z3\, an SMT solver) and interactive proofs (using Coq )\, in order to produce machine-checked security proofs of c ryptographic programs and libraries under concrete computati onal assumptions. This work is part of the “Secure Distrib uted Computations” group of the “MSR-INRIA Joint Centre . DTSTART;TZID=Europe/Paris:20110927T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201109271 100 UID:LSVsemLSV.201109271100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Keeping track of your friends and enemies: privacy threats o f new mobile technologies STATUS:CONFIRMED ATTENDEE;CN="Myrto Arapinis": MAILTO:no@spam.com DESCRIPTION: Joint work with Loretta Mancini\, Eike Ritter\, and Mark Rya n. The proliferation of portable computing devices\, such as mobile phones\, Bluetooth devices\, and RFID tags\, has lea d to a range of new computer security problems. In order to fulfil their goals\, these devices need to report our moveme nts to service providers such as mobile phone network operat ors\, banks\, and governments. While most of users accept th at the service providers can track their physical movements\ , few would be happy if an arbitrary third party could do so . Such a possibility would enable all kinds of undesirable b ehaviours\, ranging from criminal stalking to more mundane m onitoring of spouse or employee movements. For this reason\, protocols have been designed to prevent third parties from identifying wireless messages as coming from a particular us er. These protocols usually include cryptography and make us e of temporary identifiers\, in an effort to achieve the aim of untraceability by third parties. At CSF'10\, we presente d a formal framework for analysing untraceability/unlinkabil ity in the applied pi calculus. We used our framework to sho w that French e-Passports are traceable\, while British ones aren't. In this talk\, I will present you our work on the a nalysis of Universal Mobile Telecommunication System (UMTS) protocols. I will show you a problem we have identified with the UMTS authentication and key establishment protocol: alt hough mobile phones use temporary identities to identify the mselves to the Network\, a replayed message can be used to i dentify a particular mobile phone. Our attack exploits the f act that the victim's phone will reply with subtly different error messages\, depending on whether the replayed request is associated with it or with a different phone. To thwart t his attack\, we propose a modification of the protocol\, and verify the proposed fix using our framework and the ProVeri f tool. DTSTART;TZID=Europe/Paris:20110920T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201109201 100 UID:LSVsemLSV.201109201100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Verification of Ad hoc Networks: Unreliability and Time STATUS:CONFIRMED ATTENDEE;CN="Giorgio Delzanno": MAILTO:no@spam.com DESCRIPTION: In the first part of the talk we present an analysis of veri fication problems\, formulated as parameterized reachability \, for an abstract model of Ad Hoc Network protocols in pres ence of node and communication failures. We consider here di fferent types of failures: intermittency\, crash and restart of single nodes\, loss and conflicts of broadcast messages. In the second part we present an extension of the model in which nodes are specified by timed automata and\, for the ne w model\, discuss parameterized reachability problems for di fferent classes of topologies. DTSTART;TZID=Europe/Paris:20110712T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201107121 100 UID:LSVsemLSV.201107121100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Reasoning about Web Security STATUS:CONFIRMED ATTENDEE;CN="Tamara Rezk": MAILTO:no@spam.com DESCRIPTION: Mixing existing online libraries and data into new online ap plications in a rapid\, inexpensive manner\, often referred to as mashups\, has captured the way of designing web applic ations. In this talk\, I will: overview security vulnerabili ties that arise from web applications specificities such as code injection and gadget inclusion; and describe proposals based on language-based security approaches. DTSTART;TZID=Europe/Paris:20110705T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201107051 100 UID:LSVsemLSV.201107051100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Coalgebraic Logics and Tableaux STATUS:CONFIRMED ATTENDEE;CN="Clemens Kupke": MAILTO:no@spam.com DESCRIPTION: Many of the logics that are used in computer science today a re variations of modal logics as they offer a good compromis e between expressive power on the one hand\, and good algori thmic properties on the other hand. Extensions of basic moda l logic are obtained by allowing for ontological reasoning ( description logics) and by adding the ability to specify ong oing\, possibly infinite behaviour (fixpoint logics). Other variations of basic modal logic are designed to fit specific semantic domains such as modal logics for Markov chains\, g ame frames or neighbourhood structures. In my talk I am goin g to present coalgebraic modal logic as a general framework in which the above mentioned variations of basic modal logic can be studied in a uniform way. In particular\, I am going to describe tableau calculi that yield generic decidability proofs for the coalgebraic mu-calculus and coalgebraic desc ription logics. As corollaries we obtain previously unknown Exptime-decidability results for these logics. DTSTART;TZID=Europe/Paris:20110614T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201106141 100 UID:LSVsemLSV.201106141100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Beyond Control-State Reachability for Communicating Pushdown Systems STATUS:CONFIRMED ATTENDEE;CN="Alexander Heußner": MAILTO:no@spam.com DESCRIPTION: Pushdown systems synchronizing by unbounded\, reliable fifo queues seem a quite natural model for distributed systems th at communicate via TCP or MPI. Recent publications focus on the influence of constraining the network architecture on ba sic decidability questions\, but do not allow to derive posi tive results beyond control-state reachability when assuming syntactic and semantic restrictions that are still "applica ble" in practice. We present first ideas on leaving behind i nterleaving semantics in order to verify MSO properties base d on a graph grammar based representation of a system's part ial-order behaviour. DTSTART;TZID=Europe/Paris:20110531T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105311 100 UID:LSVsemLSV.201105311100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Assembling Sessions STATUS:CONFIRMED ATTENDEE;CN="Madhavan Mukund": MAILTO:no@spam.com DESCRIPTION: Sessions are a central paradigm in Web services\, as they al low the implementation of decentralized transactions with mu ltiple participants. Sessions enable the cooperation of work flows while at the same time avoiding the mixing of workflow s from distinct transactions. Several languages such as BPEL \, ORC\, AXML have been proposed to implement Web Services. Sessions are usually implemented by attaching unique identif iers to transactions. The expressive power of these language s makes the properties of the implemented services undecidab le. In this talk\, we propose a new formalism for modelling web services. Our model is session-based\, but avoids using session identifiers. The model can be translated to a dialec t of Petri nets that allows the verification of important pr operties of web services in terms of coverability in Petri n ets. This is joint work with Philippe Darondeau and Loic Hel ouet. DTSTART;TZID=Europe/Paris:20110524T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105241 100 UID:LSVsemLSV.201105241100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Approximating Hybrid Systems STATUS:CONFIRMED ATTENDEE;CN="Mahesh Viswanathan": MAILTO:no@spam.com DESCRIPTION: he widespread deployment of computing devices that manage an d control physical processes in safety critical environments \, has made their analysis and verification a very important problem. Since formal models that disregard the physical pr ocesses tend to be conservative and suboptimal\, the most po pular way to model and analyze such systems is using hybrid systems\, that have finitely many control states to model di screte behavior and finitely many real valued variables that evolve continuously with time to model the interaction with the physical world. Despite considerable progress in the la st couple of decades\, the automated verification of cyber p hysical systems remains stubbornly challenging. In this talk we will discuss one approach to making the analysis more sc alable\, namely\, by automatically constructing "simpler"\, "smaller" models\, and then analysing these approximated mod els. We will present a couple of techniques to approximate h ybrid models\, based on the Stone-Weierstrauss Theorem and c ounter-example guided abstraction-refinement (CEGAR)\, and d iscuss their applications to automated verification. DTSTART;TZID=Europe/Paris:20110517T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105171 100 UID:LSVsemLSV.201105171100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Towards better tools for the analysis and quality assurance of FOSS distributions STATUS:CONFIRMED ATTENDEE;CN="Ralf Treinen": MAILTO:no@spam.com DESCRIPTION: Free and Open Source Software (FOSS) distributions are among the largest and fastest moving existing component-based sof tware distributions\, which poses interesting challenges bot h for the quality assurance process of distributions as for the management of individual installations. The first part o f this talk will give an overview of some of the results obt ained in the EDOS and Mancoosi European projects on the anal ysis of inter-package relationships. We will focus on the to ols that came out of these research projects\, and discuss t he way how these are currently put to use. In the second par t of the talk I will present recent results on deciding prop erties that range over all possible future evolutions of a c urrent component repository. The properties we are intereste d in concern the coherent component installations permitted in any future. We show that a certain class of these propert ies can be decided by checking a finite set of repositories that is representative for the infinite set of all possible futures. We discuss our implementation of tools checking two particular instances of this schema. DTSTART;TZID=Europe/Paris:20110426T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104261 100 UID:LSVsemLSV.201104261100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Playing games when states have rich structure STATUS:CONFIRMED ATTENDEE;CN="Lukasz Kaiser": MAILTO:no@spam.com DESCRIPTION: Both in the classical theory of extensive-form games and in the more recent theory of games on graphs it is normally ass umed that a state of the game has no structure beyond the ou tgoing moves. In other words\, the internal structure of the states is abstracted away. This is very useful in some case s\, but can be a hindrance in others\, for example when stud ying games on pushdown graphs or on timed automata. To bette r understand how internal structure of the states can influe nce behaviour of the players\, we introduce a general model of games with structured states. In our model\, actions of t he players are given by structure rewriting rules and winnin g conditions by logic formulas. In case of games with perfec t information\, we show that the structure of the states can be exploited to create simple strategies\, sometimes even w hen the number of states in the game is infinite. This is si milar to games on pushdown graphs and indeed\, we prove a cl ose relationship between pushdown games and our model when r ewriting rules are of a certain simple form. DTSTART;TZID=Europe/Paris:20110412T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104121 100 UID:LSVsemLSV.201104121100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Pattern-based Verification for Multithreaded Programs STATUS:CONFIRMED ATTENDEE;CN="Pierre Ganty": MAILTO:no@spam.com DESCRIPTION: Pattern-based verification checks the correctness of the pro gram executions that follow a given pattern\, a regular expr ession over the alphabet of program transitions of the form w1* ... wn*. For multithreaded programs\, the alphabet of th e pattern is given by the synchronization operations between threads. After introducing the model\, we study the complex ity of pattern-based verification for abstracted multithread ed. While unrestricted verification is undecidable for abstr acted multithreaded programs with recursive procedures and P SPACE-complete for abstracted multithreaded while-programs\, we show that pattern-based verification is NP-complete for both classes. Using recent results about Parikh images of co ntext-free languages and semilinear sets\, we show that patt ern-based verification becomes polynomial when the number of threads\, the longest acyclic path in the call graph\, and the size of the pattern are fixed\, but the procedures can s till be arbitrarily large. DTSTART;TZID=Europe/Paris:20110405T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104051 100 UID:LSVsemLSV.201104051100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Entropy of timed languages STATUS:CONFIRMED ATTENDEE;CN="Eugene Asarin": MAILTO:no@spam.com DESCRIPTION: For timed languages\, we define measures of their size: volu me for a fixed finite number of events\, and entropy (growth rate) as asymptotic measure for an unbounded number of even ts. These measures can be used for comparison of languages\, and the entropy can be viewed as information contents of a timed language. In case of languages of deterministic timed automata\, we give exact formulas for volumes. Next we chara cterize the entropy\, using methods of functional analysis\, as a logarithm of the leading eigenvalue (spectral radius) of a positive integral operator. We devise several methods t o compute the entropy: a symbolical one for so-called "1 1/2 -clock" automata\, and two numerical ones: one using techniq ues of functional analysis\, another based on discretization . (The talk is based on Concur'09\, FORMATS'09\, FSTTCS'10 a rticles with Aldric Degorre) DTSTART;TZID=Europe/Paris:20110322T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201103221 100 UID:LSVsemLSV.201103221100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Residuation of tropical series: rationality issues STATUS:CONFIRMED ATTENDEE;CN="Anne Bouillard": MAILTO:no@spam.com DESCRIPTION: Decidability of existence\, rationality of delay controllers and robust delay controllers are investigated for systems w ith time weights in the tropical and interval semirings. Dep ending on the (max\,+) or (min\,+)-rationality of the series specifying the controlled system and the control objective\ , cases are identified where the controller series defined b y residuation is rational\, and when it is positive (i.e.\, when delay control is feasible). When the control objective is specified by a tolerance\, i.e. by two bounding rational series\, a nice case is identified in which the controller s eries is of the same rational type as the system specificati on series. DTSTART;TZID=Europe/Paris:20110308T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201103081 100 UID:LSVsemLSV.201103081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: A Logical Framework for Capturing the Dynamics of Informatio n and Abilities of Players in Multi-Player Games: a prelimin ary report STATUS:CONFIRMED ATTENDEE;CN="Valentin Goranko": MAILTO:no@spam.com DESCRIPTION: I will discuss first steps towards a more realistic treatmen t and logical formalization of the abilities of players to a chieve objectives in multi-player games under incomplete\, i mperfect\, or simply wrong information that they may have ab out the game and about the course of the play. In this talk\ , after some motivating examples I will introduce a variatio n of the multi-agent logic ATL as a logical framework for ca pturing the interplay between the dynamics of information an d the dynamics of abilities of players. This framework takes into account both the a priori information of players with respect to the game structure and the empirical information that players develop over the course of an actual play. It a ssociate with them respective information relations and noti ons of `a priori' and `empirical' strategies and strategic a bilities. I will discuss the problem of model checking of st atements formalized in the new logic under different assumpt ions about the abilities of the players to observe\, remembe r\, and reason. Most of the talk will be based on a joint wo rk with Peter Hawke (now at Stanford Univ.) DTSTART;TZID=Europe/Paris:20110222T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102221 100 UID:LSVsemLSV.201102221100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Proving that programs eventually do something good STATUS:CONFIRMED ATTENDEE;CN="Byron Cook": MAILTO:no@spam.com DESCRIPTION: Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing)\, a nd those that result in the software not doing something use ful (e.g. hanging). In recent years automatic tools have bee n developed which use mathematical proof techniques to certi fy that software cannot crash. But\, based on Alan Turing's proof of the halting problem's undecidablity\, many have con sidered the dream of automatically proving the absence of ha ngs to be impossible. While not refuting Turing's original r esult\, recent research now makes this dream a reality. This lecture will describe this recent work and its application to industrial software. Bio: Dr. Byron Cook is a Principal R esearcher at Microsoft Research in Cambridge\, UK as well as Professor of Computer Science at Queen Mary\, University of London. He is one of the developers of the Terminator progr am termination proving tool\, as well as the SLAM software m odel checker. See research.microsoft.com/~bycook/ for more i nformation. DTSTART;TZID=Europe/Paris:20110218T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102181 100 UID:LSVsemLSV.201102181100@lsv.ens-cachan.fr LOCATION:Amphithéâtre Marie Curie (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT SUMMARY: Recursion Schemes and their Automata Models STATUS:CONFIRMED ATTENDEE;CN="Olivier Serre": MAILTO:no@spam.com DESCRIPTION: In this talk\, I will present two equi-expressive models for generating infinite trees. The first one are higher-order r ecursion schemes\, which can be thought as a deterministic r ewriting system over terms (essentially\, the simply-typed l ambda calculus with recursion). The second one are higher-or der pushdown automata\, which are an extension of pushdown a utomata that uses stacks of stacks instead of stacks of symb ols. The first part of the talk will be devoted to present t he models and give examples. The second part\, will focus on properties of the trees generated by such models (in partic ular\, the decidability of the monadic second order logic)\, and will illustrate the advantages of automata techniques w hen working with such objects. DTSTART;TZID=Europe/Paris:20110215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102151 100 UID:LSVsemLSV.201102151100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Temporal logics over linear time domains are in PSPACE STATUS:CONFIRMED ATTENDEE;CN="Alexander Rabinovich": MAILTO:no@spam.com DESCRIPTION: We investigate the complexity of the satisfiability problem of temporal logics with a finite set of modalities. We show that the problem is in PSPACE over the class of all linear o rders\, over rationals\, over the reals and over many intere sting classes of linear orders. DTSTART;TZID=Europe/Paris:20110125T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201101251 100 UID:LSVsemLSV.201101251100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Symbolic Techniques in Propositional Satisfiability Solving STATUS:CONFIRMED ATTENDEE;CN="Moshe Y. Vardi": MAILTO:no@spam.com DESCRIPTION: Search-based techniques in propositional satisfiability (SAT ) solving have been enormously successful\, leading to what is becoming known as the "SAT Revolution". Essentially all s tate-of-the-art SAT solvers are based on the Davis-Putnam-Lo gemann-Loveland (DPLL) technique\, augmented with backjumpin g and conflict learning. Much of current research in this ar ea involves refinements and extensions of the DPLL technique . Yet\, due to the impressive success of DPLL\, little effor t has gone into investigating alternative techniques. This w ork focuses on symbolic techniques for SAT solving\, with th e aim of stimulating a broader research agenda in this area. Refutation proofs can be viewed as a special case of constr aint propagation\, which is a fundamental technique in solvi ng constraint-satisfaction problems. The generalization lift s\, in a uniform way\, the concept of refutation from Boolea n satisfiability problems to general constraint-satisfaction problems. On the one hand\, this enables us to study and ch aracterize basic concepts\, such as refutation width\, using tools from finite-model theory. On the other hand\, this en ables us to introduce new proof systems\, based on represent ation classes\, that have not been considered up to this poi nt. We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations\, and compare their strength to well-known proof systems\, such a s resolution\, the Gaussian calculus\, cutting planes\, and Frege systems of bounded alternation-depth. In particular\, we show that refutations by ODBBs polynomially simulate reso lution and can be exponentially stronger. We then describe a n effort to turn OBDD refutations into OBBD decision procedu res. The idea of this approach\, which we call "symbolic qua ntifier elimination"\, is to view an instance of proposition al satisfiability as an existentially quantified proposition al formula. Satisfiability solving then amounts to quantifie r elimination; once all quantifiers have been eliminated we are left with either 1 or 0. Our goal here is to study the e ffectiveness of symbolic quantifier elimination as an approa ch to satisfiability solving. To that end\, we conduct a dir ect comparison with the DPLL-based ZChaff\, as well as evalu ate a variety of optimization techniques for the symbolic ap proach. In comparing the symbolic approach to ZChaff\, we ev aluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas\, the symboli c approach is superior for other classes of formulas. Finall y\, we turn our attention to Quantified Boolean Formulas (QB F) solving. Much recent work has gone into adapting techniqu es that were originally developed for SAT solving to QBF sol ving. In particular\, QBF solvers are often based on SAT sol vers. Most competitive QBF solvers are search-based. Here we describe an alternative approach to QBF solving\, based on symbolic quantifier elimination. We extend some symbolic app roaches for SAT solving to symbolic QBF solving\, using vari ous decision-diagram formalisms such as OBDDs and ZDDs. In b oth approaches\, QBF formulas are solved by eliminating all their quantifiers. Our first solver\, QMRES\, maintains a se t of clauses represented by a ZDD and eliminates quantifiers via multi-resolution. Our second solver\, QBDD\, maintains a set of OBDDs\, and eliminate quantifiers by applying them to the underlying OBDDs. We compare our symbolic solvers to several competitive search-based solvers. We show that QBDD is not competitive\, but QMRESS compares favorably with sear ch-based solvers on various benchmarks consisting of non-ran dom formulas. DTSTART;TZID=Europe/Paris:20101103T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201011031 100 UID:LSVsemLSV.201011031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: On probabilistic regular graphs STATUS:CONFIRMED ATTENDEE;CN="Christophe Morvan": MAILTO:no@spam.com DESCRIPTION: Regular graphs (generated by deterministic graph grammars) f orm a simple and natural generalisation of pushdown automata . In this talk we use such graphs to define infinite state M arkov chains. We establish some model checking results for a probabilistic temporal logic (pCTL). These results were alr eady known for probabilistic pushdown automata\, but we advo cate that regular graphs enable a simpler exposition. This i s joint work with Nathalie Bertrand (INRIA Rennes). DTSTART;TZID=Europe/Paris:20101116T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201011161 100 UID:LSVsemLSV.201011161100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Parameterized Verification of Ad Hoc Networks STATUS:CONFIRMED ATTENDEE;CN="Arnaud Sangnier": MAILTO:no@spam.com DESCRIPTION: We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adja cent nodes represent single-hop neighbors. Processes are fin ite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-h op neighbors. For this model we consider verification proble ms that can be expressed as reachability of configurations w ith one node (resp. all nodes) in a certain state from an in itial configuration with an arbitrary number of nodes and un known topology. We are interested in decision problems that are parametric on the size and on the shape of the communica tion topology of the initial configurations. We draw a compl ete picture of the decidability boundaries of these problems according to different assumptions on the mobility of the n odes in the networks and on the form of the communication gr aphs. This a joint work with Giorgio Delzanno (University of Genova) and Gianluigi Zavattaro (University of Bologna). DTSTART;TZID=Europe/Paris:20101019T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201010191 100 UID:LSVsemLSV.201010191100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: OPA -- reconquering the web STATUS:CONFIRMED ATTENDEE;CN="David Rajchenbach-Teller": MAILTO:no@spam.com DESCRIPTION: For many\, the Web is Wikipedia\, Google Maps and hundreds o f other rich applications\, both powerful and usable from an ywhere. For others\, it is a security nightmare\, full of ho les\, both low-level and high-level\, exploited or waiting t o be exploited. And for developers\, it is a heap of dozens of distinct technologies\, often approximative\, incompatibl e\, which need to be configured individually\, connected man ually\, often blindly and without clear semantics. In such c onditions\, nothing can be checked or verified. In this talk \, we present OPA\, a new approach for web programming\, bas ed on semantics and type systems. OPA is a programming langu age\, grounded in lambda-calculus and pi-calculus\, designed for the web\, for databases\, for concurrency and for distr ibution. One unique language for the whole application\, wit h formal semantics\, simple primitives\, a clear syntax\, an d safety and security guarantees. Oh\, and a few proofs in C oq. DTSTART;TZID=Europe/Paris:20100914T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201009141 100 UID:LSVsemLSV.201009141100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Composable symbolic security definitions STATUS:CONFIRMED ATTENDEE;CN="Dominique Unruh": MAILTO:no@spam.com DESCRIPTION: The definition of Universal Composability (UC; Canetti\, FOC S 2001) is a cryptographic security definition that is both simple and gives very strong security guarantees. In particu lar\, it ensures that the composition of secure protocols st ays secure. The idea of UC is not\, however\, restricted to the cryptographic (computational) setting; instead\, one can see it as a refinement relation on protocols and programs t hat preserves security and is composable. We show how UC can be applied in a symbolic security setting. We also show a n ew design technique (virtual primitives). This design techni que allows to circumvent\, in a symbolic UC setting\, variou s impossibility results that apply in the cryptographic sett ing. DTSTART;TZID=Europe/Paris:20100629T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006291 100 UID:LSVsemLSV.201006291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: The Tree-Width of the Auxiliary Storage STATUS:CONFIRMED ATTENDEE;CN="Gennaro Parlato": MAILTO:no@spam.com DESCRIPTION: The talk is about a generalization of various results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks\, queues) that have recently been proved. Our genera lization relies on reducing emptiness of these automata to f inite-state *graph automata* (without storage) defined on mo nadic second-order (MSO) definable graphs of bounded tree-wi dth\, where the graph structure encodes the mechanism provid ed by the auxiliary storage. Our results outline a uniform m echanism to derive emptiness algorithms for automata\, expla ining and simplifying several existing results\, as well as proving new decidability theorems. DTSTART;TZID=Europe/Paris:20100601T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006011 100 UID:LSVsemLSV.201006011100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Constrained Environment Assumptions for Multi-Threaded Progr ams STATUS:CONFIRMED ATTENDEE;CN="Andrey Rybalchenko": MAILTO:no@spam.com DESCRIPTION: Automated verification of multi-threaded programs requires e xplicit identification of the interplay between interacting threads\, so-called environment assumptions\, to enable scal able reasoning. Once identified\, these assumptions can be u sed for reasoning with one program thread at a time\, which is possible by using the respective environment assumption t o model the interleaving with other threads. Finding adequat e assumptions that are sufficiently precise to yield conclus ive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major challenge. In this talk I will present a constraint-based t echnique for the inference of such assumptions. Our techniqu e automatically steers towards an optimal precision/efficien cy trade-off between the extremes of efficient\, but incompl ete thread-modular reasoning and complete\, but prohibitivel y expensive consideration of all interleavings. For this tas k\, we pinpoint a declarative formulation of modular verific ation that allows one to express requisite environment assum ptions using constraints and admits algorithmic solutions ba sed on abstract fixpoint checking. I will describe an applic ation of our environment assumption inference for the verifi cation of reachability and termination properties of multi-t hreaded programs. Joint work with Ashutosh Gupta and Corneli u Popeea DTSTART;TZID=Europe/Paris:20100330T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201003301 100 UID:LSVsemLSV.201003301100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: What's in a Name? Evaluating (and Possibly Improving) the Se curity and Usability of Personal Knowledge Questions STATUS:CONFIRMED ATTENDEE;CN="Mike Just": MAILTO:no@spam.com DESCRIPTION: Authentication systems that rely upon personal knowledge que stions (such as "What is your mother's maiden name?") are wi dely used but have\, until recently\, received little attent ion from the academic community. In this talk\, I will prese nt several methods and results regarding the security and us ability of these authentication questions. Evaluating securi ty has\, on one hand\, involved adapting techniques from gue ssing theory and applying them to real-world statistical dis tributions for typical answer categories such as the names o f people\, pets and places. It can also involve staging expe riments where friends or family members are encouraged to gu ess answers. Experiments can also be used to evaluate the us ability (e.g.\, memorability) of challenge questions and the ir answers. And while the results of existing personal knowl edge question systems have been mostly negative\, some possi ble improvements might be gained through increased interacti on with the user\, for example\, to shape the answer distrib ution and lower the prevalence of common answers\, or to int roduce more tolerant authentication so as to reduce the reli ance on perfect response accuracy. DTSTART;TZID=Europe/Paris:20100608T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006081 100 UID:LSVsemLSV.201006081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Programmes de branchement pour l'évaluation d'arbres STATUS:CONFIRMED ATTENDEE;CN="Pierre McKenzie": MAILTO:no@spam.com DESCRIPTION: Après un retour sur le "pebbling"\, sur le modèle du progr amme de branchement et sur sa relation avec la machine de Tu ring\, je présenterai des bornes inférieures sur la taille de programmes de branchement résolvant le problème de l' valuation d'un arbre (je préciserai ce problème\, qui rap pelle la façon dont un "treillis automaton" effectue son ca lcul). Travaux effectués avec Mark Braverman\, Steve Cook\, Rahul Santhanam et Dustin Wehr\, présentés à MFCS 2009 e t FSTTCS 2009. DTSTART;TZID=Europe/Paris:20100427T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201004271 100 UID:LSVsemLSV.201004271100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: On Weak Modal Compatibility and Refinement of Modal I/O Tran sition Systems STATUS:CONFIRMED ATTENDEE;CN="Rolf Hennicker": MAILTO:no@spam.com DESCRIPTION: Modal I/O automata (MIOs) by Larsen et al. provide a flexibl e framework for the specification and implementation of inte racting systems. They distinguish between "may" transitions and "must" transitions\, where the former can be disregarded and the latter must be respected by any correct refinement. Building on the theory of MIOs we introduce a new compatibi lity notion\, called weak modal compatibility\, for interact ing components. As an important property of behavioural inte rface theories we prove that weak modal compatibility is pre served under weak modal refinement. Then we extend the notio n of weak modal compatibility to loosely coupled systems whi ch interact via buffered FIFO channels. We show that also in this case weak compatibility is preserved by weak modal ref inement and that\, moreover\, local refinements compose to g lobal refinements. Finally\, we describe the MIO Workbench\, an Eclipse-based editor and verification tool for modal I/O automata. DTSTART;TZID=Europe/Paris:20100511T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201005111 100 UID:LSVsemLSV.201005111100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: On cycles and separability of persistent Petri nets STATUS:CONFIRMED ATTENDEE;CN="Philippe Darondeau": MAILTO:no@spam.com DESCRIPTION: We show that PBRP nets (plain\, bounded\, reversible and per sistent Petri nets) have bases of cycles made of transition disjoint cycles. We show that PBRP nets are strongly separab le\, meaning that a PBRP net whose initial marking is of the form k.M may be simulated by k replicas of this net\, each with initial marking M. We show that if a net with initial m arking k.M is PBRP then the similar net with initial marking (k-1).M is also PBRP. (joint work with Eike Best) DTSTART;TZID=Europe/Paris:20100525T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201005251 100 UID:LSVsemLSV.201005251100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: From Counter Abstraction to Thread-State Cutoffs: New Techni ques for Multi-Threaded Program Verification STATUS:CONFIRMED ATTENDEE;CN="Thomas Wahl": MAILTO:no@spam.com DESCRIPTION: The formal analysis of multi-threaded programs is among the grand challenges of software verification research. In this talk\, I describe our recent and ongoing work on analyzing p arameterized finite-state programs\, such as non-recursive m ulti-threaded Boolean programs\, a principal ingredient in p redicate abstraction. I begin with a scalable method for ana lyzing the reachability of program locations in programs exe cuted by a bounded number of threads. This method\, being ba sed on counter abstraction\, extends in principle to unbound ed thread counts\, but suffers in practice from the high com plexity of coverability and reachability analyses for certai n types of counter machines. A different approach to program location reachability rests on the assumption that in pract ical parametric program settings\, a small "cutoff" number o f threads suffice to generate all reachable program location s. While this assumption is widely considered to be safe\, i ts practical usefulness hinges on how accurately we are able to estimate the cutoff of a given program. I present a new method that analyses the reachable state space of a replicat ed finite-state program for increasing thread counts\, until a condition emerges that allows us to conclude that the cut off thread count has been reached. Completeness of this meth od is achieved by resorting to traditional coverability anal yses in corner cases. The result is a precise and efficient program location reachability method for replicated finite-s tate programs run by arbitrarily many threads. DTSTART;TZID=Europe/Paris:20100420T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201004201 100 UID:LSVsemLSV.201004201100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: (Un)decidability in Petri nets with name creation and replic ation STATUS:CONFIRMED ATTENDEE;CN="Fernando Rosa Velardo": MAILTO:no@spam.com DESCRIPTION: The study of the expressive power of computation models in between Petri nets and Turing machines\, and in particular o f the class of Well Structured Transition Systems\, is a cha llenging research problem. In this talk I will present two o rthogonal extensions of Petri nets\, with the capability of creating and managing pure names\, and with a replication pr imitive\, getting ν-Petri nets and g-RN systems\, respectiv ely. First\, I will show how these two extensions are strong ly equivalent\, but only when a garbage collection mechanism is added for idle threads. However\, when both extensions a re considered simultaneously\, we obtain a Turing complete m odel\, that we call ν-RN systems. Then I will survey the kn own expressivity results for ν-Petri nets (and therefore\, for g-RN systems). In particular\, coverability\, boundednes s and termination are decidable\, while reachability and pla ce-boundedness are undecidable\, so that ν-Petri nets are s trictly in between Petri nets and Turing machines. Then I wi ll show how can we restrict ν-Petri nets (and\, therefore\, g-RN systems) and ν-RN systems in order to keep decidabili ty of reachability and coverability\, respectively. In parti cular\, if we forbid synchronizations between the different components in a g-RN system\, then reachability is still dec idable. Analogously\, if we forbid name communication betwee n the different components in a ν-RN system\, or restrict c ommunication to happen only for a given finite set of names\ , we obtain decidability of coverability. Finally\, I will c omment on some ongoing work. This is joint work with David d e Frutos-Escrig. http://kimba.mat.ucm.es/~frosa/publicacione s#fi08 DTSTART;TZID=Europe/Paris:20100209T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002091 100 UID:LSVsemLSV.201002091100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Electing a University President using Open-Audit Voting STATUS:CONFIRMED ATTENDEE;CN="Olivier Pereira": MAILTO:no@spam.com DESCRIPTION: In March 2009\, the Université catholique de Louvain electe d its President using a custom deployment of the Helios web- based open-audit voting system. Out of 25\,000 potential vot ers\, 5000 registered\, and almost 4000 voted in each round of the election. The precision of the voting system turned o ut to be crucial: in the first round\, the leader came short of winning the election by only 2 votes. We will describe t he Helios-based voting system used in this election\, the sp ecifics of the UCL deployment\, and the lessons learned in t his deployment. We note at least one interesting conclusion: while it is often assumed that open-audit voting will lead to more complaints and potentially a denial-of-service attac k on the auditing process\, we found that\, instead\, compla ints are likely to be more easily handled in open-audit elec tions because evidence and counter-evidence can be presented . This is joint work with Ben Adida and Olivier de Marneffe. DTSTART;TZID=Europe/Paris:20100309T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201003091 100 UID:LSVsemLSV.201003091100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Modular Verification of Security Protocol Code by Typing STATUS:CONFIRMED ATTENDEE;CN="Karthik Bhargavan": MAILTO:no@spam.com DESCRIPTION: TBA DTSTART;TZID=Europe/Paris:20100126T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201001261 100 UID:LSVsemLSV.201001261100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Machines Reasoning about Machines STATUS:CONFIRMED ATTENDEE;CN="J Strother Moore": MAILTO:no@spam.com DESCRIPTION: Computer hardware and software can be modeled precisely in m athematical logic. If expressed appropriately\, these models can be executable. An appropriate logic is an axiomatically formalized functional programming language. This allows mod els to be used as simulation engines or rapid prototypes. Bu t because they are formal they can be manipulated by symboli c means: theorems can be proved about them\, directly\, with mechanical theorem provers. But how practical is this visio n of machines reasoning about machines? In this highly perso nal talk\, I will describe the 40 year history of the Boyer- Moore Project and discuss progress toward making formal veri fication practical. Among other examples I will describe imp ortant theorems about commercial microprocessor designs\, in cluding parts of processors by AMD\, Motorola\, IBM\, Rockwe ll-Collins and others. Some of these microprocessor models e xecute at 90% the speed of C models and have had important f unctional properties verified. In addition\, I will describe a model of the Java Virtual Machine\, including class loadi ng and bytecode verification and the proofs of theorems abou t JVM methods. Biography J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the Unive rsity of Texas at Austin. He is the author of many books and papers on automated theorem proving and mechanical verifica tion of computing systems. Along with Boyer he is a co-autho r of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co -author of the ACL2 theorem prover. Moore got his SB from MI T in 1970 and his PhD from the University of Edinburgh in 19 73. Moore was a founder of Computational Logic\, Inc.\, and served as its chief scientist for ten years. He served as ch air of the UT Austin CS department for eight years. He and B ob Boyer were awarded the McCarthy Prize in 1983 and the Cur rent Prize in Automatic Theorem Proving by the American Math ematical Society in 1991. In 1999\, they were awarded the He rbrand Award for their work in automatic theorem proving. Bo yer\, Moore\, and Kaufmann were awarded the 2005 ACM Softwar e Systems Award for the Boyer-Moore theorem prover. Moore is a Fellow of both the American Association for Artificial In telligence and the ACM and is a member of the National Acade my of Engineering. DTSTART;TZID=Europe/Paris:20101026T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201010261 100 UID:LSVsemLSV.201010261100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Vérification des propriétés logiques avec des étiquettes STATUS:CONFIRMED ATTENDEE;CN="Mamadou Kanté": MAILTO:no@spam.com DESCRIPTION: Un système d'étiquetage pour une propriété P dans une st ructure consiste à assigner à chaque élément du domaine une étiquette\, aussi petite que possible\, de telle sorte que l'on puisse vérifier la propriété en ne regardant que les étiquettes. Les systèmes d'étiquetage peuvent être vus comme un pré-traitement en vu de faire du model checkin g. En model-checking les objets manipulés sont le plus souv ent statiques. Lorsque la structure est modifiée dans le te mps\, on refait tous les calculs. Nous nous intéressons aux structures qui peuvent perdre des sommets/relations. Nous v oulons pouvoir répondre\, de manière rapide à n'importe q uel moment\, si le graphe résultant après suppression de s ommets/arêtes vérifie une propriété P. Notre technique c onsiste à utiliser les systèmes d'étiquetage. Je montrera i comment vérifier des propriétés du premier ordre dans c ertaines classes de graphes en utilisant des étiquettes de taille logarithmique (les étiquettes sont calculées une se ule fois). Un ingrédient principal est le résultat de Gaif man et une décomposition des formules locales de Frick. Ces résultats peuvent être étendus au comptage. DTSTART;TZID=Europe/Paris:20100202T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002021 100 UID:LSVsemLSV.201002021100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Computational Complexity of Constraint Satisfaction Problems STATUS:CONFIRMED ATTENDEE;CN="Manuel Bodirsky": MAILTO:no@spam.com DESCRIPTION: This talk is an introduction to techniques to determine the computational complexity of constraint satisfaction problems . The central concept here is the notion of a *polymorphism* of a set of constraints. Polymorphisms can be used to trans late questions about computational complexity into questions of fundamental importance in universal algebra. I will firs t give an overview over recent breakthrough results on const raint satisfaction over finite domains based on this transla tion. Then I give an introduction on how to generalize those techniques from finite to infinite domain constraint satisf action\, and present applications in temporal reasoning. DTSTART;TZID=Europe/Paris:20100216T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002161 100 UID:LSVsemLSV.201002161100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: The Complexity of Nash Equilibria in Stochastic Games STATUS:CONFIRMED ATTENDEE;CN="Michael Ummels": MAILTO:no@spam.com DESCRIPTION: We analyse the computational complexity of finding Nash equi libria in simple stochastic multiplayer games. We show that restricting the search space to equilibria whose payoffs fal l into a certain interval may lead to undecidability. In par ticular\, we prove that the following problem is undecidable : Given a game G\, does there exist a pure-strategy Nash equ ilibrium of G where player 0 wins with probability 1. Moreov er\, this problem remains undecidable if it is restricted to strategies with (unbounded) finite memory. However\, if mix ed strategies are allowed\, decidability remains an open pro blem. One way to obtain a provably decidable variant of the problem is restricting the strategies to be positional or st ationary. For the complexity of these two problems\, we obta in a common lower bound of NP and upper bounds of NP and PSP ACE respectively. DTSTART;TZID=Europe/Paris:20091208T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912081 100 UID:LSVsemLSV.200912081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Towards provable security against side-channel attacks STATUS:CONFIRMED ATTENDEE;CN="Boris Köpf": MAILTO:no@spam.com DESCRIPTION: Side-channel attacks threaten the security of cryptographic algorithms by exploiting information that is revealed by the physical characteristics of the algorithm's execution\, for example through variations in the running time or power con sumption. In distributed environments such as the Internet\, timing attacks are the most daunting kind of side-channel a ttack: Timing can be measured and exploited remotely\, openi ng the door for a potentially large number of attackers. Unf ortunately\, there have been no countermeasures against timi ng attacks that are practical and provably secure at the sam e time. In this talk\, I present work on novel methods for r easoning about the security of countermeasures against side- channel attacks. The basis for this work is a model that ena bles one to express bounds for the amount of information tha t can be extracted from a system in a side-channel attack. I present algorithms for computing such bounds\, and I report on experimental results where we apply these algorithms to analyze concrete implementations of cryptographic algorithms . One finding is that the state-of-the-art countermeasure ag ainst timing attacks reduces the rate at which an implementa tion leaks information about the key\, but that the entire k ey information is still eventually revealed. Finally\, I pre sent recent work where we propose a novel countermeasure aga inst timing attacks that is provably secure in our model. A case study shows that this countermeasure is also practical in that it leads to implementations with minor performance o verhead. DTSTART;TZID=Europe/Paris:20091215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912151 100 UID:LSVsemLSV.200912151100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Time-Bounded Verification STATUS:CONFIRMED ATTENDEE;CN="Joel Ouaknine": MAILTO:no@spam.com DESCRIPTION: I will discuss some recent results on verification problems for timed automata over time intervals of fixed\, bounded le ngth. DTSTART;TZID=Europe/Paris:20091027T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200910271 100 UID:LSVsemLSV.200910271100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Reachability in Parametric One-Counter Machines STATUS:CONFIRMED ATTENDEE;CN="James Worrell": MAILTO:no@spam.com DESCRIPTION: In this talk we consider one-counter machines in which count er updates can mention integer-valued parameters. Our main r esult is to show NP-completeness of the problem of determini ng whether a given state is reachable from the initial state for some value of the parameters. Membership in NP is shown by reduction to the existential fragment of Presburger arit hmetic with divisibility. DTSTART;TZID=Europe/Paris:20091103T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200911031 100 UID:LSVsemLSV.200911031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Savez-vous compter ? STATUS:CONFIRMED ATTENDEE;CN="Julien Clément": MAILTO:no@spam.com DESCRIPTION: Les réseaux de capteurs mobiles font leur apparition en inf ormatique depuis plusieurs années. Les applications de ces réseaux sont nombreuses: environnementales\, militaires\, conomiques\, écologiques... Certaines caractéristiques de ces réseaux sont nouvelles et posent ainsi un défi pour l es concepteurs d'algorithmes que nous sommes. Le modèle des protocoles de population [AAD+04] a été conçu pour repr senter formellement les réseaux de capteurs constitués d' agents mobiles dont la mémoire est très limitée\, sans au cun contrôle sur leur propre mouvement. Nous étendrons ce modèle en un modèle plus hétérogène dans lequel nous é tudierons deux problèmes particuliers. Dans cet exposé je présenterai en effet mes résultats sur deux types d'algori thmes. Tout d'abord les 'algorithmes de comptage'\, permetta nt de compter le nombre d'agents présents dans le système alors que des fautes peuvent survenir. Puis\, nous étudiero ns un raffinement de ce modèle\, afin de prendre en compte la différence de vitesse entre les agents\, dans lequel nou s présenterons des 'algorithmes de collecte'\, permettant d e rassembler les données mesurées par les différents agen ts du réseau. DTSTART;TZID=Europe/Paris:20091201T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912011 100 UID:LSVsemLSV.200912011100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Finite Representations for Reconfigurable Systems STATUS:CONFIRMED ATTENDEE;CN="Roland Meyer": MAILTO:no@spam.com DESCRIPTION: To bridge the gap to existing automated verification techniq ues\, we present finite representations for reconfigurable s ystems (RS). Despite an unbounded number of components and c onnections\, a large class of RS exhibits only finitely many connection patterns at runtime; a property called structura l stationarity. We propose a translation of structurally sta tionary systems into finite place/transition Petri nets\, wh ich allows us to reuse existing Petri net verification tools for the verification of RS. To judge the expressiveness of the system class\, we prove that structural stationarity is equivalent to boundedness in the novel functions depth and b readth. The breadth of a RS corresponds to the connection de gree of the components\, while the depth measures their inte rdependence. Investigating these larger classes\, we find th at systems of bounded depth are well-structured. Therefore\, properties can be decided on a finite prefix of the computa tion tree. For systems of bounded breadth\, we show Turing c ompleteness. To recover a Petri net translation for systems of bounded depth\, we combine the newly developed structural semantics with classical concurrency semantics. Although th e resulting mixed translation generalises the previous appro aches\, it does not cover the full class of depth bounded sy stems. An undecidability proof for reachability shows that a translation into finite nets does not exist for the full cl ass. DTSTART;TZID=Europe/Paris:20091124T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200911241 100 UID:LSVsemLSV.200911241100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Fragments of first-order logic over infinite words STATUS:CONFIRMED ATTENDEE;CN="Volker Diekert": MAILTO:no@spam.com DESCRIPTION: In my lecture I report about a joint work with Manfred Kufle itner which was presented at STACS 09 in Freiburg. In that w ork we give topological and algebraic characterizations as w ell as language theoretic descriptions of the following subc lasses of first-order logic for omega-languages: Sigma2\, FO 2\, the intersection of FO2 and Sigma2\, and Delta2 (and by duality Pi2 and the intersection of FO2 and Pi2). These desc riptions extend the respective results for finite words. In particular\, we relate the above fragments to language class es of certain (unambiguous) polynomials. The talk is interpl ay of algebraic\, topological\, and language theoretic prope rties. DTSTART;TZID=Europe/Paris:20090929T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200909291 100 UID:LSVsemLSV.200909291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Approximate Verification of Parameterized Systems STATUS:CONFIRMED ATTENDEE;CN="Giorgio Delzanno": MAILTO:no@spam.com DESCRIPTION: In the talk I will present a series of abstractions that can be used to obtain approximated verification algorithms for parameterized systems with global conditions and different t ypes of topology (ordered/unordered arrays\, trees\, graphs) . The verification algorithms perform a symbolic exploration of a possibly infinite-state space and exploit the theory o f well-quasi orderings for ensuring the theoretical terminat ion of the analysis. The presentation is based on joint work with Parosh Abdulla and Ahmed Rezine. DTSTART;TZID=Europe/Paris:20090922T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200909221 100 UID:LSVsemLSV.200909221100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Regular fixed points\, non-deterministic cyclic proofs and f inite automata STATUS:CONFIRMED ATTENDEE;CN="David Baelde": MAILTO:no@spam.com DESCRIPTION: We consider encoding finite automata as least fixed points i n a proof-theoretical framework equipped with a general indu ction scheme\, and study automata inclusion in that setting. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This leads us to g eneralize these observations to regular formulas\, obtaining new insights about inductive theorem proving and cyclic pro ofs in particular. DTSTART;TZID=Europe/Paris:20090715T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200907151 100 UID:LSVsemLSV.200907151100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: XPath: expressive power and static analysis STATUS:CONFIRMED ATTENDEE;CN="Balder ten Cate": MAILTO:no@spam.com DESCRIPTION: XPath is a language for navigating in XML documents. It is p art of the W3C standard XML querying and processing language s XQuery and XSLT. From the perspective of logic\, XPath can be understood as a variant of temporal logics on finite tre es. In this talk\, I will discuss two aspects of XPath 1.0 a nd 2.0 (as well as of some other variants of XPath proposed in the literature): Expressivity and succinctness: Which pat hs through XML documents can be described in XPath\, and how succinctly? One way to answer this is by comparing XPath to more well established and understood languages such as firs t-order logic. Static analysis: What is the complexity of te sting whether two XPath expressions are equivalent (always g ive the same answer)? Can we find a complete set of equivale nce-preserving rewrite rules (i.e.\, so that every two equiv alent expressions can be rewritten to each other using these rules)? Based on joint works with Maarten Marx\, with Carst en Lutz\, and with Luc Segoufin. DTSTART;TZID=Europe/Paris:20090707T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200907071 100 UID:LSVsemLSV.200907071100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Using ProVerif to Analyze Protocols with XOR and Diffie-Hell man Exponentiation STATUS:CONFIRMED ATTENDEE;CN="Ralf Küsters": MAILTO:no@spam.com DESCRIPTION: ProVerif is one of the most successful tools for cryptograph ic protocol analysis. However\, dealing with algebraic prope rties of operators such as the exclusive OR (XOR) and Diffie -Hellman exponentiation has been problematic. In this talk\, I will present an approach which enables ProVerif\, and rel ated tools\, to analyze a large class of protocols that empl oy the XOR operator and Diffie-Hellman exponentiation. The c ore of our approach is to reduce the derivation problem for Horn theories modulo algebraic properties of XOR/Diffie-Hell man exponentiation to a purely syntactical derivation proble m for Horn theories. The latter problem can then be solved b y tools such as ProVerif. Our reduction works for a large cl ass of Horn theories\, allowing to model a wide range of int ruder capabilities and protocols. We implemented our reducti on and\, in combination with ProVerif\, applied it in the au tomatic analysis of several state-of-the-art protocols that use XOR or Diffie-Hellman exponentiation. This talk is based on joint work with Tomasz Truderung\, published at CCS 2008 and CSF 2009. DTSTART;TZID=Europe/Paris:20090629T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200906291 100 UID:LSVsemLSV.200906291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Specifying Interacting Components with Coordinated Concurren t Scenarios STATUS:CONFIRMED ATTENDEE;CN="Madhavan Mukund": MAILTO:no@spam.com DESCRIPTION: We introduce a visual notation for local specification of co ncurrent components based on message sequence charts (MSCs). Each component is a finite-state machine whose actions are MSCs that specify its local view of the overall communicatio n in the system. These local MSCs are composed into coherent global scenarios using a separately specified set of transa ctions. Intuitively\, each MSC represents a phase of interac tion. We introduce a mechanism to overlap phases that allows complex interactions to be specified without obscuring the logical structure of the constituent scenarios. Our notation combines the global view available in models such as high-l evel message sequence charts (HMSCs) with the local\, asynch ronous structure captured by message-passing automata (MPA). In fact\, both HMSCs and MPAs can be captured as special ca ses of our formalism. In this talk we focus on the syntax an d formal semantics of our notation\, with examples that illu strate why this approach is more natural for capturing real- life specifications. We also describe an approach to use aut omated tools to analyze systems specified using our notation . This is joint work with Prakash Chandrasekaran. DTSTART;TZID=Europe/Paris:20090609T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200906091 100 UID:LSVsemLSV.200906091100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Weak Time Petri Nets Strike Back! STATUS:CONFIRMED ATTENDEE;CN="Arnaud Sangnier": MAILTO:no@spam.com DESCRIPTION: We consider the model of Time Petri Nets where time is assoc iated with transitions. Two semantics for time elapsing can be considered: the strong one\, for which all transitions ar e urgent\, and the weak one\, for which time can elapse arbi trarily. It is well known that many verification problems su ch as the marking reachability are undecidable with the stro ng semantics. In this talk\, we focus on Time Petri Nets wit h weak semantics equipped with three different memory polici es for the firing of transitions. We prove that the reachabi lity problem is decidable for the most common memory policy (intermediate) and becomes undecidable otherwise. Moreover\, we study the relative expressiveness of these memory polici es and obtain partial and surprising results. This a joint w ork with Pierre-Alain Reynier (LIF-Université Aix-Marseille ) DTSTART;TZID=Europe/Paris:20090519T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200905191 100 UID:LSVsemLSV.200905191100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: High-Level Programming for E-Cash STATUS:CONFIRMED ATTENDEE;CN="Pedro Adão": MAILTO:no@spam.com DESCRIPTION: E-cash protocols aim at providing robust abstractions for an onymous payment protocols. Properties of interest include\, for instance\, that users can spend coins anonymously\, that users cannot forge coins\, and that a user should not spend the same coin twice without being eventually caught. These protocols involve sophisticated cryptographic constructions such as blind signatures and commitment and proving their co rrectness is a non-trivial task\, hence reasoning about e-ca sh applications becomes an almost impossible task. Relying o n recent work on optimistic value commitment [FGZN08]\, we p ropose a calculus to reason about e-cash applications. Our c alculus has a simple\, symbolic semantics; it can be used fo r programming with e-cash and for reasoning on its propertie s\, while shielding the programmer from its cryptographic im plementation. We consider two variants of the symbolic seman tics. An abstract semantics rules out any double spending (b y design) while a more realistic\, intermediate semantics ac counts for the possibility of double spending\, with reliabl e detection. We first relate these two semantics\, and then relate the intermediate semantics to the computational prope rties of the underlying e-cash protocol. We show that our ca lculus is a sound abstraction of the low-level e-cash protoc ols\, that is\, all low-level behaviours can be mapped to an high-level equivalent trace. DTSTART;TZID=Europe/Paris:20090512T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200905121 100 UID:LSVsemLSV.200905121100@lsv.ens-cachan.fr LOCATION:Salle Condorcet (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT SUMMARY: Automated Computational Verification for Cryptographic Proto col Implementations STATUS:CONFIRMED ATTENDEE;CN="Eugen Zalinescu": MAILTO:no@spam.com DESCRIPTION: We automatically verify implementations of cryptographic pro tocols programmed in ML. We develop a prototype compiler fro m a subset of ML to CryptoVerif\, Blanchet's prover for comp utational cryptography. Thus\, we obtain a first tool chain that yields security guarantees for computational models tig htly related to executable code. We show the soundness of th e underlying translation for authentication and secrecy. To this end\, we equip ML programs with a probabilistic semanti cs\, and relate it to the probabilistic polynomial-time sema ntics of CryptoVerif. We also review experimental (symbolic and computational) results recently obtained for a reference implementation of the TLS protocol. (This is joint work wit h Karthik Bhargavan\, Ricardo Corin\, and Cédric Fournet.) DTSTART;TZID=Europe/Paris:20090428T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904281 100 UID:LSVsemLSV.200904281100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Test à partir de spécifications logiques STATUS:CONFIRMED ATTENDEE;CN="Delphine Longuet": MAILTO:no@spam.com DESCRIPTION: Le test est l'une des méthodes les plus utilisées pour la validation des syst-bèmes informatiques. Lorsque l'implant ation du système -Aà tester n'est pas connue\, les tests sont sélectionnés et construits à partir d'une spécifica tion (formelle) du syst-bème. Il existe principalement deu x approches du test -Aà partir de spécifications formelle s : les spécifications logiques sont utilisées pour tester le comportement fonctionnel des syst-bèmes (les donn-Aé es)\, tandis que les syst-bèmes de transitions sont utilis -Aés pour tester le comportement dynamique et réactifs de s syst-bèmes (actions et communications).-A Une théorie du test à partir de spécifications logiques a été défin ie dans les années 90\, formalisant le cadre de test ainsi que les différentes phases du processus de test. Ces travau x proposent en particulier une méthode de sélection de tes ts appelée dépliage pour des spécifications de forme rest reinte dont les axiomes sont des équations conditionnelles. L'idée de cette méthode est d'utiliser des techniques de preuve afin de guider la sélection de tests. Le but est d'o btenir une couverture pertinente des comportements du syst- bème.-A Je présenterai tout d'abord cette formalisation d u test\, en particulier le probl-bème de l'existence d'un jeu de tests exhaustif\, puis la m-Aéthode de sélection d e tests par dépliage. Je présenterai ensuite deux aspects de mes travaux : - la généralisation de ce cadre de test a ux spécifications du premier ordre\, et en particulier les résultats d'exhaustivité et de complétude de la sélectio n par dépliage étendue à ces spécifications - l'adaptati on de ce cadre\, ainsi que les résultats d'exhaustivité et l'adaptation du dépliage\, à des spécifications modales du premier ordre\, dans le but de proposer une nouvelle appr oche de test pour les syst-bèmes r-Aéactifs. DTSTART;TZID=Europe/Paris:20090427T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904271 100 UID:LSVsemLSV.200904271100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Qualitative Determinacy and Decidability of Stochastic Games with Partial Observation STATUS:CONFIRMED ATTENDEE;CN="Hugo Gimbert": MAILTO:no@spam.com DESCRIPTION: (Joint work with Nathalie Bertrand and Blaise Genest.) We co nsider the standard model of finite two-person zero-sum stoc hastic games with signals. We are interested in the existenc e of almost-surely winning or positively winning strategies\ , under reachability\, safety\, Büchi or co-Büchi winning objectives. We prove two qualitative determinacy results. Fi rst\, in a reachability game either player 1 can achieve alm ost surely the reachability objective\, or player 2 can ensu re almost surely the complimentary safety objective\, or bot h players have positively winning strategies. Second\, in a Büchi game if player 1 cannot achieve almost surely the Bü chi objective\, then player 2 can ensure positively the comp limentary co-Büchi objective. We prove that players only ne ed strategies with finite-memory\, whose sizes range from no memory at all to doubly-exponential size\, with matching lo wer bounds. We provide fix-point algorithms to decide which player has an almost surely winning or positive winning stra tegy and compute the finite memory strategy. Complexity rang es from EXPTIME to 2EXPTIME with matching lower bounds\, and better complexity can be achieved for some special cases wh ere one of the players is better informed than her opponent. DTSTART;TZID=Europe/Paris:20090421T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904211 100 UID:LSVsemLSV.200904211100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Kleene et Kozen en Coq STATUS:CONFIRMED ATTENDEE;CN="Damien Pous": MAILTO:no@spam.com DESCRIPTION: Formaliser des choses dans un assistant de preuve s'av-bèr e souvent-A pénible\, de nombreuses étapes de raisonnemen t devant -bêtre explicit-Aées alors qu'elles sont d'habi tude laissées au relecteur scrupuleux. Ceci est en particul ier vrai lorsque l'on doit travailler sur des relations bina ires (réécriture\, réductions\, équivalences\, etc...)\, tr-bès-A intuitives\, mais pas compl-bètement triviale s.-A Lorsque c'est possible\, une premi-bère astuce consi ste -Aà considérer les relations de fa-bçon alg-Aébri que : en montant le niveau d'abstraction\, on facilite la fo rmalisation de certaines preuves. Une fois ce pas franchi\, on réalise que les relations binaires sont un mod-bèle de s-A alg-bèbres de Kleene\, d-Aécidables par la théorie des automates finis. Nous exposerons un travail en cours\, sur une formalisation Coq des automates - via des matrices\, afin d'obtenir une tactique de décision des alg-bèbres d e-A Kleene\, par réflection. Plus généralement\, nous ex poserons les outils que nous développons pour raisonner sur ce genre de structures algébriques. DTSTART;TZID=Europe/Paris:20090414T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904141 100 UID:LSVsemLSV.200904141100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Logics with Rank Operators STATUS:CONFIRMED ATTENDEE;CN="Anuj Dawar": MAILTO:no@spam.com DESCRIPTION: It is a long-standing open problem in descriptive complexity theory whether there is a logic that expresses exactly the polynomial-time decidable properties of unordered structures . It has been known since the early 90s that fixed-point log ic with counting (FPC) is not sufficient and there have been several proposals for more expressive logics. Taking our in spiration from recent results that show that natural linear- algebraic operations are not definable in FPC\, we propose F PR - an extension of fixed-point logic with an operator for matrix rank. We show that this is strictly more expressive t han FPC and can express the polynomial-time problems that ha ve been shown to be inexpressible in FPC. We also show that FO+R\, the extension of first-order logic with rank operator s is surprisingle expressive. It can express some forms of t ransitive closure and\, on ordered structures\, captures the complexity classes ModpL. In this talk\, I will give the hi story and general background to the question (assuming littl e or no previous knowledge of descriptive complexity and fix ed-point logics) and explain the context of the new results. I will also point to several interesting open problems. (Jo int work with Martin Grohe\, Bjarki Holm and Bastian Laubner ). DTSTART;TZID=Europe/Paris:20090407T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904071 100 UID:LSVsemLSV.200904071100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Games of ordinal Length STATUS:CONFIRMED ATTENDEE;CN="Florian Horn": MAILTO:no@spam.com DESCRIPTION: We present an extension of the classical model of infinite t wo-player games\, allowing plays with arbitrary ordinal leng th. In addition to the usual ''successor transitions''\, our arenas feature ''limit transitions'' which describe what ha ppens after partial plays whose length is a limit ordinal. T he play only stops when it reaches a final state\, which can be winning for either of the players. We describe two solut ions for such games. The first one uses a reduction to infin ite Muller games\, and shows that the problem of the winner is PSPACE-complete. The second one uses a special case of or dinal games with ''priority'' transitions\, where the player s have positional strategies. A LAR-like construction allows us to derive the existence of finite-memory strategies in t he general case. DTSTART;TZID=Europe/Paris:20090406T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904061 100 UID:LSVsemLSV.200904061100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Cryptographic protocols as Building Blocks: From the Man-in- the-Middle attack to Compositional Symbolic Analysis. STATUS:CONFIRMED ATTENDEE;CN="Cas Cremers": MAILTO:no@spam.com DESCRIPTION: Despite using very coarse abstractions\, and making strong a ssumptions on the environment\, the symbolic analysis of cry ptographic protocols has proven very successful. By now\, ma ny dimensions of the symbolic (Dolev-Yao) model have been ex plored to some extent\, including compositionality propertie s of protocols and the relation between symbolic correctness proofs and computational proofs. One might expect that form al approaches are ideally suited for building larger communi cation infrastructures\, because of their high level of abst raction. However\, in practice\, symbolic methods are only u sed for analysis of existing protocols\, whereas protocol co nstruction is performed at the detailed level of cryptograph ic protocols. In this talk we cover some of the requirements for using cryptographic protocols as components in symbolic \, Dolev-Yao like\, analyses. In particular\, we discuss var ious compositionality results\, and their relation to using cryptographic protocols as building blocks. Finally\, we rev isit the cryptographic requirements on real-world protocols and show how they influence the compositionality problem\, a nd conclude with a number of open problems. DTSTART;TZID=Europe/Paris:20090331T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903311 100 UID:LSVsemLSV.200903311100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: What's decidable for Asynchronous Programs? STATUS:CONFIRMED ATTENDEE;CN="Pierre Ganty": MAILTO:no@spam.com DESCRIPTION: An asynchronous or ''event-driven'' program is one that cont ains procedure calls which are not directly executed from th e call site\, but stored and executed later by an external s cheduler. By providing a low-overhead way to manage concurre nt interactions\, asynchronous programs form the core of man y server programs\, embedded systems\, and popular programmi ng styles for the web (Ajax). Unfortunately\, such programs can be hard to write and maintain as sequential control flow needs to be split into several disjoint handlers. They are a challenge for static analysis tools as they are infinite s tate: both the program stack and the number of outstanding a synchronous requests may be unbounded. We show that safety a nd liveness properties can be checked effectively for the cl ass of Boolean asynchronous programs\, thus enabling automat ic static techniques to check for correctness or for errors. DTSTART;TZID=Europe/Paris:20090330T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903301 100 UID:LSVsemLSV.200903301100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: TPTP\, TSTP\, CASC\, etc. - Automated Reasoning in Practice STATUS:CONFIRMED ATTENDEE;CN="Geoff Sutcliffe": MAILTO:no@spam.com DESCRIPTION: This talk gives an overview of the activities and products t hat stem from the Thousands of Problems for Theorem Provers (TPTP) problem library for Automated Theorem Proving (ATP) s ystems. These include the TPTP itself\, the Thousands of Sol utions from Theorem Provers (TSTP) solution library\, the TP TP language\, the CADE ATP System Competition (CASC)\, tools such as my semantic Derivation Verifier (GDV) and the Inter active Derivation Viewer (IDV)\, meta-ATP systems such as th e Smart Selective Competition Parallelism (SSCPA) system and the Semantic Relevance Axiom Selection System (SRASS)\, onl ine access to automated reasoning systems and tools through the SystemOnTPTP web service\, and applications in various d omains. Current work extending the TPTP to higher-order logi c will be introduced. DTSTART;TZID=Europe/Paris:20090317T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903171 100 UID:LSVsemLSV.200903171100@lsv.ens-cachan.fr LOCATION:Salle Renaudeau (Bâtiment Laplace) END:VEVENT BEGIN:VEVENT SUMMARY: On the Reachability Analysis of Acyclic Networks of Pushdown Systems STATUS:CONFIRMED ATTENDEE;CN="Tayssir Touili": MAILTO:no@spam.com DESCRIPTION: We address the reachability problem in acyclic networks of p ushdown systems. We consider communication based either on s hared memory or on message passing through unbounded lossy c hannels. We prove mainly that the reachability problem betwe en recognizable sets of configurations (i.e.\, definable by a finite union of products of finite-state automata) is deci dable for such networks\, and that for lossy channel pushdow n networks\, the channel language is effectively recognizabl e. This fact holds although the set of reachable configurati ons (including stack contents) for a network of depth (at le ast) 2 is not rational in general (i.e.\, not definable by a multi-tape finite automaton). Moreover\, we prove that for a network of depth 1\, the reachability set is rational and effectively constructible (under an additional condition on the topology for lossy channel networks). This is a joint wo rk with Mohamed Faouzi Atig and Ahmed Bouajjani. DTSTART;TZID=Europe/Paris:20090310T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903101 100 UID:LSVsemLSV.200903101100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Context-bounded analysis of multithreaded Java programs STATUS:CONFIRMED ATTENDEE;CN="Stefan Schwoon": MAILTO:no@spam.com DESCRIPTION: The reachability problem is undecidable for programs with bo th recursive procedures and multiple threads with shared mem ory. One approach to resolve this problem is to use context- bounded reachability\, i.e. to consider only those runs in w hich the active thread changes at most k times\, where k is fixed. However\, until recently\, context-bounded reachabili ty has been only a theoretical possibility\, primarily becau se of its prohibitive worst-case runtime. In the talk\, whic h presents joint work with Dejvuth Suwimonteerabuth and Javi er Esparza\, I will talk about an improvement that alleviate s this problem. The approach has been implemented in the too l jMoped. DTSTART;TZID=Europe/Paris:20090304T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903041 100 UID:LSVsemLSV.200903041100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: A weighted mu-calculus on words STATUS:CONFIRMED ATTENDEE;CN="Ingmar Meinecke": MAILTO:no@spam.com DESCRIPTION: We define a weighted mu-calculus on finite and infinite word s. Hereby\, the mu-calculus does not use conjunction and the weights are taken from semirings satisfying certain complet eness and continuity properties. For important semirings lik e distributive complete lattices\, the tropical and the prob abilistic semiring\, we show that the formulas of the conjun ction-free weighted mu-calculus define exactly the class of omega-rational formal power series. DTSTART;TZID=Europe/Paris:20090303T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903031 100 UID:LSVsemLSV.200903031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: On Simulation-Based Probabilistic Model Checking of Mixed-An alog Circuits STATUS:CONFIRMED ATTENDEE;CN="Axel Legay": MAILTO:no@spam.com DESCRIPTION: In this talk\, we consider verifying properties of mixed-sig nal circuits\, i.e.\, circuits for which there is an interac tion between analog (continuous) and digital (discrete) valu es. We use a simulation-based approach that consists of eval uating the property on a representative subset of behaviors\ , generated by simulation\, and answering the question of wh ether the circuit satisfies the property with a probability greater than or equal to some value. We propose a logic adap ted to the specification of properties of mixed-signal circu its\, in the temporal domain as well as in the frequency dom ain. We also demonstrate the applicability of the method on different models of Δ-Σ modulators for which previous form al verification attempts were too conservative and required excessive computation time. With Alexandre Donzé and Edmund Clarke. DTSTART;TZID=Europe/Paris:20090224T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902241 100 UID:LSVsemLSV.200902241100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Verifying Functional Properties of Pointer Programs STATUS:CONFIRMED ATTENDEE;CN="Ewen Maclean": MAILTO:no@spam.com DESCRIPTION: Separation logic has been used successfully to verify safety properties of programs which manipulate the heap. The Small foot family of program analysers are capable of verifying sh ape properties of pointer programs\, for example analysing t he shape of inductive structures on the heap\, such as linke d lists. I discuss an extension to this work which concerns the automatic verification of functional properties of point er programs. I will discuss the challenging parts of such ve rifications which require creative input. The talk will be m otivated by examples and possibly a working demo of some of the early results. DTSTART;TZID=Europe/Paris:20090217T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902171 100 UID:LSVsemLSV.200902171100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Regular graphs: a perfect model for infinite state systems? STATUS:CONFIRMED ATTENDEE;CN="Christophe Morvan": MAILTO:no@spam.com DESCRIPTION: There are dozens of models for infinite state systems. Indee d\, Turing machine\, cellular automata\, pushdown systems\, Petri nets\, or process algebras are only major examples of such systems. Most of these systems do not provide the simpl icity and efficiency of finite state systems. Finite graphs\ , or finite state automata\, are the corner stone of compute r science\, it is still a very active field of research with countless applications. Infinite state systems lack that ki nd of universal and simple framework. Graph grammars were in itially used to produce infinite sets of graphs. But in the early 90's\, Courcelle used deterministic graph grammars to characterise a general class of infinite graphs: regular gra phs. Recently Caucal built up a nice toolbox for studying re gular graphs\, and with Hassen they provided an elegant exte nsion of visibly pushdown automata\, which captures every de terministic context-free language. In this talk we will pres ent a survey on regular graphs\, including a discussion on t he extensions of visibly pushdown automata. We will present\ , as well\, an ongoing work with Nathalie Bertrand aiming at generalising probabilistic pushdown automata to this graph grammar setting. DTSTART;TZID=Europe/Paris:20090210T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902101 100 UID:LSVsemLSV.200902101100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Parameter Synthesis for Probabilistic Timed Reachability STATUS:CONFIRMED ATTENDEE;CN="Joost-Pieter Katoen": MAILTO:no@spam.com DESCRIPTION: In this talk\, we propose a technique to synthesize parametr ic rate values in continuous-time Markov chains that ensure the validity of time-bounded reachability properties. Rate e xpressions over variables indicate the average speed of stat e changes and are expressed using the polynomials over reals . The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity of bounded reachability prope rties. This algorithm is based on discretizing parameter ran ges together with a refinement technique. We will describe t he algorithm\, analyze its time complexity\, and show its ap plicability by deriving parameter constraints for a real-tim e storage system with probabilistic error checking facilitie s. (This is joint work with Tingting Han and Alexandre Merea cre.) DTSTART;TZID=Europe/Paris:20090113T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200901131 100 UID:LSVsemLSV.200901131100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Analyses de propriétés quantitatives de programmes STATUS:CONFIRMED ATTENDEE;CN="Laure Gonnord": MAILTO:no@spam.com DESCRIPTION: Dans cet exposé je présenterai mes travaux doctoraux et po stdoctoraux qui se placent tous les deux dans le contexte d' analyse des propriétés quantitatives de programmes dans le but de faire des logiciels embarqués s-bûrs.-A Dans ma th-bèse\, j'ai -Aétudié l'analyse des relations linéai res\, qui permet de découvrir automatiquement\, en chaque p oint de contrôle d'un programme\, des syst-bèmes de contr aintes lin-Aéaires invariantes sur les variables numériqu es. Les résultats de l'analyse sont utilisables en compilat ion\, en vérification de programmes et en parallélisation. Apr-bès une introduction rapide -Aà cette méthode\, je montrerai plus spécifiquement comment la précision des an alyses peut -bêtre am-Aéliorée grâce à la notion d'ac célération abstraite. Mes travaux postdoctoraux ont étudi é d'autres types d'applications embarquées que sont les ap plications multimédia. Ces applications ne sont plus critiq ues\, mais par contre on désire évaluer et garantir des pr opriétés extra fonctionnelles\, comme la qualité de servi ce. En effet\, la resource allouée à un composant logiciel peut évoluer\, et on aimerait garantir une certaine fluidi té de l'application. Je présenterai mes travaux de formali sation des contraintes de ressources au sein d'une architect ure logicielle à composants\, Qinna\, ainsi que les mécani smes de maintenance de ces contraintes. DTSTART;TZID=Europe/Paris:20090106T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200901061 100 UID:LSVsemLSV.200901061100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: The State of Inductive Theorem Proving for Software Verifica tion STATUS:CONFIRMED ATTENDEE;CN="Lucas Dixon": MAILTO:no@spam.com DESCRIPTION: Functional correctness for non-trivial properties of softwar e requires inductive proof. Sadly this is an undecidable pro blem which typically requires frustrating amounts of user gu idance. Fortunately\, this makes it a fascinating topic for research; indeed\, a significant strand of research consider s heuristic approaches to inductive theorem proving\, driven by syntactic observations. Recently\, a type-theory based f orm of synthesis\, combined with an upside-down twist on rew riting\, has led to some exciting results. In this talk I wi ll outline the state the field\, give my view of the key int uitions for the emerging proof strategies\, and highlight th e exciting challenges currently being considered. DTSTART;TZID=Europe/Paris:20081216T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812161 100 UID:LSVsemLSV.200812161100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Quantitative Languages: Decision Problems\, Expressive Power \, and Closure Properties STATUS:CONFIRMED ATTENDEE;CN="Laurent Doyen": MAILTO:no@spam.com DESCRIPTION: Quantitative generalizations of classical languages\, which assign to each word a real number instead of a boolean value \, have applications in modeling resource-constrained comput ation. We use weighted automata (finite automata with transi tion weights) to define several natural classes of quantitat ive languages over finite and infinite words; in particular\ , the real value of an infinite run is computed as the maxim um\, limsup\, liminf\, limit average\, or discounted sum of the transition weights. We define the classical decision pro blems of automata theory (emptiness\, universality\, languag e inclusion\, and language equivalence) in the quantitative setting and study their computational complexity. As the dec idability of language inclusion remains open for some classe s of weighted automata\, we introduce a notion of quantitati ve simulation that is decidable and implies language inclusi on. We also give a complete characterization of the expressi ve power of the various classes of weighted automata. In par ticular\, we show that most classes of weighted automata can not be determinized. Finally\, for quantitative languages L\ , L'\, we study the operations max(L\,L')\, min(L\,L')\, and 1-L as natural generalizations of the boolean operations; w e also consider the sum L + L'. We establish the closure pro perties of all classes of quantitative languages with respec t to these four operations. This talk is based on joint work with Krishnendu Chatterjee and Tom Henzinger. DTSTART;TZID=Europe/Paris:20081215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812151 100 UID:LSVsemLSV.200812151100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: An Easy Algorithm For The General Vector Addition System Rea chability Problem STATUS:CONFIRMED ATTENDEE;CN="Jérôme Leroux": MAILTO:no@spam.com DESCRIPTION: The reachability problem for Vector Addition Systems (VAS) or equivalently for Petri Nets is a central problem of net t heory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sac erdote-Tenney (KLMST) decomposition. This decomposition is d ifficult and it just has a non-primitive recursive upper-bou nd complexity. In this paper\, we prove that if a final conf iguration is not reachable from an initial one\, there exist s a pair of Presburger formulas denoting an inductive separa tor proving this property. Since we can decide with any deci sion procedure for the Presburger arithmetic if pairs of Pre sburger formulas denote inductive separators\, we deduce tha t there exist checkable certificates of non-reachability. In particular\, there exists an easy algorithm for deciding th e general VAS reachability problem based on two semi-algorit hms. A first one that tries to prove the reachability by fai rly enumerating finite sequence of actions and a second one that tries to prove the non-reachability by fairly enumerati ng pairs of Presburger formulas. Even if the KLMST decomposi tion is used for proving the termination\, this algorithm is the very first one that can be implemented without using it . DTSTART;TZID=Europe/Paris:20081209T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812091 100 UID:LSVsemLSV.200812091100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: XML Reasoning: From Theory to Practice STATUS:CONFIRMED ATTENDEE;CN="Pierre Genevès": MAILTO:no@spam.com DESCRIPTION: In the research for XML static type systems\, one challenge is to deal with XPath powerful navigational features. I wil l present a fixpoint modal logic designed for reasoning on f inite trees\, along with a satisfiability-testing algorithm that performs well in practice. The fully implemented system allows to effectively solve a whole class of problems invol ving XPath queries\, regular tree types and any boolean comb ination of them (like query containment\, and query satisfia bility in the presence of schemas). DTSTART;TZID=Europe/Paris:20081125T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811251 100 UID:LSVsemLSV.200811251100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: From Philosophical to Industrial Logics STATUS:CONFIRMED ATTENDEE;CN="Moshe Vardi": MAILTO:no@spam.com DESCRIPTION: One of the surprising developments in the area of program v erification is how several ideas introduced by logicians in the first part of the 20th century ended up yielding at the start of the 21st century industry-standard property-specifi cation languages called PSL and SVA. This development was en abled by the equally unlikely transformation of the mathemat ical machinery of automata on infinite words\, introduced in the early 1960s for second-order arithmetics\, into effecti ve algorithms for industrial model-checking tools. This talk attempts to trace the tangled threads of this development. DTSTART;TZID=Europe/Paris:20081106T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811061 100 UID:LSVsemLSV.200811061100@lsv.ens-cachan.fr LOCATION:Amphithéâtre Marie Curie (bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT SUMMARY: Questions de théorie des jeux et de convexité abstraite en analyse statique de programme STATUS:CONFIRMED ATTENDEE;CN="Stéphane Gaubert": MAILTO:no@spam.com DESCRIPTION: Le but de cet exposé est de donner quelques exemples d'appl ication de techniques d'optimisation et de théorie des jeux en analyse statique de programme par interprétation abstra ite. On présentera tout d'abord une correspondance entre le s problèmes de point fixe rencontrés en interprétation ab straite et ceux que l'on rencontre en théorie des jeux à s omme nulle. Cette correspondance permet d'adapter des algori thmes inspirés de la théorie des jeux ou du contrôle tels que l'itération sur les politiques\, mais le caractère "e xpansif" des opérateurs de point fixe\, qui se traduit par la présence d'un taux d'actualisation négatif\, pose des d ifficultés algorithmiques inédites. On discutera notamment le problème du calcul du point fixe minimal (ou de la vér ification de la minimalité d'un point fixe) à l'aide de te chniques de théorie de Perron-Frobenius non-linéaire. On m ontrera ensuite comment des idées empruntées à l'analyse convexe abstraite permettent de définir des classes de doma ines généralisant le domaine des "templates" introduit par Manna et ses collaborateurs. On traitera spécialement du d omaine des polyèdres max-plus ou tropicaux. Ces résultats sont issus de travaux en collaboration avec A. Adje (LIX/MeA SI)\, X. Allamigeon (EADS)\, E. Goubault et S. Putot (CEA/Me ASI). DTSTART;TZID=Europe/Paris:20081104T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811041 100 UID:LSVsemLSV.200811041100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Tree Pattern Rewriting Systems STATUS:CONFIRMED ATTENDEE;CN="Olivier Serre": MAILTO:no@spam.com DESCRIPTION: Classical verification often uses abstraction when dealing w ith data. On the other hand\, dynamic XML-based applications have become pervasive\, for instance with the ever growing importance of web services. We define here Tree Pattern Rewr iting Systems (TPRS) as an abstract model of dynamic XML-bas ed documents. TPRS systems generate infinite transition syst ems\, where states are unranked and unordered trees (hence p ossibly modeling XML documents). The guarded transition rule s are described by means of tree patterns. Our main result i s that given a TPRS system (T\,R)\, a tree pattern P and som e integer k such that any reachable document from T has dept h at most k\, it is decidable (albeit of non elementary comp lexity) whether some tree satisfying P is reachable from T. This is joint work with B. Genest\, A. Muscholl\, and M. Zei toun. DTSTART;TZID=Europe/Paris:20081028T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200810281 100 UID:LSVsemLSV.200810281100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Génération Automatique d'Approximations Régulières STATUS:CONFIRMED ATTENDEE;CN="Pierre-Cyrille Héam": MAILTO:no@spam.com DESCRIPTION: Etant donnés deux langages réguliers d'arbres I et B\, et un système de réécriture R\, on ne peut pas décider si R*(I) et B ont une intersection vide\, m-bême pour des sys t-Aèmes de réécritures simples. Une approche pour résou dre ce problème consiste alors à utiliser des approximatio ns de R*(I). Nous montrerons dans cet exposé comment une te chnique manuelle d'approximations introduite par Th. Genet e n 98 peut -bêtre automatis-Aée\, notamment pour la véri fication de protocoles cryptographiques. DTSTART;TZID=Europe/Paris:20081014T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200810141 100 UID:LSVsemLSV.200810141100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Diagnostic et Test en ordres partiels STATUS:CONFIRMED ATTENDEE;CN="Stefan Haar": MAILTO:no@spam.com DESCRIPTION: The talk takes a stand to advocate the use of partial order unfolding semantics for the analysis of large networked sys tems\, exemplified by fault diagnosis in telecommunication n etworks. The methodology of asynchronous diagnosis is presen ted\, followed by a discussion of fun but challenging proble ms connected to diagnosis\, in particular distribution of un folding. In a different domain\, the talk will present recen t and ongoing work on testing of input/output automata over partially ordered I/O streams. DTSTART;TZID=Europe/Paris:20080930T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809301 100 UID:LSVsemLSV.200809301100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Génération d'une suite de tests de grammaticalité STATUS:CONFIRMED ATTENDEE;CN="Sylvain Schmitz": MAILTO:no@spam.com DESCRIPTION: L'exposé s'intéresse à des techniques de fouille d'erreu rs dans une grammaire du fran-bçais d-Aéveloppée au LOR IA. Cette grammaire\, de taille importante\, utilisée à la fois pour l'analyse syntaxique et la génération de texte\ , souffre de problèmes de sur-génération : elle décrit d es phrases incorrectes. Pour un ensemble de phrases de test\ , la fouille d'erreurs cherche alors à identifier les cause s les plus probables de sur-génération pour assister le li nguiste dans son travail de correction. Je présenterai en d étail une méthode de génération de telles phrases qui vi se à explorer les coins et recoins de la grammaire et les i nteractions inattendues qu'elle permet. DTSTART;TZID=Europe/Paris:20080923T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809231 100 UID:LSVsemLSV.200809231100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Programming in Malbolge STATUS:CONFIRMED ATTENDEE;CN="Masahiko Sakai": MAILTO:no@spam.com DESCRIPTION: Malbolge is known as one of the most esoteric programming l anguages\, in which programming is very difficult. The diffi culty comes from (a) its restrictive instructions\, (b) inst ruction-replacement after execution and (c) restriction for loadable data. In this talk\, we solve these problems and sh ows that general loop-programming is possible in this langua ge. DTSTART;TZID=Europe/Paris:20080916T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809161 100 UID:LSVsemLSV.200809161100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Regular Model Checking using nondeterministic tree automata STATUS:CONFIRMED ATTENDEE;CN="Tomas Vojnar": MAILTO:no@spam.com DESCRIPTION: Abstract regular tree model checking (ARTMC) is a generic t echnique for automated formal verification of various kinds of infinite-state and parameterised systems\, including\, e. g.\, parameterised protocols or programs manipulating dynami c\, pointer-linked data structures. ARTMC is based on repres enting infinite sets of configurations of the examined syste ms by finite tree automata whose efficient manipulation is t hus crucial for an overall efficiency of ARTMC. It turns out that a significant bottleneck in dealing with finite tree a utomata is the need to determinise them when checking inclus ion or within the classical automata minimisation procedure. In the talk\, we will present several recent works whose ai m is to eliminate the need to determinise the automata being handled in ARTMC. In particular\, we will present methods f or an antichain-based inclusion checking on nondeterministic tree automata and efficient methods for reducing the size o f such automata based on various types of upward\, downward\ , and composed (bi)simulations. According to our experimenta l results\, these techniques really very significantly impro ve the performance of ARTMC. The talk is based on joint work with Ahmed Bouajjani and Tayssir Touili from LIAFA\, Peter Habermehl from LSV\, Parosh Aziz Abdulla and Lisa Kaati from Uppsala\, and Lukas Holik from FIT BUT. DTSTART;TZID=Europe/Paris:20080708T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200807081 100 UID:LSVsemLSV.200807081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Tableau-based decision procedure for the logic of strategic ability in multi-agent systems ATL STATUS:CONFIRMED ATTENDEE;CN="Valentin Goranko": MAILTO:no@spam.com DESCRIPTION: The Alternating-time Temporal Logic (ATL)\, introduced by A lur\, Henzinger\, and Kupferman\, is a logic for reasoning a bout strategic abilities of agents and coalitions in multi-a gent systems\, in which one can express statements\, such as : "The agent (or\, coalition of agents) A has a strategy suc h that\, if A follows that strategy then\, no matter what ot her agents do\, the objective $\phi$ will be achieved"\, the re the objective is itself a formula of ATL prefixed by a te mporal operator such as `nexttime'\, `until'\, or `always in the future'. Testing satisfiability in ATL has been proved decidable (ExpTime complete)\, by using alternating tree aut omata and by small model property\, but both methods have so me practical deficiencies and are not suitable for manual ap plication. In this talk I will give a concise introduction t o ATL and then will present a recently developed decision pr ocedure for testing satisfiability in ATL based on sound\, c omplete\, and terminating incremental tableaux. This decisio n procedure runs in the theoretically prescribed time comple xity\, i.e.\, ExpTime\, but in most practical cases is much more efficient\, and is suitable for both manual and compute rized application. (Joint work with Dmitry Shkatov\, Univ. o f the Witwatersrand) DTSTART;TZID=Europe/Paris:20080701T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200807011 100 UID:LSVsemLSV.200807011100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Star-height of tree languages STATUS:CONFIRMED ATTENDEE;CN="Christof Löding": MAILTO:no@spam.com DESCRIPTION: The star-height problem for regular word languages is to de termine for a given regular language the minimal number of n estings of Kleene-stars required in a regular expression def ining the given language. We consider the corresponding prob lem for regular tree languages and show that this problem is decidable. We do this by adapting a proof method that was u sed by Daniel Kirsten to the setting of trees. DTSTART;TZID=Europe/Paris:20080617T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200806171 100 UID:LSVsemLSV.200806171100@lsv.ens-cachan.fr LOCATION:Amphi 109N (Bât. Léonard de Vinci) END:VEVENT BEGIN:VEVENT SUMMARY: Precise Fixpoint-Based Analysis of Programs with Thread-Crea tion and Procedures STATUS:CONFIRMED ATTENDEE;CN="Markus Müller-Olm": MAILTO:no@spam.com DESCRIPTION: Most papers on precise analysis of parallel programs descri be process creation by parbegin/parend blocks or their inter procedural counterpart\, parallel procedure calls. In these models\, the creator of processes running in parallel must w ait until all the created processes have terminated before i t can resume its execution. However\, in presence of procedu res or methods\, this does not allow one to model thread cre ation primitives as the found in languages like Java adequat ely. In this talk I am going to present recent work on fixpo int-based analysis of programs with thread creation and (rec ursive) procedures. Our algorithm solves gen/kill-problems p recisely up to abstraction of synchronization common in this line of research; it can handle forward as well as backward problems. Our results complement earlier work on automata-b ased analysis of similar program models. The resulting algor ithm\, however\, computes global information faster and more directly. This is joint work with Peter Lammich. DTSTART;TZID=Europe/Paris:20080603T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200806031 100 UID:LSVsemLSV.200806031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Accelerated Data-flow Analysis STATUS:CONFIRMED ATTENDEE;CN="Grégoire Sutre": MAILTO:no@spam.com DESCRIPTION: Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to spe ed up the iterative fix-point computation of reachable state s. Even if no termination guarantee is provided in theory\, successful results were obtained in practice by different to ols implementing this framework. In this talk\, we show how to extend the acceleration framework to data-flow analysis. Compared to a classical widening/narrowing-based abstract in terpretation\, the loss of precision is controlled here by t he choice of the abstract domain and does not depend on the way the abstract value is computed. We illustrate our approa ch on convex polyhedral data-flow analysis\, and we provide a cubic-time acceleration-based algorithm for solving interv al constraints with full multiplication. Joint work with Jé rôme Leroux. DTSTART;TZID=Europe/Paris:20080527T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805271 100 UID:LSVsemLSV.200805271100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Systèmes dynamiques linéaires : décidabilité de problèm es de sécurité STATUS:CONFIRMED ATTENDEE;CN="Emmanuel Hainry": MAILTO:no@spam.com DESCRIPTION: Les systèmes dynamiques décrivent un processus (trajectoi re\, phénomène naturel\, calcul) par l'espace sur lequel i l se produit\, sa dynamique et son point initial. Cette desc ription est suffisante pour définir toute l'évolution du s ystème mais ne donne guère d'idée sur l'ensemble de la tr ajectoire du système\, et il est crucial pour certains syst èmes d'assurer des propriétés sur cette trajectoire (par exemple\, la comète repassera infiniment souvent par un poi nt donné\, ou la Terre et la Lune ne se heurteront jamais o u encore la machine de Turing s'arr-bête).-A Nous défini rons quelques problèmes importants sur les systèmes linéa ires : atteignabilité point à point\, atteignabilité d'un hyperplan\, omega-limite. Nous montrerons que ces problème s qui sont dans le cas général (et m-bême dans des cas s imples) ind-Aécidables deviennent décidables si l'on cons idère des systèmes dynamiques linéaires. DTSTART;TZID=Europe/Paris:20080520T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805201 100 UID:LSVsemLSV.200805201100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: À la recherche de méthodes efficaces pour la vérification de réseaux de Petri à chronomètres en temps discret STATUS:CONFIRMED ATTENDEE;CN="Morgan Magnin": MAILTO:no@spam.com DESCRIPTION: A mesure que les réseaux proliféraient et prenaient une p lace temporelle et fonctionnelle des systèmes. Il convient ainsi de développer des formalismes permettant d'écrire et de valider les interactions entre les activités des proces seurs et les réseaux de communication. Les réseaux de Petr i temporels (RdPT) sont un de ces formalismes. Ils permetten t de modéliser la durée de différentes actions sous la fo rme d'un intervalle de temps. Ils peuvent par ailleurs -bê tre enrichis afin de repr-Aésenter des tâches susceptible s d'-bêtre suspendues puis relanc-Aées (réseaux de Petr i à chronomètres notés SwPN). Le temps dense consiste à considérer le temps comme une grandeur dense tandis que le temps discret l'assimile à une grandeur discrète. Les appl ications physiques évoluent par rapport au temps physique q ui est continu ; toutefois\, l'évolution du procédé n'est en général observée par le système informatique qui ne le pilote qu'à des instants particuliers (échantillonnage ou observations sporadiques). De plus\, le système de pilot age est composé de tâches qui sont exécutées sur un (ou plusieurs) processeur(s) dont le temps physique est discret. Le recours à un temps dense lors de la modélisation condu it donc à une surapproximation du système informatique. Ma is l'intér-bêt majeur du temps dense r-Aéside dans les abstractions symboliques associées\, pratiques à mettre en oeuvre et contenant l'explosion combinatoire des états. No us nous proposons de comparer les deux approches que sont le temps dense et le temps discret. Notre étude commence par un approfondissement des liens entre réseaux de Petri\, RdP T et SwPN en fonction de leur sémantique en temps dense et en temps discret. Nous en déduisons des résultats de déci dabilité importants sur les modèles en temps discret\, not amment la décidabilité de l'accessibilité d'état sur les SwPN bornés. Nous proposons ensuite une méthode efficace de calcul énumératif de l'espace d'états de modèles en t emps discret. Comme toute méthode purement énumérative\, celle-ci souffre toutefois de l'explosion combinatoire du no mbre d'états. C'est pourquoi nous concevons une méthode sy mbolique permettant de calculer l'espace d'états d'un modè le en temps discret en adaptant les techniques habituellemen t réservées au temps dense. Cette procédure nous permet a lors de vérifier des propriétés exprimées dans la logiqu e TCTL sur les SwPN en temps discret. Nous aboutissons à de s résultats très encourageants\, qui permettent d'analyser finement le comportement de modèles à chronomètres. DTSTART;TZID=Europe/Paris:20080513T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805131 100 UID:LSVsemLSV.200805131100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: On the use of formal models for proving cryptographic securi ty notions STATUS:CONFIRMED ATTENDEE;CN="Véronique Cortier": MAILTO:no@spam.com DESCRIPTION: Since the 1980s\, two approaches have been developed for an alyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity an d probability. This approach captures a strong notion of sec urity\, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of p rotocol executions in which cryptographic primitives are tre ated as black boxes. Since the seminal work of Dolev and Yao \, it has been realized that this latter approach enables si gnificantly simpler and often automated proofs. However\, th e guarantees that it offers have been quite unclear. In this talk\, we present several approaches that enable to obtain the best of both worlds: fully automated proofs and strong\, clear security guarantees. DTSTART;TZID=Europe/Paris:20080506T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805061 100 UID:LSVsemLSV.200805061100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Conflict-Tolerant Real-Time Features STATUS:CONFIRMED ATTENDEE;CN="Deepak D'Souza": MAILTO:no@spam.com DESCRIPTION: This work addresses the problem of detecting and resolving conflicts due to timing constraints imposed by features in r eal-time systems. We consider systems composed of a base sys tem with multiple "features" or "controllers"\, each of whic h independently advises the system on how to react to input events so as to conform to their individual specifications. We propose a methodology for developing such systems in a mo dular manner based on the notion of "conflict-tolerant" feat ures that are designed to continue offering advice even when their advice has been overridden in the past. We give a sim ple priority-based scheme for composing such features\, whic h guarantees the "maximal" use of each feature. We provide a formal framework for specifying such features\, and a compo sitional technique for verifying systems developed in this f ramework. This is joint work with Madhu Gopinathan\, Prahlad Sampath\, and S. Ramesh. DTSTART;TZID=Europe/Paris:20080429T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804291 100 UID:LSVsemLSV.200804291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Data Tree Patterns STATUS:CONFIRMED ATTENDEE;CN="Claire David": MAILTO:no@spam.com DESCRIPTION: One difficulty when we want to specify and manipulate XML d ocuments is to deal with data. Here we represent an XML docu ment as a tree labelled by an infinite alphabet to represent data values. We consider Boolean combinations of data tree patterns as a specification and query language for XML docum ents. Data tree patterns are tree patterns plus variable (in )equalities which express joins between data values. We cons ider the decidability and complexity of two problems. The fi rst one is the model checking problem. We show that it is DP -complete in general and already NP-complete when we conside r a single pattern. The second one is the satisfiability pro blem in the presence of a DTD. We show that it is in general undecidable and we identify several decidable fragments. DTSTART;TZID=Europe/Paris:20080408T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804081 100 UID:LSVsemLSV.200804081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Data Exchange and Schema Mappings in Open and Closed Worlds STATUS:CONFIRMED ATTENDEE;CN="Cristina Sirangelo": MAILTO:no@spam.com DESCRIPTION: Data exchange is the problem of translating a source databa se structured according to a source schema into a new databa se structured according to a given target schema\, known the relationship between the source and the target (schema mapp ing). Two semantics of data exchange and schema mappings hav e been proposed in the literature: an open-world (OWA) seman tics \, which allows target instances to contain arbitrary e xtensions of the data translated from the source\, a closed- world (CWA) semantics\, which only allows to exchange "as mu ch data as needed" to satisfy the constraints of the schema mapping. This work proposes a new mixed OWA/CWA semantics th at generalizes and unifies the previous ones: it allows diff erent target attributes to import data according to differen t semantics (either open-world or closed-world). This approa ch allows more flexibility in the specification of schema ma ppings and collapses in the known OWA and CWA approaches whe n target attributes are either all open or all closed. Under such mixed semantics\, we address two of the main issues in data exchange and schema management: query answering and co mposition of schema mappings. In particular we study how the ir complexities depend on the number of open attributes and we identify new conditions under which schema mappings compo se. DTSTART;TZID=Europe/Paris:20080401T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804011 100 UID:LSVsemLSV.200804011100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Relational data types and proofs with Moca STATUS:CONFIRMED ATTENDEE;CN="Richard Bonichon": MAILTO:no@spam.com DESCRIPTION: A relational data type is a concrete data type that declare s invariants or relations that are verified by its construct ors (see [1]). Moca [2] is a generic construction function g enerator for OCaml data types. It allows the definition of c omplex invariants on data typs\, which are then automagicall y managed. This talk will be divided into three parts: - I w ill first introduce some theoretical background about relati onal data types; - then I will show how one can specify and use invariants with Moca; - I will end the talk with a discu ssion about how one can apply such a tool in the context of automated theorem proving. We will in particular evoke the c ase of deduction modulo [3\, 4] and the zenon automated theo rem prover [5\, 6]. [1] On the implementation of constructor functions for non-free concrete data types. F. Blanqui\, T. Hardin et P. Weis [2] Moca [3] Theorem proving modulo\, rev ised version. G. Dowek\, Th. Hardin\, and C. Kirchner [4] Ta MeD: a Tableaud Method for Deduction Modulo. R. Bonichon [5] Zenon : An Extensible Automated Theorem Prover Producing Ch eckable Proof. R. Bonichon\, D. Delahaye and D. Doligez [6] Zenon DTSTART;TZID=Europe/Paris:20080325T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803251 100 UID:LSVsemLSV.200803251100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Extrapol : Extraction de politiques de sécurité depuis C STATUS:CONFIRMED ATTENDEE;CN="David Teller": MAILTO:no@spam.com DESCRIPTION: De nos jours\, les technologies les plus avancées disponib les pour garantir la s-bûret-Aé d'un système Linux vis- à-vis de processus malicieux ou bogués sont SELinux\, AppA rmor et quelques autres techniques comparables de pare-feux internes. Dans chacun des cas\, l'approche consiste à surve iller dynamiquement les interactions entre processus ou entr e processus et objets du système et à interdire celles qui ne sont pas explicitement autorisées par une "politique de sécurité". Si l'idée est intéressante\, son implantatio n se révèle souvent trop complexe pour la mise en oeuvre\, notamment en raison de la difficulté à valider une nouvel le politique de sécurité sans devoir tester exhaustivement tous les logiciels installés. C'est à ce point qu'entre e n jeu l'analyse statique : comment\, à partir d'une politiq ue de sécurité\, vérifier statiquement la compatibilité avec les logiciels déjà installés sur le système\, ou av ec de nouveaux logiciels à installer ? C'est sur ce problè me que nous travaillons dans le cadre d'Extrapol : à partir du modèle de sécurité imposé par SELinux\, des système s de types à la Hindley-Milner et des types dépendants\, n ous définissons un mécanisme d'extraction de politiques de sécurité à partir de bibliothèques et de fonctions écr ites en langage C. Au cours de cet exposé\, nous présenter ons le modèle de sécurité de SELinux\, la transformation de ce modèle en un jeu de contraintes sur le langage C et l e processus d'extraction. DTSTART;TZID=Europe/Paris:20080318T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803181 100 UID:LSVsemLSV.200803181100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Approximate Satisfiability and Equivalence STATUS:CONFIRMED ATTENDEE;CN="Michel de Rougemont": MAILTO:no@spam.com DESCRIPTION: We show how to approximate decision problems such as satisf iability of a formula by a structure\, or Equivalence betwee n two formulas\, such that we gain an exponential factor (or more) in complexity. A typical case is to decide if two Non -deterministic automata are equivalent: we decide the approx imate version in polynomial time whereas the exact version i s PSPACE complete. For Pushdown automata\, we decide the app roximate version in exponential time whereas the exact versi on is undecidable. DTSTART;TZID=Europe/Paris:20080311T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803111 100 UID:LSVsemLSV.200803111100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Objets d'interaction et réseaux différentiels STATUS:CONFIRMED ATTENDEE;CN="Damiano Mazza": MAILTO:no@spam.com DESCRIPTION: Nous commencerons par une introduction generale et le plus possible auto-contenue aux reseaux d'interaction et leurs ex tensions non-deterministes et concurrentes (reseaux multipor t\, reseaux differentiels...). On presentera en suite des re sultats plus specifiques\, notamment une definition categori que de modele denotationnel des combinateurs d'interaction\, basée sur la notion d'"objet d'interaction". On terminera en voyant comment cette notion peut etre appliquee aussi aux reseaux d'interaction diffrentiels. DTSTART;TZID=Europe/Paris:20080304T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803041 100 UID:LSVsemLSV.200803041100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: WYSINWYX: What You See Is Not What You eXecute STATUS:CONFIRMED ATTENDEE;CN="Thomas Reps": MAILTO:no@spam.com DESCRIPTION: What You See Is Not What You eXecute: computers do not execu te source-code programs; they execute machine-code programs that are generated from source code. Not only can the WYSINW YX phenomenon create a mismatch between what a programmer in tends and what is actually executed by the processor\, it ca n cause analyses that are performed on source code -- which is the approach followed by most security-analysis tools -- to fail to detect bugs and security vulnerabilities. To addr ess the WYSINWYX problem\, we have developed algorithms to r ecover information from stripped executables about the memor y-access operations that the program performs. These algorit hms are used in the CodeSurfer/x86 tool to construct interme diate representations that are used for browsing\, inspectin g\, and analyzing stripped x86 executables. Recently\, this infrastructure has been used to create a tool for looking fo r bugs in stripped device-driver executables. Joint work wit h G. Balakrishnan (UW)\, J. Lim (UW)\, and T. Teitelbaum (Co rnell and GrammaTech\, Inc.). DTSTART;TZID=Europe/Paris:20080219T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200802191 100 UID:LSVsemLSV.200802191100@lsv.ens-cachan.fr LOCATION:Salle Condorcet (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT SUMMARY: On decision problems for Probabilistic Büchi Automata STATUS:CONFIRMED ATTENDEE;CN="Nathalie Bertrand": MAILTO:no@spam.com DESCRIPTION: Probabilistic Büchi automata (PBA) are finite-state accept ors for infinite words where all choices are resolved by fix ed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. In this work we describe a complementation operat or for PBA and a discuss on several algorithmic problems for PBA. All interesting problems\, such as checking emptiness or equivalence for PBA or checking whether a finite transiti on system satisfies a PBA-specification\, turn out to be und ecidable. An important consequence of these results are seve ral undecidability results for stochastic games with incompl ete information\, modelled by partially-observable Markov de cision processes (POMDP) and w-regular winning objectives. F urthermore\, we study an alternative semantics for PBA where it is required that almost all runs for an accepted word ar e accepting\, which turns out to be less powerful\, but has a decidable emptiness problem. This is a joint work with Chr istel Baier and Marcus Groesser. DTSTART;TZID=Europe/Paris:20080205T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200802051 100 UID:LSVsemLSV.200802051100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Unions of Type Interpretations STATUS:CONFIRMED ATTENDEE;CN="Colin Riba": MAILTO:no@spam.com DESCRIPTION: The most flexible strong normalization proofs methods for v arious extensions of typed lambda-calculi use type interpret ations. Among them we distinguish Girard's reducibility cand idates\, Tait's saturated sets and interpretations based on biorthogonality. In this talk we compare these different int erpretations wrt their ability to handle rewriting and wrt t heir stability by union. We first propose a generalization o f the notion of neutral term in Girard's candidates that all ows to define them in a generic way. Concerning stability by union\, we recall that there are confluent typed rewrite sy stems that do not admit stable by union type interpretations . We present a necessary and sufficient condition for Girard 's candidate to be stable by union and a necessary and suffi cient condition for the closure by union of biorthogonals to be reduciblity candidates. The second condition is strictly more general than the first one\, and allows to define Tait 's saturated sets for rewriting in a uniform way. Moreover\, we show that for orthogonal constructor rewriting\, Girard' s candidates are stable by union. DTSTART;TZID=Europe/Paris:20080129T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200801291 100 UID:LSVsemLSV.200801291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Automates et logiques pour les mots sur un alphabet infini STATUS:CONFIRMED ATTENDEE;CN="Alexis Bès": MAILTO:no@spam.com DESCRIPTION: Plusieurs modèles d'automates ont été proposés pour man ipuler des mots sur un alphabet infini. Ces mots apparaissen t par exemple dans l'étude de problèmes de vérification d e systèmes distribués ou temporisés\, ou encore de manipu lation de données semi-structurées. Un objectif commun est d'obtenir un modèle à la fois simple et expressif\, et qu i conserve tant que possible les bonnes propriétés du mod le classique. Dans cet exposé on présentera un nouveau ty pe d'automate dans lequel l'alphabet A est vu comme le domai ne d'une structure M\, et les transitions de l'automate sont des formules du premier ordre écrites dans le langage de M . Ce modèle s'inspire directement de la notion de puissance généralisée de structures introduite par Feferman et Vau ght à la fin des années 1950\, et généralise un modèle introduit récemment par Choffrut et Grigorieff. On verra qu 'il possède de bonnes propriétés de clôture et de décis ion\, ainsi que plusieurs caractérisations logiques. On pr sentera également une extension du formalisme de Feferman et Vaught qui permet de pallier le manque d'expressivité du modèle initial. DTSTART;TZID=Europe/Paris:20080108T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200801081 100 UID:LSVsemLSV.200801081100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Equivalence of Labeled Markov Chains STATUS:CONFIRMED ATTENDEE;CN="Laurent Doyen": MAILTO:no@spam.com DESCRIPTION: We consider the equivalence problem for probabilistic machi nes. Two probabilistic machines are equivalent if every fini te sequence of observations has the same probability of occu rrence in the two machines. We show that deciding equivalenc e is polynomial for labeled Markov chains\, using a reductio n to the equivalence problem for probabilistic automata\, wh ich is known to be polynomial. We provide an alternative alg orithm to solve the latter problem\, which is based on a new definition of bisimulation for probabilistic machines. Then \, we consider the equivalence problem for labeled Markov de cision processes (LMDPs) which asks given two LMDPs whether for every way of resolving the decisions in each of the proc esses\, there exists a way of resolving the decisions in the other process such that the resulting probabilistic machine s are equivalent. The decidability of this problem remains o pen. We show that the strategies used to resolve the decisio ns can be restricted to be observation-based\, but may requi re infinite memory. This is a joint work with Tom Henzinger and Jean-Francois Raskin. DTSTART;TZID=Europe/Paris:20071218T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200712181 100 UID:LSVsemLSV.200712181100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Ordinal recursive bounds for Higman's lemma STATUS:CONFIRMED ATTENDEE;CN="Adam Cichon": MAILTO:no@spam.com DESCRIPTION: In this talk we give a constructive proof of Higman's lemma for strings generated over a finite alphabet enabling us to construct and characterise functions which bound the lengths of bad sequences. These bounding functions are described by ordinal-b­recursive definitions and their characterisatio n is achieved with reference to known ordinal-recursive hier archies of number­theoretic functions.-A DTSTART;TZID=Europe/Paris:20071204T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200712041 100 UID:LSVsemLSV.200712041100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Formal Analysis of Security APIs STATUS:CONFIRMED ATTENDEE;CN="Graham Steel": MAILTO:no@spam.com DESCRIPTION: Cash machines (ATMs) and other critical parts of the electr onic payment infrastructure contain tamper-proof hardware se curity modules (HSMs)\, which protect highly sensitive data such as the keys used to obtain personal identification numb ers (PINs). These HSMs have a restricted API that is designe d to prevent malicious intruders from gaining access to the data. However\, several attacks have been found on these API s\, as the result of painstaking manual analysis by experts such as Mike Bond and Jolyon Clulow. I have been carrying ou t research aimed at formalising and mechanising the analysis of these APIs. This talk will present some API attacks\, an d some automated formal analysis using theorem provers\, pro tocol analysis tools\, and the PRISM probabilistic model che cker. DTSTART;TZID=Europe/Paris:20071113T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200711131 100 UID:LSVsemLSV.200711131100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Integrating verification\, testing\, and learning for crypto graphic protocols STATUS:CONFIRMED ATTENDEE;CN="Vlad Rusu": MAILTO:no@spam.com DESCRIPTION: Joint work with Martijn Oostdijk (Riscure\, NL)\, Jan Tretma ns (EmbeddedSystems Institute\, NL)\, Rene de Vries (Radboud University Nijmegen\, NL)and T. Willemse (Eindhoven Univers ity of Technology\, NL) The verification of cryptographic pr otocol specifications is an activeresearch topic and has rec eived much attention from the formalverification community. By contrast\, the testing of actual black-boximplementations of protocols\, which is\, arguably\, as important asverific ation for ensuring the correct functioning of protocols in t he "real" world\, is little studied. We propose an approach for checkingsecrecy and authenticity properties not only on protocol specifications\,but also on black-box implementatio ns. The approach is compositional andintegrates ideas from v erification\, black-box testing\, and learning. Itis illustr ated on the Basic Access Control protocol implemented inbiom etric passports. DTSTART;TZID=Europe/Paris:20071109T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200711091 100 UID:LSVsemLSV.200711091100@lsv.ens-cachan.fr LOCATION:Amphi 112 (Bât. d'Alembert\, couloir du LPQM) END:VEVENT BEGIN:VEVENT SUMMARY: Making Random Choices Invisible to the Scheduler STATUS:CONFIRMED ATTENDEE;CN="Kostas Chatzikokolakis": MAILTO:no@spam.com DESCRIPTION: When dealing with process calculi and automata which express both nondeterministic and probabilistic behavior\, it is cu stomary to introduce the notion of scheduler to resolve the nondeterminism. It has been observed that for certain applic ations\, notably those in security\, the scheduler needs to be restricted so not to reveal the outcome of the protocol's random choices\, or otherwise the model of adversary would be too strong even for "obviously correct" protocols. In thi s talk I present a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms \, and I show how to apply it to solve the problem mentioned above. I also consider the definition of (probabilistic) ma y and must preorders\, and show that they are precongruences with respect to the restricted schedulers. Furthermore\, I show that all the operators of the language\, except replica tion\, distribute over probabilistic summation\, which is a useful property for verification. This framework is applied to the dining cryptographers problem\, where the scheduler p roblem comes into play. DTSTART;TZID=Europe/Paris:20071030T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200710301 100 UID:LSVsemLSV.200710301100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Decidability Results for Well-Structured Transition Systems with Auxiliary Storage STATUS:CONFIRMED ATTENDEE;CN="Rohit Chadha": MAILTO:no@spam.com DESCRIPTION: We consider the problem of verifying the safety of well-uctu red transition systems (WSTS) with auxiliary storage. WSTSs with storage are automata that have (possibly) infinitely ma ny control states along with an auxiliary store\, but which have a well-quasi-ordering on the set of control states. The set of reachable configurations of the tomaton may themselv es not be well-quasi-ordered because of the presence of the extra store. consider the coverability problem for such syst ems\, which asks if it is possible to reach a ntrol state (w ith some store value) that covers some given control state. Our main result that if control state reachability is decida ble for automata with some store and finitely control states then the coverability problem can be decided for WSTSs (wit h infinitely many ntrol states) and the same store\, provide d the ordering on the control states has some special proper ty. The special property we require is defined in terms of t he existence of a ranking ction compatible with the transiti on relation. We then show that there are several classes of nfinite state systems that can be viewed as WSTSs with an au xiliary storage. These can then be used to both reestablish old decidability results\, as well as discover new ones.Join t work with Mahesh Viswanathan. DTSTART;TZID=Europe/Paris:20071023T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200710231 100 UID:LSVsemLSV.200710231100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Structured specification of strategies in games on graphs STATUS:CONFIRMED ATTENDEE;CN="R. Ramanujam": MAILTO:no@spam.com DESCRIPTION: The analysis of non-zero-sum games proceeds by determining t he response of players to opponents' strategies. However\, t his requires each player to know what every other player wou ld do in every possible situation\, which is quite unrealist ic in large games. We look at situations where players const ruct bounded memory strategies in a structured manner\, wher e the opponent's strategy may be known only by its propertie s. In the new setting we study the algorithmic question of f inding best response for a player. We also present a simple modal logic to reason about strategies and show that checkin g assertion on a game graph is decidable. DTSTART;TZID=Europe/Paris:20070921T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200709211 100 UID:LSVsemLSV.200709211100@lsv.ens-cachan.fr LOCATION:Salle Condorcet (Bât. d'Alembert) END:VEVENT BEGIN:VEVENT SUMMARY: Automatic Generation of Loop Invariants STATUS:CONFIRMED ATTENDEE;CN="Deepak Kapur": MAILTO:no@spam.com DESCRIPTION: An overview of the recent work in our group on automatic gen eration of loop invariants using different approaches will b e presented. Particularly\, a heuristic based on quantifier- elimination will be reviewed. Methods based on abstract inte rpretation and ideal-theoretic semantics of programming lang uage constructs will be discussed. An approach based on solv ing recurrences will be presented. These methods have been i mplemented and successfully tried on many programs implement ing nontrivial number theoretic functions. Some preliminary ideas about how to generalize these approaches to work on da ta types other than numbers will be discussed. DTSTART;TZID=Europe/Paris:20070703T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200707031 100 UID:LSVsemLSV.200707031100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Formal Verification of Security Protocols using Automata STATUS:CONFIRMED ATTENDEE;CN="Roberto Segala": MAILTO:no@spam.com DESCRIPTION: In this talk we will show how it is possible to use Probabil istic Automata for the verification of security protocols\, and in particular how simulation-based proofs can be employe d. The simulation method is useful in general to reduce the analysis of global properties to the analysis of local prope rties of single computational steps. We extend the same idea to analyze global security properties. Since security holds under computational assumptions and up to a negligible prob ability of error\, we propose a notion of polynomially accur ate simulation relation for Probabilistic Automata and we il lustrate it by analyzing a simple authentication protocol. I n particular we show how the negation of the step condition of our simulation relation becomes the definition of a forge r for a signature scheme. DTSTART;TZID=Europe/Paris:20070619T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200706191 100 UID:LSVsemLSV.200706191100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Automatic Analysis of LAN Infrastructures STATUS:CONFIRMED ATTENDEE;CN="Christoph Weidenbach": MAILTO:no@spam.com DESCRIPTION: Important guarantees for LAN infrastructures include connect ivity\, error detection/recovery\, robust changes and securi ty. In the talk I will develop a LAN infrastructure model in first-order logic enabling automatic analysis of such prope rties. The model starts at the ethernet layer of the TCP/IP stack and ranges up to application protocols such as DHCP. DTSTART;TZID=Europe/Paris:20070614T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200706141 100 UID:LSVsemLSV.200706141100@lsv.ens-cachan.fr LOCATION:Amphi 109 N (bât L. de Vinci) END:VEVENT BEGIN:VEVENT SUMMARY: Local Testing of Message Sequence Charts is Difficult STATUS:CONFIRMED ATTENDEE;CN="K. Narayan Kumar": MAILTO:no@spam.com DESCRIPTION: Message sequence charts are an attractive visual formalism u sed to specify distributed communicating systems. One way to test such a system is to substitute a component by a test p rocess and observe its interaction with the rest of the syst em. We consider the question of whether we can characterize the distributed behaviour of such a system based on local ob servations. The main difficulty is that local observations c an combine in unexpected ways to define implied scenarios no t present in the original specification. We consider variant s of this simple notion of testing. In most cases the proble m turns out to be undecidable. (Joint work with Puneet Bhate ja\, Paul Gastin and Madhavan Mukund) DTSTART;TZID=Europe/Paris:20070529T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200705291 100 UID:LSVsemLSV.200705291100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT SUMMARY: Local Testing of Message Sequence Charts is Difficult STATUS:CONFIRMED ATTENDEE;CN="Madhavan Mukund": MAILTO:no@spam.com DESCRIPTION: We consider message sequence charts enriched with timing con straints between pairs of events. As in the untimed setting\ , an infinite family of time-constrained message sequence ch arts (TC-MSCs) is generated using an HMSC?a finite-state aut omaton whose nodes are labelled by TC-MSCs. A timed MSC is a n MSC in which each event is assigned an explicit time-stamp . A timed MSC covers a TC-MSC if it satisfies all the time c onstraints of the TC-MSC. A natural recognizer for timed MSC s is a message-passing automaton (MPA) augmented with clocks . The question we address is the following: given a timed sy stem specified as a time-constrained HMSC H and an implement ation in the form of a timed MPA A\, is every TC-MSC generat ed by H covered by some timed MSC recognized by A? We give a complete solution for locally synchronized time-constrained HMSCs\, whose underlying behaviour is always regular. We al so describe a restricted solution for the general case. This is joint work with S Akshay and K Narayan Kumar. DTSTART;TZID=Europe/Paris:20070522T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200705221 100 UID:LSVsemLSV.200705221100@lsv.ens-cachan.fr LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT END:VCALENDAR