BEGIN:VCALENDAR VERSION:2.0 CALSCALE:GREGORIAN METHOD:PUBLISH URL;VALUE=URI: http://www.lsv.ens-cachan.fr/Seminaires/ical.php X-WR-CALNAME:Séminaires du Laboratoire Spécification et Vérification X-WR-TIMEZONE:Europe/Paris X-WR-CALDESC:Calendrier des séminaires du LSV 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 STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Alexander Heußner - (to be announced) 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/anciens?se m=201204101100 UID:semLSV.201204101100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Amélie Gheerbrant - (to be announced) 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/anciens?se m=201204031100 UID:semLSV.201204031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : David Baelde - (to be announced) 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/anciens?se m=201203221100 UID:semLSV.201203221100 LOCATION:Salle ? END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Cezara Drăgoi - (to be announced) 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/anciens?se m=201203201100 UID:semLSV.201203201100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Barnaby Martin - (to be announced) 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/anciens?se m=201203121400 UID:semLSV.201203121400 LOCATION:Amphithéâtre 121 N (Bâtiment Léonard de Vinci) END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Tobias Heindel - (to be announced) 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/anciens?se m=201203061400 UID:semLSV.201203061400 LOCATION:Salle ? END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Emmanuel Filiot - (to be announced) 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/anciens?se m=201203061100 UID:semLSV.201203061100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:TENTATIVE ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Mathieu Sassolas - (to be announced) 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/anciens?se m=201202281100 UID:semLSV.201202281100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Swan Dubois - Tolerating Transient\, Permane nt\, and Intermittent Failures 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 that some elements of the system are subject to faults (failure\, memory corruption\, hacking\, ...) become impossible to elude . Faults can be classified according to duration\, span\, or n ature. In this talk\, we focus on distributed systems that si multaneously tolerate several kinds of faults using three cl assical problems as case studies. We present first a distrib uted protocol simulating a single-writer multi-reader atomic register in the presence of transient faults and of permane nt crash faults. This protocol relies on two re-usable tools : a communication primitive and a bounded timestamp scheme. Then\, we study logical clock weak synchronization in the pre sence of transient faults and of intermittent Byzantine faul ts. We prove several impossibility results and provide a pro tocol that is optimal both with respect to impossibility res ult and with respect to recovery time. Finally\, we define th ree new fault tolerance schemes in distributed systems that are subject to transient faults and to intermittent Byzantin e faults. We design a protocol constructing a wide class of spanning trees that is optimal with respect to fault toleran ce metrics defined for these three schemes. DTSTART;TZID=Europe/Paris:20120216T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201202161400 UID:semLSV.201202161400 LOCATION:Salle ? END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : B Srivathsan - Better abstractions for time d automata 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 abstract ions preserve underlying simulation relations on the state s pace 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 that A-lu abstraction is the biggest abstraction with respect to LU-bounds that is sound and complete for reachability. We a lso provide an efficient technique to use the A-lu abstracti on to solve the reachability problem. Joint work with Frédér ic Herbreteau and Igor Walukiewicz. DTSTART;TZID=Europe/Paris:20120214T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201202141100 UID:semLSV.201202141100 LOCATION:Amphithéâtre Tocqueville END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Mohamed Faouzi Atig - Counter-Example Guide d Fence Insertion under TSO 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 corre sponding to the addition of an unbounded store buffer betwee n each processor and the main memory. We show that the reach ability problem for a program under TSO is decidable. Then\, we propose a counter-example guided fence insertion procedu re. The procedure is augmented by a placement constraint tha t allows the user to choose places inside the program where fences may be inserted. For a given placement constraint\, we automatically infer all minimal sets of fences that ensure correctness. We have implemented a prototype and run it succ essfully on all standard benchmarks together with several ch allenging examples that are beyond the applicability of exis ting methods. [This talk will be based on: (1) POPL'10 pape r with Ahmed Bouajjani\, Burckhardt and Madanlal Musuvathi\, a nd (2) TACAS'12 paper with Parosh Abdulla\, Yu-Fang Chen\, Car l Leonardsson and Ahmed Rezine] DTSTART;TZID=Europe/Paris:20120131T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201201311100 UID:semLSV.201201311100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Giuseppe Lipari - Component-based analysis of real-time systems 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 a dded to existing software. At the same time\, due to the incr easing computational power of the hardware platforms and to the pressure to reduce the costs\, software that in the past was run on different computational nodes\, is now being integ rated onto a single node. An appealing way to reduce comple xity is to apply a component-based real-time design methodol ogy. A real-time system can be seen as a set of interacting components\, each one providing a well-defined subset of func tionalities\, whose integration produces the final system beh avior. A component-based methodology is successful only if i t can effectively reduce the complexity. To achieve this goa l\, the system designer must be able to 1) analyze and valida te each component in isolation from the rest of the system\, 2) summarize its properties and requirements into simpler in terfaces\, 3) perform the final integration analysis and vali dation on the component interfaces. In this talk\, the autho r will give an overview of current techniques for component- based analysis of real-time systems\, with a look at their po ssible use in avionics and automotive systems. Then\, a possi ble research agenda will be discussed\, highlighting the shor tcomings of current analysis and how to improve on it. DTSTART;TZID=Europe/Paris:20120124T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201201241100 UID:semLSV.201201241100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Dominique Unruh - Everlasting Security thro ugh Quantum Cryptography 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 a s the underlying encryption schemes. And we do not know whet her these might not be broken at some point in the future. T his leaves us in a difficult situation: If we process highly sensitive data using cryptographic protocols\, an attacker m ight simply record all messages. Should the underlying encry ption 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 records) s uch a situation is not acceptable. A way out is "everl asting security". A protocol with everlasting security guarantees that all data involved in the protocol stays secu re\, even if at some point in the future all the underlying e ncryption schemes are broken. Unfortunately\, with traditiona l cryptographic techniques\, everlasting security can only be achieved in very limited situations. In this talk\, we expl ain how everlasting security can be achieved for a wide vari ety 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/anciens?se m=201201171100 UID:semLSV.201201171100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre-Alain Fouque - Cryptanalysis 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 computationa lly-hard problem on which the security of a scheme is based; at the scheme level\, attacking the scheme directly when its security is not based on some hard problems (this is the ca se when specific instances of a hard problems are used) or i n symmetric cryptography; finally at the implementation leve l\, when side channel information can be used. In this talk\, I will make a survey of some cryptanalytic techniques and d escribe my contributions towards this field. DTSTART;TZID=Europe/Paris:20111129T140000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201111291400 UID:semLSV.201111291400 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Sophie Pinchinat - Uniform strategies 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 featu res of computing systems\, attacker's dialog with a security system\, etc. Also\, such games naturally arise in logic\, e.g. as satisfiability games for mu-calculus formulas. Recently\, some kind of imperfect information games have been used to provide the semantics of logics\, as for Dependence Logic. W e propose the notion of "uniform strategy" which u nifies the aforementioned approaches\, and even provides new model-checking games for complex logics\, e.g. combining time and knowledge. Our definition relies on pairs of parameters : an equivalence relation between plays\, and a uniformity c ondition 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 observ e and recall what happened during the play (The perfect reca ll-imperfect recall spectrum lies in this parameter). Additi onally\, the uniformity condition can express many aspects. I t can capture the nature of the strategy\, e.g. that it is ob servation-based\, as needed in the very standard imperfect in formation games setting. It can characterize non-regular pro perties of strategies\, e.g. that strategies maintain the opp onent's uncertainty about some secret\, as considered in game s with opacity condition. In this talk\, we will explain and motivate our notion of uniform strategy\, and relate it to v arious examples from the literature: namely\, imperfect infor mation games\, games with opacity condition\, emptiness of alt ernating automata\, first-order dependence logic model-checki ng games\, epistemic temporal logic model-checking games. If time left\, we will address decidability and complexity issue s by scanning computational hypothesis one may require on th e pair of parameters. DTSTART;TZID=Europe/Paris:20111129T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201111291100 UID:semLSV.201111291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Stefan Göller - The Computational Comp lexity of Verifying One-Counter Processes 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 p rocesses (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 pl an to show that it is PSPACE-complete to decide strong bisim ulation equivalence for OCPs. The previously best known uppe r bound for this problem was 3-EXPSPACE. The same problem tu rns out to be NL-complete when the processes are described b y deterministic one-counter automata. In the second part of the talk\, I plan to discuss a technique for proving lower b ounds by employing two known results from complexity theory: (i) Converting a natural number in Chinese remainder presen tation into binary presentation is in logspace-uniform NC^1 and (ii) PSPACE is AC^0-serializable. With the latter one ca n prove that there exists a fixed CTL formula for which mode l checking of OCPs is PSPACE-hard. With the same technique one can show some further lower bounds\, as for example the f ollowing one: The emptiness problem for timed automata with two clocks but with modulo tests is PSPACE-complete even if all numbers are encoded in unary. The results were obtained in joint works with Stanislav Böhm\, Petr Jancar and Ma rkus Lohrey. DTSTART;TZID=Europe/Paris:20111122T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201111221100 UID:semLSV.201111221100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Charles Bouillaguet - Symbolic Methods for the Automatic Search of Attacks Against Some Block Ciphers 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 goal is\, in most cases\, to retrieve this secret key using less t ime than exhaustive search and asking less encryptions/decry ptions to the black box than the whole codebook. Several re searchers had previously observed that the Advanced Encrypti on Standard (AES)\, the most widespread block cipher\, had a r elatively simple algebraic description over the field with 2 56 elements\, because of its byte-oriented design. However\, t his property has not been harnessed by cryptanalysts to this day. In particular the (tempting) approach consisting in wr iting down the equations describing the AES\, and trying to s olve them directly using off-the-shelf tools such as SAT-sol vers\, has systematically failed to provide any result. In t his talk\, I will present the results we obtained using a sli ghtly different method. We have designed tools that take as input a system of AES-like equations\, and that search for an efficient ad hoc solving procedure. The result of these too ls is the source code of a solver that can only solve the in put system\, but which can in some cases be efficient (its co mplexity 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 algorithm for SAT\, the Knuth-Bendix completion algorithm\, or the reso lution algorithm for first-order logic. These tools found\, nearly automatically\, the best known Low-Data-Complexity att acks on reduced versions of the AES\, and the best known atta ck on the full versions of AES-derived primitives\, such as t he Message Authentication code Pelican-MAC\, and the stream c ipher LEX. DTSTART;TZID=Europe/Paris:20111115T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201111151100 UID:semLSV.201111151100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Peter Schrammel - Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Fl ow Programs 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-st ate analysis for this problem. Two main techniques for ensur ing the termination of such an analysis are acceleration and widening (within the abstract interpretation framework). A cceleration-based methods lead to exact results\, but they gu arantee termination only for a restricted class of programs. Widening is less precise and less predictable but does not have this limitation. Abstract acceleration integrates accel eration techniques into the abstract interpretation framewor k\, such as to reduce the need for widening and thus to impro ve precision. All these techniques however require the enum eration of the Boolean state-space\, which leads to a state-s pace explosion even for medium-sized Lustre programs. In thi s talk we propose a solution by extending numerical accelera tion to logico-numerical acceleration. We define logico-nume rical abstract acceleration methods based on a partial decou pling of Boolean and numerical transitions and we show how w ell-chosen partitioning techniques make them effective. Expe rimental results show that incorporating these methods in a verification tool based on abstract interpretation provides not only significant advantage in terms of precision\, but al so a gain in performance. DTSTART;TZID=Europe/Paris:20111108T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201111081100 UID:semLSV.201111081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre-Yves Strub - Toward Machine-Checked Program Verification for Concrete Cryptography ATTENDEE;CN=Pierre-Yves Strub: MAILTO:no@spam.com DESCRIPTION: Type systems\, relational logics\, and interactive proof assis tants are effective tools for verifying the security of prog rams and systems that rely on cryptography. They can provide automation\, modularity and scalability. As illustrated in r ecent case studies\, they can be usefully applied to large se curity protocols and applications [Bhargavan et al.\, 2008\, F ournet et al.\, 2009]. However\, their models traditionally r ely on abstract assumptions on the underlying cryptographic primitives\, expressed in symbolic models. Cryptographers usu ally reason on security assumptions in lower-level models th at precisely account for the complexity and probability of a ttacks. These models are more complex and realistic\, but rec ent results suggest thay they are also amenable to formal au tomated verification [Blanchet\, 2006\, Barthe et al.\, 2009\, A car et al.\, 2011]. I will present our on-going work in adap ting and extending our programming and verification framewor k based on refinement types for ML programs [Bengtson et al. \, 2008\, Bhargavan et al.\, 2010\, Fournet\, 2011] which current ly uses a combination of automated proofs (using Z3\, an SMT solver) and interactive proofs (using Coq)\, in order to prod uce machine-checked security proofs of cryptographic program s and libraries under concrete computational assumptions. T his work is part of the “Secure Distributed Computatio ns” group of the “MSR-INRIA Joint Centre”. DTSTART;TZID=Europe/Paris:20110927T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201109271100 UID:semLSV.201109271100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Myrto Arapinis - Keeping track of your frie nds and enemies: privacy threats of new mobile technologies ATTENDEE;CN=Myrto Arapinis: MAILTO:no@spam.com DESCRIPTION: Joint work with Loretta Mancini\, Eike Ritter\, and Mark Ryan. The proliferation of portable computing devices\, such as m obile phones\, Bluetooth devices\, and RFID tags\, has lead to a range of new computer security problems. In order to fulfi l their goals\, these devices need to report our movements to service providers such as mobile phone network operators\, b anks\, and governments. While most of users accept that the s ervice providers can track their physical movements\, few wou ld be happy if an arbitrary third party could do so. Such a possibility would enable all kinds of undesirable behaviours \, ranging from criminal stalking to more mundane monitoring 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 user. These p rotocols usually include cryptography and make use of tempor ary identifiers\, in an effort to achieve the aim of untracea bility by third parties. At CSF'10\, we presented a formal f ramework for analysing untraceability/unlinkability in the a pplied pi calculus. We used our framework to show that Frenc h e-Passports are traceable\, while British ones aren't. In t his talk\, I will present you our work on the analysis of Uni versal Mobile Telecommunication System (UMTS) protocols. I w ill show you a problem we have identified with the UMTS auth entication and key establishment protocol: although mobile p hones use temporary identities to identify themselves to the Network\, a replayed message can be used to identify a parti cular mobile phone. Our attack exploits the fact that the vi ctim's phone will reply with subtly different error messages \, depending on whether the replayed request is associated wi th it or with a different phone. To thwart this attack\, we p ropose a modification of the protocol\, and verify the propos ed fix using our framework and the ProVerif tool. DTSTART;TZID=Europe/Paris:20110920T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201109201100 UID:semLSV.201109201100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Giorgio Delzanno - Verification of Ad hoc N etworks: Unreliability and Time 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 prese nce of node and communication failures. We consider here dif ferent types of failures: intermittency\, crash and restart o f single nodes\, loss and conflicts of broadcast messages. In the second part we present an extension of the model in whi ch nodes are specified by timed automata and\, for the new mo del\, discuss parameterized reachability problems for differe nt classes of topologies. DTSTART;TZID=Europe/Paris:20110712T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201107121100 UID:semLSV.201107121100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Tamara Rezk - Reasoning about Web Security 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 applicati ons. In this talk\, I will: overview security vulnerabiliti es that arise from web applications specificities such as co de injection and gadget inclusion; and describe proposals ba sed on language-based security approaches. DTSTART;TZID=Europe/Paris:20110705T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201107051100 UID:semLSV.201107051100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Clemens Kupke - Coalgebraic Logics and Tabl eaux 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 algorit hmic properties on the other hand. Extensions of basic modal logic are obtained by allowing for ontological reasoning (d escription logics) and by adding the ability to specify ongo ing\, possibly infinite behaviour (fixpoint logics). Other va riations of basic modal logic are designed to fit specific s emantic domains such as modal logics for Markov chains\, game frames or neighbourhood structures. In my talk I am going to present coalgebraic modal logic as a general framework in which the above mentioned variations of basic modal logic c an be studied in a uniform way. In particular\, I am going to describe tableau calculi that yield generic decidability pr oofs for the coalgebraic mu-calculus and coalgebraic descrip tion logics. As corollaries we obtain previously unknown Exp time-decidability results for these logics. DTSTART;TZID=Europe/Paris:20110614T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201106141100 UID:semLSV.201106141100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Alexander Heußner - Beyond Control-St ate Reachability for Communicating Pushdown Systems 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 t hat communicate via TCP or MPI. Recent publications focus on the influence of constraining the network architecture o n basic decidability questions\, but do not allow to derive positive results beyond control-state reachability when ass uming syntactic and semantic restrictions that are still & quot;applicable" in practice. We present first ideas on leaving behind interleaving semantics in order to verif y MSO properties based on a graph grammar based representat ion of a system's partial-order behaviour. DTSTART;TZID=Europe/Paris:20110531T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201105311100 UID:semLSV.201105311100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Madhavan Mukund - Assembling Sessions ATTENDEE;CN=Madhavan Mukund: MAILTO:no@spam.com DESCRIPTION: Sessions are a central paradigm in Web services\, as they all ow the implementation of decentralized transactions with mul tiple participants. Sessions enable the cooperation of workf lows while at the same time avoiding the mixing of workflows from distinct transactions. Several languages such as BPE L\, 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 languag es makes the properties of the implemented services undecida ble. 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 diale ct of Petri nets that allows the verification of important p roperties of web services in terms of coverability in Petri nets. This is joint work with Philippe Darondeau and Loic H elouet. DTSTART;TZID=Europe/Paris:20110524T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201105241100 UID:semLSV.201105241100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Mahesh Viswanathan - Approximating Hybrid S ystems 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 pro cesses tend to be conservative and suboptimal\, the most popu lar way to model and analyze such systems is using hybrid sy stems\, that have finitely many control states to model discr ete behavior and finitely many real valued variables that ev olve continuously with time to model the interaction with th e physical world. Despite considerable progress in the last couple of decades\, the automated verification of cyber physi cal systems remains stubbornly challenging. In this talk we will discuss one approach to making the analysis more scalab le\, namely\, by automatically constructing "simpler" ;\, "smaller" models\, and then analysing these appr oximated models. We will present a couple of techniques to a pproximate hybrid models\, based on the Stone-Weierstrauss Th eorem and counter-example guided abstraction-refinement (CEG AR)\, and discuss their applications to automated verificatio n. DTSTART;TZID=Europe/Paris:20110517T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201105171100 UID:semLSV.201105171100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Ralf Treinen - Towards better tools for the analysis and quality assurance of FOSS distributions 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 both for the quality assurance process of distributions as for t he management of individual installations. The first part of this talk will give an overview of some of the results obta ined in the EDOS and Mancoosi European projects on the analy sis of inter-package relationships. We will focus on the too ls that came out of these research projects\, and discuss the way how these are currently put to use. In the second part of the talk I will present recent results on deciding prope rties that range over all possible future evolutions of a cu rrent component repository. The properties we are interested in concern the coherent component installations permitted i n any future. We show that a certain class of these properti es can be decided by checking a finite set of repositories t hat is representative for the infinite set of all possible f utures. 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/anciens?se m=201104261100 UID:semLSV.201104261100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Lukasz Kaiser - Playing games when states h ave rich structure 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 cases \, but can be a hindrance in others\, for example when studyin g games on pushdown graphs or on timed automata. To better u nderstand how internal structure of the states can influence behaviour of the players\, we introduce a general model of g ames with structured states. In our model\, actions of the pl ayers are given by structure rewriting rules and winning con ditions by logic formulas. In case of games with perfect inf ormation\, we show that the structure of the states can be ex ploited to create simple strategies\, sometimes even when the number of states in the game is infinite. This is similar t o games on pushdown graphs and indeed\, we prove a close rela tionship between pushdown games and our model when rewriting rules are of a certain simple form. DTSTART;TZID=Europe/Paris:20110412T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201104121100 UID:semLSV.201104121100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre Ganty - Pattern-based Verification f or Multithreaded Programs 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 expre ssion over the alphabet of program transitions of the form w 1* ... wn*. For multithreaded programs\, the alphabet of the pattern is given by the synchronization operations between threads. After introducing the model\, we study the complexit y of pattern-based verification for abstracted multithreaded . While unrestricted verification is undecidable for abstrac ted multithreaded programs with recursive procedures and PSP ACE-complete for abstracted multithreaded while-programs\, we show that pattern-based verification is NP-complete for bot h classes. Using recent results about Parikh images of conte xt-free languages and semilinear sets\, we show that pattern- based verification becomes polynomial when the number of thr eads\, the longest acyclic path in the call graph\, and the si ze of the pattern are fixed\, but the procedures can still be arbitrarily large. DTSTART;TZID=Europe/Paris:20110405T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201104051100 UID:semLSV.201104051100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Eugene Asarin - Entropy of timed languages ATTENDEE;CN=Eugene Asarin: MAILTO:no@spam.com DESCRIPTION: For timed languages\, we define measures of their size: volum e for a fixed finite number of events\, and entropy (growth r ate) as asymptotic measure for an unbounded number of events . These measures can be used for comparison of languages\, an d the entropy can be viewed as information contents of a tim ed language. In case of languages of deterministic timed aut omata\, we give exact formulas for volumes. Next we character ize the entropy\, using methods of functional analysis\, as a logarithm of the leading eigenvalue (spectral radius) of a p ositive integral operator. We devise several methods to comp ute the entropy: a symbolical one for so-called "1 1/2- clock" automata\, and two numerical ones: one using tech niques of functional analysis\, another based on discretizati on. (The talk is based on Concur'09\, FORMATS'09\, FSTTCS'10 articles with Aldric Degorre) DTSTART;TZID=Europe/Paris:20110322T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201103221100 UID:semLSV.201103221100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Anne Bouillard - Residuation of tropical se ries: rationality issues ATTENDEE;CN=Anne Bouillard: MAILTO:no@spam.com DESCRIPTION: Decidability of existence\, rationality of delay controllers and robust delay controllers are investigated for systems wi th time weights in the tropical and interval semirings. Dep ending on the (max\,+) or (min\,+)-rationality of the series s pecifying the controlled system and the control objective\, c ases are identified where the controller series defined by r esiduation is rational\, and when it is positive (i.e.\, when delay control is feasible). When the control objective is sp ecified by a tolerance\, i.e. by two bounding rational series \, a nice case is identified in which the controller series is of the same rational type as the system specification ser ies. DTSTART;TZID=Europe/Paris:20110308T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201103081100 UID:semLSV.201103081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Valentin Goranko - A Logical Framework for Capturing the Dynamics of Information and Abilities of Playe rs in Multi-Player Games: a preliminary report 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\, im perfect\, or simply wrong information that they may have abou t the game and about the course of the play. In this talk\, a fter some motivating examples I will introduce a variation o f the multi-agent logic ATL as a logical framework for captu ring the interplay between the dynamics of information and t he dynamics of abilities of players. This framework takes in to account both the a priori information of players with res pect to the game structure and the empirical information tha t players develop over the course of an actual play. It asso ciate with them respective information relations and notions of `a priori' and `empirical' strategies and strategic abil ities. I will discuss the problem of model checking of state ments formalized in the new logic under different assumption s about the abilities of the players to observe\, remember\, a nd reason. Most of the talk will be based on a joint work w ith Peter Hawke (now at Stanford Univ.) DTSTART;TZID=Europe/Paris:20110222T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201102221100 UID:semLSV.201102221100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Byron Cook - Proving that programs eventual ly do something good 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)\, an d those that result in the software not doing something usef ul (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certif y that software cannot crash. But\, based on Alan Turing's p roof of the halting problem's undecidablity\, many have consi dered the dream of automatically proving the absence of hang s to be impossible. While not refuting Turing's original res ult\, recent research now makes this dream a reality. This le cture will describe this recent work and its application to industrial software. Bio: Dr. Byron Cook is a Principal Re searcher at Microsoft Research in Cambridge\, UK as well as P rofessor of Computer Science at Queen Mary\, University of Lo ndon. He is one of the developers of the Terminator program termination proving tool\, as well as the SLAM software mode l checker. See research.microsoft.com/~bycook/ for more inf ormation. DTSTART;TZID=Europe/Paris:20110218T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201102181100 UID:semLSV.201102181100 LOCATION:Amphithéâtre Marie Curie (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Olivier Serre - Recursion Schemes and their Automata Models 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 re cursion schemes\, which can be thought as a deterministic re writing system over terms (essentially\, the simply-typed lam bda calculus with recursion). The second one are higher-ord er pushdown automata\, which are an extension of pushdown aut omata that uses stacks of stacks instead of stacks of symbol s. The first part of the talk will be devoted to present th e models and give examples. The second part\, will focus on p roperties of the trees generated by such models (in particul ar\, the decidability of the monadic second order logic)\, and will illustrate the advantages of automata techniques when working with such objects. DTSTART;TZID=Europe/Paris:20110215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201102151100 UID:semLSV.201102151100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Alexander Rabinovich - Temporal logics over linear time domains are in PSPACE 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 interest ing classes of linear orders. DTSTART;TZID=Europe/Paris:20110125T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201101251100 UID:semLSV.201101251100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Moshe Y. Vardi - Symbolic Techniques in Pro positional Satisfiability Solving 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 i s becoming known as the "SAT Revolution". Essentia lly all state-of-the-art SAT solvers are based on the Davis- Putnam-Logemann-Loveland (DPLL) technique\, augmented with ba ckjumping and conflict learning. Much of current research in this area involves refinements and extensions of the DPLL t echnique. Yet\, due to the impressive success of DPLL\, little effort has gone into investigating alternative techniques. This work focuses on symbolic techniques for SAT solving\, wi th the aim of stimulating a broader research agenda in this area. Refutation proofs can be viewed as a special case of c onstraint propagation\, which is a fundamental technique in s olving constraint-satisfaction problems. The generalization lifts\, in a uniform way\, the concept of refutation from Boo lean satisfiability problems to general constraint-satisfact ion problems. On the one hand\, this enables us to study and characterize basic concepts\, such as refutation width\, usin g tools from finite-model theory. On the other hand\, this en ables us to introduce new proof systems\, based on representa tion classes\, that have not been considered up to this point . We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations\, and co mpare their strength to well-known proof systems\, such as re solution\, the Gaussian calculus\, cutting planes\, and Frege s ystems of bounded alternation-depth. In particular\, we show that refutations by ODBBs polynomially simulate resolution a nd can be exponentially stronger. We then describe an effort to turn OBDD refutations into OBBD decision procedures. The idea of this approach\, which we call "symbolic quantif ier 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 dire ct comparison with the DPLL-based ZChaff\, as well as evaluat e a variety of optimization techniques for the symbolic appr oach. In comparing the symbolic approach to ZChaff\, we evalu ate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZC haff dominates for many classes of formulas\, the symbolic ap proach is superior for other classes of formulas. Finally\, w e turn our attention to Quantified Boolean Formulas (QBF) so lving. Much recent work has gone into adapting techniques t hat were originally developed for SAT solving to QBF solving . In particular\, QBF solvers are often based on SAT solvers. Most competitive QBF solvers are search-based. Here we desc ribe an alternative approach to QBF solving\, based on symbol ic quantifier elimination. We extend some symbolic approache s for SAT solving to symbolic QBF solving\, using various dec ision-diagram formalisms such as OBDDs and ZDDs. In both ap proaches\, QBF formulas are solved by eliminating all their q uantifiers. Our first solver\, QMRES\, maintains a set of clau ses represented by a ZDD and eliminates quantifiers via mult i-resolution. Our second solver\, QBDD\, maintains a set of OB DDs\, and eliminate quantifiers by applying them to the under lying OBDDs. We compare our symbolic solvers to several comp etitive search-based solvers. We show that QBDD is not compe titive\, but QMRESS compares favorably with search-based solv ers on various benchmarks consisting of non-random formulas. DTSTART;TZID=Europe/Paris:20101103T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201011031100 UID:semLSV.201011031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Christophe Morvan - On probabilistic regula r graphs 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 advoc ate 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/anciens?se m=201011161100 UID:semLSV.201011161100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Arnaud Sangnier - Parameterized Verificatio n of Ad Hoc Networks 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/anciens?se m=201010191100 UID:semLSV.201010191100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : David Rajchenbach-Teller - OPA -- reconquer ing the web ATTENDEE;CN=David Rajchenbach-Teller: MAILTO:no@spam.com DESCRIPTION: For many\, the Web is Wikipedia\, Google Maps and hundreds of other rich applications\, both powerful and usable from anywh ere. For others\, it is a security nightmare\, full of holes\, both low-level and high-level\, exploited or waiting to be ex ploited. And for developers\, it is a heap of dozens of disti nct technologies\, often approximative\, incompatible\, which n eed to be configured individually\, connected manually\, often blindly and without clear semantics. In such conditions\, no thing can be checked or verified. In this talk\, we present O PA\, a new approach for web programming\, based on semantics a nd type systems. OPA is a programming language\, grounded in lambda-calculus and pi-calculus\, designed for the web\, for d atabases\, for concurrency and for distribution. One unique l anguage for the whole application\, with formal semantics\, si mple primitives\, a clear syntax\, and safety and security gua rantees. Oh\, and a few proofs in Coq. DTSTART;TZID=Europe/Paris:20100914T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201009141100 UID:semLSV.201009141100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Dominique Unruh - Composable symbolic secur ity definitions ATTENDEE;CN=Dominique Unruh: MAILTO:no@spam.com DESCRIPTION: The definition of Universal Composability (UC; Canetti\, FOCS 2001) is a cryptographic security definition that is both s imple and gives very strong security guarantees. In particul ar\, it ensures that the composition of secure protocols stay s 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 that p reserves security and is composable. We show how UC can be a pplied in a symbolic security setting. We also show a new de sign technique (virtual primitives). This design technique a llows to circumvent\, in a symbolic UC setting\, various impos sibility results that apply in the cryptographic setting. DTSTART;TZID=Europe/Paris:20100629T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201006291100 UID:semLSV.201006291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Gennaro Parlato - The Tree-Width of the Aux iliary Storage 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 general ization 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 provide d by the auxiliary storage. Our results outline a uniform m echanism to derive emptiness algorithms for automata\, explai ning and simplifying several existing results\, as well as pr oving new decidability theorems. DTSTART;TZID=Europe/Paris:20100601T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201006011100 UID:semLSV.201006011100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Andrey Rybalchenko - Constrained Environmen t Assumptions for Multi-Threaded Programs 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 scalab le reasoning. Once identified\, these assumptions can be used for reasoning with one program thread at a time\, which is p ossible by using the respective environment assumption to mo del the interleaving with other threads. Finding adequate as sumptions that are sufficiently precise to yield conclusive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major cha llenge. In this talk I will present a constraint-based techn ique for the inference of such assumptions. Our technique au tomatically steers towards an optimal precision/efficiency t rade-off between the extremes of efficient\, but incomplete t hread-modular reasoning and complete\, but prohibitively expe nsive consideration of all interleavings. For this task\, we pinpoint a declarative formulation of modular verification t hat allows one to express requisite environment assumptions using constraints and admits algorithmic solutions based on abstract fixpoint checking. I will describe an application o f our environment assumption inference for the verification of reachability and termination properties of multi-threaded programs. Joint work with Ashutosh Gupta and Corneliu Pope ea DTSTART;TZID=Europe/Paris:20100330T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201003301100 UID:semLSV.201003301100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Mike Just - What's in a Name? Evaluating (a nd Possibly Improving) the Security and Usability of Persona l Knowledge Questions 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 attentio n from the academic community. In this talk\, I will present several methods and results regarding the security and usabi lity of these authentication questions. Evaluating security has\, on one hand\, involved adapting techniques from guessing theory and applying them to real-world statistical distribu tions for typical answer categories such as the names of peo ple\, pets and places. It can also involve staging experiment s where friends or family members are encouraged to guess an swers. Experiments can also be used to evaluate the usabili ty (e.g.\, memorability) of challenge questions and their ans wers. And while the results of existing personal knowledge question systems have been mostly negative\, some possible im provements might be gained through increased interaction wit h the user\, for example\, to shape the answer distribution an d lower the prevalence of common answers\, or to introduce mo re tolerant authentication so as to reduce the reliance on p erfect response accuracy. DTSTART;TZID=Europe/Paris:20100608T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201006081100 UID:semLSV.201006081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre McKenzie - Programmes de branchement pour l'évaluation d'arbres ATTENDEE;CN=Pierre McKenzie: MAILTO:no@spam.com DESCRIPTION: Après un retour sur le "pebbling"\, sur le modèle du programm e de branchement et sur sa relation avec la machine de Turin g\, je présenterai des bornes inférieures sur la taille de pr ogrammes de branchement résolvant le problème de l'évaluatio n d'un arbre (je préciserai ce problème\, qui rappelle la faç on dont un "treillis automaton" effectue son calcul). Travau x effectués avec Mark Braverman\, Steve Cook\, Rahul Santhanam et Dustin Wehr\, présentés à MFCS 2009 et FSTTCS 2009. DTSTART;TZID=Europe/Paris:20100427T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201004271100 UID:semLSV.201004271100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Rolf Hennicker - On Weak Modal Compatibilit y and Refinement of Modal I/O Transition Systems 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 compatibil ity notion\, called weak modal compatibility\, for interacting components. As an important property of behavioural interfa ce theories we prove that weak modal compatibility is preser ved under weak modal refinement. Then we extend the notion o f weak modal compatibility to loosely coupled systems which interact via buffered FIFO channels. We show that also in th is case weak compatibility is preserved by weak modal refine ment and that\, moreover\, local refinements compose to global refinements. Finally\, we describe the MIO Workbench\, an Ecl ipse-based editor and verification tool for modal I/O automa ta. DTSTART;TZID=Europe/Paris:20100511T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201005111100 UID:semLSV.201005111100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Philippe Darondeau - On cycles and separabi lity of persistent Petri nets ATTENDEE;CN=Philippe Darondeau: MAILTO:no@spam.com DESCRIPTION: We show that PBRP nets (plain\, bounded\, reversible and persi stent Petri nets) have bases of cycles made of transition di sjoint cycles. We show that PBRP nets are strongly separable \, meaning that a PBRP net whose initial marking is of the fo rm k.M may be simulated by k replicas of this net\, each with initial marking M. We show that if a net with initial marki ng 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/anciens?se m=201005251100 UID:semLSV.201005251100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Thomas Wahl - From Counter Abstraction to T hread-State Cutoffs: New Techniques for Multi-Threaded Progr am Verification 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 pa rameterized finite-state programs\, such as non-recursive mul ti-threaded Boolean programs\, a principal ingredient in pred icate abstraction. I begin with a scalable method for analyz ing the reachability of program locations in programs execut ed by a bounded number of threads. This method\, being based on counter abstraction\, extends in principle to unbounded th read counts\, but suffers in practice from the high complexit y of coverability and reachability analyses for certain type s of counter machines. A different approach to program locat ion reachability rests on the assumption that in practical p arametric program settings\, a small "cutoff" number of threa ds suffice to generate all reachable program locations. Whil e this assumption is widely considered to be safe\, its pract ical usefulness hinges on how accurately we are able to esti mate the cutoff of a given program. I present a new method t hat analyses the reachable state space of a replicated finit e-state program for increasing thread counts\, until a condit ion emerges that allows us to conclude that the cutoff threa d count has been reached. Completeness of this method is ach ieved by resorting to traditional coverability analyses in c orner cases. The result is a precise and efficient program l ocation reachability method for replicated finite-state prog rams run by arbitrarily many threads. DTSTART;TZID=Europe/Paris:20100420T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201004201100 UID:semLSV.201004201100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Fernando Rosa Velardo - (Un)decidability in Petri nets with name creation and replication 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 of the class of Well Structured Transition Systems\, is a chall enging research problem. In this talk I will present two ort hogonal extensions of Petri nets\, with the capability of cre ating and managing pure names\, and with a replication primit ive\, getting ν-Petri nets and g-RN systems\, respectively. First\, I will show how these two extensions are strongly eq uivalent\, but only when a garbage collection mechanism is ad ded for idle threads. However\, when both extensions are cons idered simultaneously\, we obtain a Turing complete model\, th at we call ν-RN systems. Then I will survey the known exp ressivity results for ν-Petri nets (and therefore\, for g- RN systems). In particular\, coverability\, boundedness and te rmination are decidable\, while reachability and place-bounde dness are undecidable\, so that ν-Petri nets are strictly in between Petri nets and Turing machines. Then I will show how can we restrict ν-Petri nets (and\, therefore\, g-RN s ystems) and ν-RN systems in order to keep decidability of reachability and coverability\, respectively. In particular\, if we forbid synchronizations between the different compone nts in a g-RN system\, then reachability is still decidable. Analogously\, if we forbid name communication between the dif ferent components in a ν-RN system\, or restrict communica tion to happen only for a given finite set of names\, we obta in decidability of coverability. Finally\, I will comment on some ongoing work. This is joint work with David de Frutos-E scrig. http://kimba.mat.ucm.es/~frosa/publicaciones#fi08 DTSTART;TZID=Europe/Paris:20100209T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201002091100 UID:semLSV.201002091100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Olivier Pereira - Electing a University Pre sident using Open-Audit Voting ATTENDEE;CN=Olivier Pereira: MAILTO:no@spam.com DESCRIPTION: In March 2009\, the Université catholique de Louvain elected its President using a custom deployment of the Helios web-ba sed open-audit voting system. Out of 25\,000 potential voters \, 5000 registered\, and almost 4000 voted in each round of th e election. The precision of the voting system turned out to be crucial: in the first round\, the leader came short of wi nning the election by only 2 votes. We will describe the He lios-based voting system used in this election\, the specific s of the UCL deployment\, and the lessons learned in this dep loyment. 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 attack on th e auditing process\, we found that\, instead\, complaints are l ikely to be more easily handled in open-audit elections beca use 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/anciens?se m=201003091100 UID:semLSV.201003091100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Karthik Bhargavan - Modular Verification of Security Protocol Code by Typing 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/anciens?se m=201001261100 UID:semLSV.201001261100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : J Strother Moore - Machines Reasoning about Machines 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 mo dels to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbo lic means: theorems can be proved about them\, directly\, with mechanical theorem provers. But how practical is this visi on of machines reasoning about machines? In this highly per sonal talk\, I will describe the 40 year history of the Boyer -Moore Project and discuss progress toward making formal ver ification practical. Among other examples I will describe i mportant theorems about commercial microprocessor designs\, i ncluding parts of processors by AMD\, Motorola\, IBM\, Rockwell -Collins and others. Some of these microprocessor models ex ecute at 90% the speed of C models and have had important fu nctional properties verified. In addition\, I will describe a model of the Java Virtual Machine\, including class loading and bytecode verification and the proofs of theorems about JVM methods. Biography J Strother Moore holds the Admiral B .R. Inman Centennial Chair in Computing Theory at the Univer sity 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-auth or of the Boyer-Moore theorem prover and the Boyer-Moore fas t string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. Moore got his SB from MIT in 1970 and his PhD from the University of Edinburgh in 1973. Moore was a founder of Computational Logic\, Inc.\, an d served as its chief scientist for ten years. He served as chair of the UT Austin CS department for eight years. He a nd Bob Boyer were awarded the McCarthy Prize in 1983 and the Current Prize in Automatic Theorem Proving by the American Mathematical Society in 1991. In 1999\, they were awarded th e Herbrand Award for their work in automatic theorem proving . Boyer\, Moore\, and Kaufmann were awarded the 2005 ACM Soft ware Systems Award for the Boyer-Moore theorem prover. Moor e is a Fellow of both the American Association for Artificia l Intelligence and the ACM and is a member of the National A cademy of Engineering. DTSTART;TZID=Europe/Paris:20101026T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201010261100 UID:semLSV.201010261100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Mamadou Kanté - Vérification des propriétés logiques avec des étiquettes ATTENDEE;CN=Mamadou Kanté: MAILTO:no@spam.com DESCRIPTION: Un système d'étiquetage pour une propriété P dans une struct ure consiste à assigner à chaque élément du domaine une étiq uette\, aussi petite que possible\, de telle sorte que l'on pu isse vérifier la propriété en ne regardant que les étiquette s. Les systèmes d'étiquetage peuvent être vus comme un pré- traitement en vu de faire du model checking. En model-che cking les objets manipulés sont le plus souvent statiques. L orsque la structure est modifiée dans le temps\, on refait to us les calculs. Nous nous intéressons aux structures qui peu vent perdre des sommets/relations. Nous voulons pouvoir répo ndre\, de manière rapide à n'importe quel moment\, si le graph e résultant après suppression de sommets/arêtes vérifie une propriété P. Notre technique consiste à utiliser les systèm es d'étiquetage. Je montrerai comment vérifier des propriét és du premier ordre dans certaines classes de graphes en uti lisant des étiquettes de taille logarithmique (les étiquette s sont calculées une seule fois). Un ingrédient principal e st le résultat de Gaifman et une décomposition des formules locales de Frick. Ces résultats peuvent être étendus au com ptage. DTSTART;TZID=Europe/Paris:20100202T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201002021100 UID:semLSV.201002021100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Manuel Bodirsky - Computational Complexity of Constraint Satisfaction Problems 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 fir st give an overview over recent breakthrough results on cons traint satisfaction over finite domains based on this transl ation. Then I give an introduction on how to generalize thos e techniques from finite to infinite domain constraint satis faction\, and present applications in temporal reasoning. DTSTART;TZID=Europe/Paris:20100216T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=201002161100 UID:semLSV.201002161100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Michael Ummels - The Complexity of Nash Equ ilibria in Stochastic Games 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 equil ibrium of G where player 0 wins with probability 1. Moreover \, this problem remains undecidable if it is restricted to st rategies with (unbounded) finite memory. However\, if mixed s trategies are allowed\, decidability remains an open problem. One way to obtain a provably decidable variant of the probl em is restricting the strategies to be positional or station ary. For the complexity of these two problems\, we obtain a c ommon lower bound of NP and upper bounds of NP and PSPACE re spectively. DTSTART;TZID=Europe/Paris:20091208T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200912081100 UID:semLSV.200912081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Boris Köpf - Towards provable security agai nst side-channel attacks 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 cons umption. In distributed environments such as the Internet\, t iming attacks are the most daunting kind of side-channel att ack: Timing can be measured and exploited remotely\, opening the door for a potentially large number of attackers. Unfor tunately\, there have been no countermeasures against timing attacks that are practical and provably secure at the same t ime. In this talk\, I present work on novel methods for reaso ning about the security of countermeasures against side-chan nel attacks. The basis for this work is a model that enables one to express bounds for the amount of information that ca n be extracted from a system in a side-channel attack. I pre sent algorithms for computing such bounds\, and I report on e xperimental results where we apply these algorithms to analy ze concrete implementations of cryptographic algorithms. One finding is that the state-of-the-art countermeasure against timing attacks reduces the rate at which an implementation leaks information about the key\, but that the entire key inf ormation is still eventually revealed. Finally\, I present re cent work where we propose a novel countermeasure against ti ming attacks that is provably secure in our model. A case s tudy shows that this countermeasure is also practical in tha t it leads to implementations with minor performance overhea d. DTSTART;TZID=Europe/Paris:20091215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200912151100 UID:semLSV.200912151100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Joel Ouaknine - Time-Bounded Verification 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 len gth. DTSTART;TZID=Europe/Paris:20091027T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200910271100 UID:semLSV.200910271100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : James Worrell - Reachability in Parametric One-Counter Machines 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 result is to show NP-completeness of the problem of determin ing whether a given state is reachable from the initial stat e for some value of the parameters. Membership in NP is show n by reduction to the existential fragment of Presburger ari thmetic with divisibility. DTSTART;TZID=Europe/Paris:20091103T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200911031100 UID:semLSV.200911031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Julien Clément - Savez-vous compter ? ATTENDEE;CN=Julien Clément: MAILTO:no@spam.com DESCRIPTION: Les réseaux de capteurs mobiles font leur apparition en info rmatique depuis plusieurs années. Les applications de ces ré seaux sont nombreuses: environnementales\, militaires\, économ iques\, écologiques... Certaines caractéristiques de ces rése aux sont nouvelles et posent ainsi un défi pour les concepte urs d'algorithmes que nous sommes. Le modèle des protocoles de population [AAD+04] a été conçu pour représenter formell ement les réseaux de capteurs constitués d'agents mobiles do nt la mémoire est très limitée\, sans aucun contrôle sur leur propre mouvement. Nous étendrons ce modèle en un modèle plu s hétérogène dans lequel nous étudierons deux problèmes part iculiers. Dans cet exposé je présenterai en effet mes résul tats sur deux types d'algorithmes. Tout d'abord les 'algorit hmes de comptage'\, permettant de compter le nombre d'agents présents dans le système alors que des fautes peuvent surven ir. Puis\, nous étudierons un raffinement de ce modèle\, afin de prendre en compte la différence de vitesse entre les agen ts\, dans lequel nous présenterons des 'algorithmes de collec te'\, permettant de rassembler les données mesurées par les d ifférents agents du réseau. DTSTART;TZID=Europe/Paris:20091201T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200912011100 UID:semLSV.200912011100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Roland Meyer - Finite Representations for R econfigurable Systems 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 sy stems (RS). Despite an unbounded number of components and co nnections\, a large class of RS exhibits only finitely many c onnection patterns at runtime; a property called structural stationarity. We propose a translation of structurally stati onary systems into finite place/transition Petri nets\, which allows us to reuse existing Petri net verification tools fo r the verification of RS. To judge the expressiveness of the system class\, we prove that structural stationarity is equi valent to boundedness in the novel functions depth and bread th. The breadth of a RS corresponds to the connection degree of the components\, while the depth measures their interdepe ndence. Investigating these larger classes\, we find that sys tems of bounded depth are well-structured. Therefore\, proper ties can be decided on a finite prefix of the computation tr ee. For systems of bounded breadth\, we show Turing completen ess. To recover a Petri net translation for systems of bound ed depth\, we combine the newly developed structural semantic s with classical concurrency semantics. Although the resulti ng mixed translation generalises the previous approaches\, it does not cover the full class of depth bounded systems. An undecidability proof for reachability shows that a translati on into finite nets does not exist for the full class. DTSTART;TZID=Europe/Paris:20091124T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200911241100 UID:semLSV.200911241100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Volker Diekert - Fragments of first-order l ogic over infinite words 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\, FO2 \, the intersection of FO2 and Sigma2\, and Delta2 (and by dua lity Pi2 and the intersection of FO2 and Pi2). These descrip tions extend the respective results for finite words. In par ticular\, we relate the above fragments to language classes o f certain (unambiguous) polynomials. The talk is interplay o f algebraic\, topological\, and language theoretic properties. DTSTART;TZID=Europe/Paris:20090929T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200909291100 UID:semLSV.200909291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Giorgio Delzanno - Approximate Verification of Parameterized Systems 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 o f a possibly infinite-state space and exploit the theory of well-quasi orderings for ensuring the theoretical terminatio n of the analysis. The presentation is based on joint work w ith Parosh Abdulla and Ahmed Rezine. DTSTART;TZID=Europe/Paris:20090922T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200909221100 UID:semLSV.200909221100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : David Baelde - Regular fixed points\, non-de terministic cyclic proofs and finite automata 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 proo fs in particular. DTSTART;TZID=Europe/Paris:20090715T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200907151100 UID:semLSV.200907151100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Balder ten Cate - XPath: expressive power a nd static analysis 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 tree s. In this talk\, I will discuss two aspects of XPath 1.0 and 2.0 (as well as of some other variants of XPath proposed in the literature): Expressivity and succinctness: Which path s through XML documents can be described in XPath\, and how s uccinctly? One way to answer this is by comparing XPath to m ore well established and understood languages such as first- order logic. Static analysis: What is the complexity of test ing whether two XPath expressions are equivalent (always giv e the same answer)? Can we find a complete set of equivalenc e-preserving rewrite rules (i.e.\, so that every two equivale nt expressions can be rewritten to each other using these ru les)? Based on joint works with Maarten Marx\, with Carsten Lutz\, and with Luc Segoufin. DTSTART;TZID=Europe/Paris:20090707T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200907071100 UID:semLSV.200907071100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Ralf Küsters - Using ProVerif to Analyze Pr otocols with XOR and Diffie-Hellman Exponentiation 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 proper ties 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 rela ted tools\, to analyze a large class of protocols that employ the XOR operator and Diffie-Hellman exponentiation. The co re of our approach is to reduce the derivation problem for H orn theories modulo algebraic properties of XOR/Diffie-Hellm an exponentiation to a purely syntactical derivation problem for Horn theories. The latter problem can then be solved by tools such as ProVerif. Our reduction works for a large cl ass of Horn theories\, allowing to model a wide range of intr uder capabilities and protocols. We implemented our reducti on and\, in combination with ProVerif\, applied it in the auto matic analysis of several state-of-the-art protocols that us e XOR or Diffie-Hellman exponentiation. This talk is based on joint work with Tomasz Truderung\, published at CCS 2008 a nd CSF 2009. DTSTART;TZID=Europe/Paris:20090629T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200906291100 UID:semLSV.200906291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Madhavan Mukund - Specifying Interacting Co mponents with Coordinated Concurrent Scenarios 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 inter action. We introduce a mechanism to overlap phases that al lows complex interactions to be specified without obscurin g the logical structure of the constituent scenarios. Our notation combines the global view available in models such as high-level message sequence charts (HMSCs) with the loc al\, asynchronous structure captured by message-passing aut omata (MPA). In fact\, both HMSCs and MPAs can be captured as special cases of our formalism. In this talk we focus on the syntax and formal semantics of our notation\, with e xamples that illustrate why this approach is more natural fo r capturing real-life specifications. We also describe an approach to use automated tools to analyze systems specifi ed using our notation. This is joint work with Prakash Ch andrasekaran. DTSTART;TZID=Europe/Paris:20090609T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200906091100 UID:semLSV.200906091100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Arnaud Sangnier - Weak Time Petri Nets Stri ke Back! 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 are urgent\, and the weak one\, for which time can elapse arbitra rily. It is well known that many verification problems such as the marking reachability are undecidable with the strong semantics. In this talk\, we focus on Time Petri Nets with we ak semantics equipped with three different memory policies f or the firing of transitions. We prove that the reachability problem is decidable for the most common memory policy (int ermediate) and becomes undecidable otherwise. Moreover\, we s tudy the relative expressiveness of these memory policies an d obtain partial and surprising results. This a joint work 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/anciens?se m=200905191100 UID:semLSV.200905191100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pedro Adão - High-Level Programming for E-C ash 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\, f or instance\, that users can spend coins anonymously\, that us ers cannot forge coins\, and that a user should not spend the same coin twice without being eventually caught. These prot ocols involve sophisticated cryptographic constructions such as blind signatures and commitment and proving their correc tness is a non-trivial task\, hence reasoning about e-cash ap plications becomes an almost impossible task. Relying on re cent work on optimistic value commitment [FGZN08]\, we propos e a calculus to reason about e-cash applications. Our calcu lus has a simple\, symbolic semantics; it can be used for pro gramming with e-cash and for reasoning on its properties\, wh ile shielding the programmer from its cryptographic implemen tation. We consider two variants of the symbolic semantics. An abstract semantics rules out any double spending (by des ign) while a more realistic\, intermediate semantics accounts for the possibility of double spending\, with reliable detec tion. We first relate these two semantics\, and then relate t he intermediate semantics to the computational properties of the underlying e-cash protocol. We show that our calculus i s a sound abstraction of the low-level e-cash protocols\, tha t is\, all low-level behaviours can be mapped to an high-leve l equivalent trace. DTSTART;TZID=Europe/Paris:20090512T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200905121100 UID:semLSV.200905121100 LOCATION:Salle Condorcet (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Eugen Zalinescu - Automated Computational V erification for Cryptographic Protocol Implementations 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 compu tational cryptography. Thus\, we obtain a first tool chain th at yields security guarantees for computational models tight ly related to executable code. We show the soundness of the underlying translation for authentication and secrecy. To th is end\, we equip ML programs with a probabilistic semantics\, and relate it to the probabilistic polynomial-time semantic s of CryptoVerif. We also review experimental (symbolic and computational) results recently obtained for a reference imp lementation of the TLS protocol. (This is joint work with K arthik Bhargavan\, Ricardo Corin\, and Cédric Fournet.) DTSTART;TZID=Europe/Paris:20090428T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200904281100 UID:semLSV.200904281100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Delphine Longuet - Test à partir de spécifi cations logiques ATTENDEE;CN=Delphine Longuet: MAILTO:no@spam.com DESCRIPTION: Le test est l'une des méthodes les plus utilisées pour la va lidation des syst-bèmes informatiques. Lorsque l'implantati on du système -Aà tester n'est pas connue\, les tests sont s électionnés et construits à partir d'une spécification (form elle) du syst-bème. Il existe principalement deux approches du test -Aà partir de spécifications formelles : les spéci fications logiques sont utilisées pour tester le comportemen t fonctionnel des syst-bèmes (les donn-Aées)\, tandis que l es syst-bèmes de transitions sont utilis-Aés pour tester l e comportement dynamique et réactifs des syst-bèmes (action s et communications).-A Une théorie du test à partir de sp écifications logiques a été définie dans les années 90\, form alisant le cadre de test ainsi que les différentes phases du processus de test. Ces travaux proposent en particulier une méthode de sélection de tests appelée dépliage pour des spé cifications de forme restreinte dont les axiomes sont des éq uations conditionnelles. L'idée de cette méthode est d'utili ser des techniques de preuve afin de guider la sélection de tests. Le but est d'obtenir une couverture pertinente des co mportements du syst-bème.-A Je présenterai tout d'abord c ette formalisation du test\, en particulier le probl-bème de l'existence d'un jeu de tests exhaustif\, puis la m-Aéthode de sélection de tests par dépliage. Je présenterai ensuite deux aspects de mes travaux : - la généralisation de ce cadr e de test aux spécifications du premier ordre\, et en particu lier les résultats d'exhaustivité et de complétude de la sél ection par dépliage étendue à ces spécifications - l'adaptat ion de ce cadre\, ainsi que les résultats d'exhaustivité et l 'adaptation du dépliage\, à des spécifications modales du pre mier ordre\, dans le but de proposer une nouvelle approche 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/anciens?se m=200904271100 UID:semLSV.200904271100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Hugo Gimbert - Qualitative Determinacy and Decidability of Stochastic Games with Partial Observation ATTENDEE;CN=Hugo Gimbert: MAILTO:no@spam.com DESCRIPTION: (Joint work with Nathalie Bertrand and Blaise Genest.) We c onsider the standard model of finite two-person zero-sum sto chastic games with signals. We are interested in the existen ce of almost-surely winning or positively winning strategies \, under reachability\, safety\, Büchi or co-Büchi winning obje ctives. We prove two qualitative determinacy results. Firs t\, in a reachability game either player 1 can achieve almost surely the reachability objective\, or player 2 can ensure a lmost surely the complimentary safety objective\, or both pla yers have positively winning strategies. Second\, in a Büchi game if player 1 cannot achieve almost surely the Büchi obj ective\, then player 2 can ensure positively the complimentar y co-Büchi objective. We prove that players only need strate gies with finite-memory\, whose sizes range from no memory at all to doubly-exponential size\, with matching lower bounds. We provide fix-point algorithms to decide which player has an almost surely winning or positive winning strategy and c ompute the finite memory strategy. Complexity ranges from EX PTIME to 2EXPTIME with matching lower bounds\, and better com plexity can be achieved for some special cases where 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/anciens?se m=200904211100 UID:semLSV.200904211100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Damien Pous - Kleene et Kozen en Coq ATTENDEE;CN=Damien Pous: MAILTO:no@spam.com DESCRIPTION: Formaliser des choses dans un assistant de preuve s'av-bère souvent-A pénible\, de nombreuses étapes de raisonnement de vant -bêtre explicit-Aées alors qu'elles sont d'habitude l aissées au relecteur scrupuleux. Ceci est en particulier vr ai lorsque l'on doit travailler sur des relations binaires ( réécriture\, réductions\, équivalences\, etc...)\, tr-bès-A in tuitives\, mais pas compl-bètement triviales.-A Lorsque c' est possible\, une premi-bère astuce consiste -Aà considére r les relations de fa-bçon alg-Aébrique : en montant le ni veau d'abstraction\, on facilite la formalisation de certaine s preuves. Une fois ce pas franchi\, on réalise que les relat ions binaires sont un mod-bèle des-A alg-bèbres de Kleene \, d-Aécidables par la théorie des automates finis. Nous ex poserons 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 de-A Kleene\, par réflection. Plus généralement\, nous exposerons les outils que nous développo ns 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/anciens?se m=200904141100 UID:semLSV.200904141100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Anuj Dawar - Logics with Rank Operators 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 lo gic with counting (FPC) is not sufficient and there have bee n several proposals for more expressive logics. Taking our inspiration from recent results that show that natural linea r-algebraic operations are not definable in FPC\, we propose FPR - an extension of fixed-point logic with an operator for matrix rank. We show that this is strictly more expressive than FPC and can express the polynomial-time problems that have been shown to be inexpressible in FPC. We also show th at FO+R\, the extension of first-order logic with rank operat ors is surprisingle expressive. It can express some forms o f transitive closure and\, on ordered structures\, captures th e complexity classes ModpL. In this talk\, I will give the h istory and general background to the question (assuming litt le or no previous knowledge of descriptive complexity and fi xed-point logics) and explain the context of the new results . I will also point to several interesting open problems. (Joint work with Martin Grohe\, Bjarki Holm and Bastian Laubn er). DTSTART;TZID=Europe/Paris:20090407T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200904071100 UID:semLSV.200904071100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Florian Horn - Games of ordinal Length 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 lengt h. In addition to the usual ''successor transitions''\, our a renas feature ''limit transitions'' which describe what happ ens after partial plays whose length is a limit ordinal. The play only stops when it reaches a final state\, which can be winning for either of the players. We describe two solutio ns for such games. The first one uses a reduction to infinit e Muller games\, and shows that the problem of the winner is PSPACE-complete. The second one uses a special case of ordin al games with ''priority'' transitions\, where the players ha ve positional strategies. A LAR-like construction allows us to derive the existence of finite-memory strategies in the g eneral case. DTSTART;TZID=Europe/Paris:20090406T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200904061100 UID:semLSV.200904061100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Cas Cremers - Cryptographic protocols as Bu ilding Blocks: From the Man-in-the-Middle attack to C ompositional Symbolic Analysis. ATTENDEE;CN=Cas Cremers: MAILTO:no@spam.com DESCRIPTION: Despite using very coarse abstractions\, and making strong as sumptions on the environment\, the symbolic analysis of crypt ographic protocols has proven very successful. By now\, many dimensions of the symbolic (Dolev-Yao) model have been explo red to some extent\, including compositionality properties of protocols and the relation between symbolic correctness pro ofs and computational proofs. One might expect that formal approaches are ideally suited for building larger communicat ion infrastructures\, because of their high level of abstract ion. However\, in practice\, symbolic methods are only used fo r analysis of existing protocols\, whereas protocol construct ion is performed at the detailed level of cryptographic prot ocols. In this talk we cover some of the requirements for u sing cryptographic protocols as components in symbolic\, Dole v-Yao like\, analyses. In particular\, we discuss various comp ositionality results\, and their relation to using cryptograp hic protocols as building blocks. Finally\, we revisit the cr yptographic requirements on real-world protocols and show ho w they influence the compositionality problem\, and conclude with a number of open problems. DTSTART;TZID=Europe/Paris:20090331T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200903311100 UID:semLSV.200903311100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre Ganty - What's decidable for Asynchr onous Programs? 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 sc heduler. By providing a low-overhead way to manage concurren t interactions\, asynchronous programs form the core of many server programs\, embedded systems\, and popular programming s tyles for the web (Ajax). Unfortunately\, such programs can b e hard to write and maintain as sequential control flow need s to be split into several disjoint handlers. They are a cha llenge for static analysis tools as they are infinite state: both the program stack and the number of outstanding asynch ronous requests may be unbounded. We show that safety and li veness properties can be checked effectively for the class o f Boolean asynchronous programs\, thus enabling automatic sta tic 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/anciens?se m=200903301100 UID:semLSV.200903301100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Geoff Sutcliffe - TPTP\, TSTP\, CASC\, etc. - Automated Reasoning in Practice 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 Solu tions from Theorem Provers (TSTP) solution library\, the TPTP language\, the CADE ATP System Competition (CASC)\, tools suc h as my semantic Derivation Verifier (GDV) and the Interacti ve Derivation Viewer (IDV)\, meta-ATP systems such as the Sma rt Selective Competition Parallelism (SSCPA) system and the Semantic Relevance Axiom Selection System (SRASS)\, online ac cess to automated reasoning systems and tools through the Sy stemOnTPTP web service\, and applications in various domains. Current work extending the TPTP to higher-order logic will be introduced. DTSTART;TZID=Europe/Paris:20090317T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200903171100 UID:semLSV.200903171100 LOCATION:Salle Renaudeau (Bâtiment Laplace) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Tayssir Touili - On the Reachability Analys is of Acyclic Networks of Pushdown Systems 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 shared memory or on message passing through unbounded lossy channels. We prove mainly that the reachability problem betw een 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 pushdown networks\, the channel language is effectively recognizable. This fact holds although the set of reachable configuration s (including stack contents) for a network of depth (at leas t) 2 is not rational in general (i.e.\, not definable by a mu lti-tape finite automaton). Moreover\, we prove that for a ne twork of depth 1\, the reachability set is rational and effec tively constructible (under an additional condition on the t opology for lossy channel networks). This is a joint work wi th Mohamed Faouzi Atig and Ahmed Bouajjani. DTSTART;TZID=Europe/Paris:20090310T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200903101100 UID:semLSV.200903101100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Stefan Schwoon - Context-bounded analysis o f multithreaded Java programs 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 wh ich the active thread changes at most k times\, where k is fi xed. However\, until recently\, context-bounded reachability h as been only a theoretical possibility\, primarily because of its prohibitive worst-case runtime. In the talk\, which pres ents joint work with Dejvuth Suwimonteerabuth and Javier Esp arza\, I will talk about an improvement that alleviates this problem. The approach has been implemented in the tool jMope d. DTSTART;TZID=Europe/Paris:20090304T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200903041100 UID:semLSV.200903041100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Ingmar Meinecke - A weighted mu-calculus on words 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 complete ness and continuity properties. For important semirings like distributive complete lattices\, the tropical and the probab ilistic semiring\, we show that the formulas of the conjuncti on-free weighted mu-calculus define exactly the class of ome ga-rational formal power series. DTSTART;TZID=Europe/Paris:20090303T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200903031100 UID:semLSV.200903031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Axel Legay - On Simulation-Based Probabilis tic Model Checking of Mixed-Analog Circuits ATTENDEE;CN=Axel Legay: MAILTO:no@spam.com DESCRIPTION: In this talk\, we consider verifying properties of mixed-sign al circuits\, i.e.\, circuits for which there is an interactio n between analog (continuous) and digital (discrete) values. We use a simulation-based approach that consists of evaluat ing the property on a representative subset of behaviors\, ge nerated by simulation\, and answering the question of whether the circuit satisfies the property with a probability great er than or equal to some value. We propose a logic adapted t o the specification of properties of mixed-signal circuits\, in the temporal domain as well as in the frequency domain. W e also demonstrate the applicability of the method on differ ent models of Δ-Σ modulators for which previous formal verification attempts were too conservative and requi red excessive computation time. With Alexandre Donzé and Edm und Clarke. DTSTART;TZID=Europe/Paris:20090224T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200902241100 UID:semLSV.200902241100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Ewen Maclean - Verifying Functional Propert ies of Pointer Programs 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 th e shape of inductive structures on the heap\, such as linked lists. I discuss an extension to this work which concerns t he automatic verification of functional properties of pointe r programs. I will discuss the challenging parts of such ver ifications which require creative input. The talk will be mo tivated by examples and possibly a working demo of some of t he early results. DTSTART;TZID=Europe/Paris:20090217T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200902171100 UID:semLSV.200902171100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Christophe Morvan - Regular graphs: a perfe ct model for infinite state systems? 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\, Petr i nets\, or process algebras are only major examples of such systems. Most of these systems do not provide the simplicit y and efficiency of finite state systems. Finite graphs\, or finite state automata\, are the corner stone of computer scie nce\, it is still a very active field of research with countl ess applications. Infinite state systems lack that kind of u niversal and simple framework. Graph grammars were initiall y used to produce infinite sets of graphs. But in the early 90's\, Courcelle used deterministic graph grammars to charact erise a general class of infinite graphs: regular graphs. Re cently Caucal built up a nice toolbox for studying regular g raphs\, and with Hassen they provided an elegant extension of visibly pushdown automata\, which captures every determinist ic context-free language. In this talk we will present a su rvey on regular graphs\, including a discussion on the extens ions of visibly pushdown automata. We will present\, as well\, an ongoing work with Nathalie Bertrand aiming at generalisi ng probabilistic pushdown automata to this graph grammar set ting. DTSTART;TZID=Europe/Paris:20090210T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200902101100 UID:semLSV.200902101100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Joost-Pieter Katoen - Parameter Synthesis f or Probabilistic Timed Reachability ATTENDEE;CN=Joost-Pieter Katoen: MAILTO:no@spam.com DESCRIPTION: In this talk\, we propose a technique to synthesize parametri c rate values in continuous-time Markov chains that ensure t he validity of time-bounded reachability properties. Rate ex pressions over variables indicate the average speed of state 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 s ystem guarantees the validity of bounded reachability proper ties. This algorithm is based on discretizing parameter rang es together with a refinement technique. We will describe th e algorithm\, analyze its time complexity\, and show its appli cability by deriving parameter constraints for a real-time s torage system with probabilistic error checking facilities. (This is joint work with Tingting Han and Alexandre Mereacr e.) DTSTART;TZID=Europe/Paris:20090113T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200901131100 UID:semLSV.200901131100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Laure Gonnord - Analyses de propriétés quan titatives de programmes ATTENDEE;CN=Laure Gonnord: MAILTO:no@spam.com DESCRIPTION: Dans cet exposé je présenterai mes travaux doctoraux et post doctoraux qui se placent tous les deux dans le contexte d'an alyse 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éaires\, qui p ermet de découvrir automatiquement\, en chaque point de contr ôle d'un programme\, des syst-bèmes de contraintes lin-Aéai res invariantes sur les variables numériques. Les résultats de l'analyse sont utilisables en compilation\, en vérificati on de programmes et en parallélisation. Apr-bès une introdu ction rapide -Aà cette méthode\, je montrerai plus spécifiqu ement comment la précision des analyses peut -bêtre am-Aél iorée grâce à la notion d'accélération abstraite. Mes trav aux postdoctoraux ont étudié d'autres types d'applications e mbarquées que sont les applications multimédia. Ces applicat ions ne sont plus critiques\, mais par contre on désire évalu er et garantir des propriétés extra fonctionnelles\, comme la qualité de service. En effet\, la resource allouée à un comp osant logiciel peut évoluer\, et on aimerait garantir une cer taine fluidité de l'application. Je présenterai mes travaux de formalisation des contraintes de ressources au sein d'une architecture logicielle à composants\, Qinna\, ainsi que les mécanismes de maintenance de ces contraintes. DTSTART;TZID=Europe/Paris:20090106T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200901061100 UID:semLSV.200901061100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Lucas Dixon - The State of Inductive Theore m Proving for Software Verification 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 r esearch; indeed\, a significant strand of research considers heuristic approaches to inductive theorem proving\, driven by syntactic observations. Recently\, a type-theory based form of synthesis\, combined with an upside-down twist on rewritin g\, has led to some exciting results. In this talk I will out line the state the field\, give my view of the key intuitions for the emerging proof strategies\, and highlight the exciti ng challenges currently being considered. DTSTART;TZID=Europe/Paris:20081216T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200812161100 UID:semLSV.200812161100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Laurent Doyen - Quantitative Languages: Dec ision Problems\, Expressive Power\, and Closure Properties ATTENDEE;CN=Laurent Doyen: MAILTO:no@spam.com DESCRIPTION: Quantitative generalizations of classical languages\, which a ssign to each word a real number instead of a boolean value\, have applications in modeling resource-constrained computat ion. We use weighted automata (finite automata with transiti on weights) to define several natural classes of quantitativ e languages over finite and infinite words; in particular\, t he real value of an infinite run is computed as the maximum\, limsup\, liminf\, limit average\, or discounted sum of the tra nsition weights. We define the classical decision problems of automata theory (emptiness\, universality\, language inclus ion\, and language equivalence) in the quantitative setting a nd study their computational complexity. As the decidability of language inclusion remains open for some classes of weig hted automata\, we introduce a notion of quantitative simulat ion that is decidable and implies language inclusion. We al so give a complete characterization of the expressive power of the various classes of weighted automata. In particular\, we show that most classes of weighted automata cannot be det erminized. Finally\, for quantitative languages L\, L'\, we st udy the operations max(L\,L')\, min(L\,L')\, and 1-L as natural generalizations of the boolean operations; we also consider the sum L + L'. We establish the closure properties of all c lasses of quantitative languages with respect to these four operations. This talk is based on joint work with Krishnend u Chatterjee and Tom Henzinger. DTSTART;TZID=Europe/Paris:20081215T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200812151100 UID:semLSV.200812151100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Jérôme Leroux - An Easy Algorithm For The G eneral Vector Addition System Reachability Problem 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 confi guration is not reachable from an initial one\, there exists a pair of Presburger formulas denoting an inductive separato r proving this property. Since we can decide with any decisi on procedure for the Presburger arithmetic if pairs of Presb urger formulas denote inductive separators\, we deduce that t here exist checkable certificates of non-reachability. In pa rticular\, there exists an easy algorithm for deciding the ge neral VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by fairly enumerating finite sequence of actions and a second one that tries to prove the non-reachability by fairly enumerating p airs of Presburger formulas. Even if the KLMST decomposition 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/anciens?se m=200812091100 UID:semLSV.200812091100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre Genevès - XML Reasoning: From Theory to Practice 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 will present a fixpoint modal logic designed for reasoning on fi nite trees\, along with a satisfiability-testing algorithm th at performs well in practice. The fully implemented system a llows to effectively solve a whole class of problems involvi ng XPath queries\, regular tree types and any boolean combina tion of them (like query containment\, and query satisfiabili ty in the presence of schemas). DTSTART;TZID=Europe/Paris:20081125T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200811251100 UID:semLSV.200811251100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Moshe Vardi - From Philosophical to Industr ial Logics 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 effective 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/anciens?se m=200811061100 UID:semLSV.200811061100 LOCATION:Amphithéâtre Marie Curie (bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Stéphane Gaubert - Questions de théorie des jeux et de convexité abstraite en analyse statique de progr amme ATTENDEE;CN=Stéphane Gaubert: MAILTO:no@spam.com DESCRIPTION: Le but de cet exposé est de donner quelques exemples d'appli cation de techniques d'optimisation et de théorie des jeux e n analyse statique de programme par interprétation abstraite . On présentera tout d'abord une correspondance entre les p roblèmes de point fixe rencontrés en interprétation abstrait e et ceux que l'on rencontre en théorie des jeux à somme nul le. Cette correspondance permet d'adapter des algorithmes in spirés de la théorie des jeux ou du contrôle tels que l'itér ation sur les politiques\, mais le caractère "expansif&q uot; des opérateurs de point fixe\, qui se traduit par la pré sence d'un taux d'actualisation négatif\, pose des difficulté s algorithmiques inédites. On discutera notamment le problèm e du calcul du point fixe minimal (ou de la vérification de la minimalité d'un point fixe) à l'aide de techniques de thé orie de Perron-Frobenius non-linéaire. On montrera ensuite comment des idées empruntées à l'analyse convexe abstraite p ermettent de définir des classes de domaines généralisant le domaine des "templates" introduit par Manna et se s collaborateurs. On traitera spécialement du domaine des po lyèdres max-plus ou tropicaux. Ces résultats sont issus de travaux en collaboration avec A. Adje (LIX/MeASI)\, X. Allami geon (EADS)\, E. Goubault et S. Putot (CEA/MeASI). DTSTART;TZID=Europe/Paris:20081104T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200811041100 UID:semLSV.200811041100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Olivier Serre - Tree Pattern Rewriting Syst ems 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 im portance of web services. We define here Tree Pattern Rewrit ing Systems (TPRS) as an abstract model of dynamic XML-based documents. TPRS systems generate infinite transition syste ms\, where states are unranked and unordered trees (hence pos sibly modeling XML documents). The guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T\,R)\, a tree pattern P and some in teger k such that any reachable document from T has depth at most k\, it is decidable (albeit of non elementary complexit y) whether some tree satisfying P is reachable from T. This is joint work with B. Genest\, A. Muscholl\, and M. Zeitoun. DTSTART;TZID=Europe/Paris:20081028T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200810281100 UID:semLSV.200810281100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Pierre-Cyrille Héam - Génération Automatiqu e d'Approximations Régulières 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 syst-Aèmes d e réécritures simples. Une approche pour résoudre ce problèm e consiste alors à utiliser des approximations de R*(I). Nou s montrerons dans cet exposé comment une technique manuelle d'approximations introduite par Th. Genet en 98 peut -bêtre automatis-Aée\, notamment pour la vérification de protocole s cryptographiques. DTSTART;TZID=Europe/Paris:20081014T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200810141100 UID:semLSV.200810141100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Stefan Haar - Diagnostic et Test en ordres partiels 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 ne tworks. The methodology of asynchronous diagnosis is present ed\, followed by a discussion of fun but challenging problems connected to diagnosis\, in particular distribution of unfol ding. In a different domain\, the talk will present recent a nd ongoing work on testing of input/output automata over par tially ordered I/O streams. DTSTART;TZID=Europe/Paris:20080930T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200809301100 UID:semLSV.200809301100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Sylvain Schmitz - Génération d'une suite de tests de grammaticalité ATTENDEE;CN=Sylvain Schmitz: MAILTO:no@spam.com DESCRIPTION: L'exposé s'intéresse à des techniques de fouille d'erreurs dans une grammaire du fran-bçais d-Aéveloppée au LORIA. Ce tte 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 des phrases incorr ectes. Pour un ensemble de phrases de test\, la fouille d'err eurs cherche alors à identifier les causes les plus probable s de sur-génération pour assister le linguiste dans son trav ail de correction. Je présenterai en détail une méthode de g énération de telles phrases qui vise à explorer les coins et recoins de la grammaire et les interactions inattendues qu' elle permet. DTSTART;TZID=Europe/Paris:20080923T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200809231100 UID:semLSV.200809231100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Masahiko Sakai - Programming in Malbolge 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 diffic ulty comes from (a) its restrictive instructions\, (b) instru ction-replacement after execution and (c) restriction for lo adable data. In this talk\, we solve these problems and shows that general loop-programming is possible in this language. DTSTART;TZID=Europe/Paris:20080916T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200809161100 UID:semLSV.200809161100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Tomas Vojnar - Regular Model Checking using nondeterministic tree automata 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 dynamic\, pointer-linked data structures. ARTMC is based on representi ng infinite sets of configurations of the examined systems b y finite tree automata whose efficient manipulation is thus crucial for an overall efficiency of ARTMC. It turns out th at a significant bottleneck in dealing with finite tree auto mata is the need to determinise them when checking inclusion or within the classical automata minimisation procedure. In the talk\, we will present several recent works whose aim is to eliminate the need to determinise the automata being han dled in ARTMC. In particular\, we will present methods for an antichain-based inclusion checking on nondeterministic tree automata and efficient methods for reducing the size of suc h automata based on various types of upward\, downward\, and c omposed (bi)simulations. According to our experimental resul ts\, these techniques really very significantly improve the p erformance of ARTMC. The talk is based on joint work with A hmed Bouajjani and Tayssir Touili from LIAFA\, Peter Habermeh l 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/anciens?se m=200807081100 UID:semLSV.200807081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Valentin Goranko - Tableau-based decision p rocedure for the logic of strategic ability in multi-agent s ystems ATL ATTENDEE;CN=Valentin Goranko: MAILTO:no@spam.com DESCRIPTION: The Alternating-time Temporal Logic (ATL)\, introduced by Al ur\, Henzinger\, and Kupferman\, is a logic for reasoning about strategic abilities of agents and coalitions in multi-agent systems\, in which one can express statements\, such as: "The agent (or\, coalition of agents) A has a strategy such that\, if A follows that strategy then\, no matter what other agent s do\, the objective $\phi$ will be achieved"\, there the obje ctive is itself a formula of ATL prefixed by a temporal oper ator such as `nexttime'\, `until'\, or `always in the future'. Testing satisfiability in ATL has been proved decidable (E xpTime complete)\, by using alternating tree automata and by small model property\, but both methods have some practical d eficiencies and are not suitable for manual application. In this talk I will give a concise introduction to ATL and the n will present a recently developed decision procedure for t esting satisfiability in ATL based on sound\, complete\, and t erminating incremental tableaux. This decision procedure run s in the theoretically prescribed time complexity\, i.e.\, Exp Time\, but in most practical cases is much more efficient\, an d is suitable for both manual and computerized application. (Joint work with Dmitry Shkatov\, Univ. of the Witwatersrand ) DTSTART;TZID=Europe/Paris:20080701T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200807011100 UID:semLSV.200807011100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Christof Löding - Star-height of tree langu ages 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/anciens?se m=200806171100 UID:semLSV.200806171100 LOCATION:Amphi 109N (Bât. Léonard de Vinci) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Markus Müller-Olm - Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures 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 m odels\, the creator of processes running in parallel must wai t until all the created processes have terminated before it can resume its execution. However\, in presence of procedures or methods\, this does not allow one to model thread creatio n primitives as the found in languages like Java adequately. In this talk I am going to present recent work on fixpoi nt-based analysis of programs with thread creation and (recu rsive) procedures. Our algorithm solves gen/kill-problems pr ecisely 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-ba sed analysis of similar program models. The resulting algori thm\, however\, computes global information faster and more di rectly. This is joint work with Peter Lammich. DTSTART;TZID=Europe/Paris:20080603T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200806031100 UID:semLSV.200806031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Grégoire Sutre - Accelerated Data-flow Anal ysis 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\, s uccessful results were obtained in practice by different too ls implementing this framework. In this talk\, we show how to extend the acceleration framework to data-flow analysis. C ompared to a classical widening/narrowing-based abstract int erpretation\, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the wa y the abstract value is computed. We illustrate our approach on convex polyhedral data-flow analysis\, and we provide a c ubic-time acceleration-based algorithm for solving interval constraints with full multiplication. Joint work with Jérôm e Leroux. DTSTART;TZID=Europe/Paris:20080527T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200805271100 UID:semLSV.200805271100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Emmanuel Hainry - Systèmes dynamiques linéa ires : décidabilité de problèmes de sécurité ATTENDEE;CN=Emmanuel Hainry: MAILTO:no@spam.com DESCRIPTION: Les systèmes dynamiques décrivent un processus (trajectoire \, phénomène naturel\, calcul) par l'espace sur lequel il se produit\, sa dynamique et son point initial. Cette descripti on est suffisante pour définir toute l'évolution du système mais ne donne guère d'idée sur l'ensemble de la trajectoir e du système\, et il est crucial pour certains systèmes d'as surer des propriétés sur cette trajectoire (par exemple\, la comète repassera infiniment souvent par un point donné\, ou la Terre et la Lune ne se heurteront jamais ou encore la ma chine de Turing s'arr-bête).-A Nous définirons quelques problèmes importants sur les systèmes linéaires : atteignab ilité point à point\, atteignabilité d'un hyperplan\, omega-l imite. Nous montrerons que ces problèmes qui sont dans le c as général (et m-bême dans des cas simples) ind-Aécidables deviennent décidables si l'on considère des systèmes dynam iques linéaires. DTSTART;TZID=Europe/Paris:20080520T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200805201100 UID:semLSV.200805201100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Morgan Magnin - À la recherche de méthodes efficaces pour la vérification de réseaux de Petri à chronom ètres en temps discret ATTENDEE;CN=Morgan Magnin: MAILTO:no@spam.com DESCRIPTION: A mesure que les réseaux proliféraient et prenaient une pla ce temporelle et fonctionnelle des systèmes. Il convient ain si de développer des formalismes permettant d'écrire et de v alider les interactions entre les activités des processeurs et les réseaux de communication. Les réseaux de Petri tempor els (RdPT) sont un de ces formalismes. Ils permettent de mod éliser la durée de différentes actions sous la forme d'un in tervalle de temps. Ils peuvent par ailleurs -bêtre enrichis afin de repr-Aésenter des tâches susceptibles d'-bêtre su spendues puis relanc-Aées (réseaux de Petri à chronomètres notés SwPN). Le temps dense consiste à considérer le temps comme une grandeur dense tandis que le temps discret l'assim ile à une grandeur discrète. Les applications physiques évol uent par rapport au temps physique qui est continu ; toutefo is\, 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 part iculiers (échantillonnage ou observations sporadiques). De p lus\, le système de pilotage est composé de tâches qui sont e xécutées sur un (ou plusieurs) processeur(s) dont le temps p hysique est discret. Le recours à un temps dense lors de la modélisation conduit donc à une surapproximation du système informatique. Mais l'intér-bêt majeur du temps dense r-Aés ide dans les abstractions symboliques associées\, pratiques à mettre en oeuvre et contenant l'explosion combinatoire des états. Nous nous proposons de comparer les deux approches q ue sont le temps dense et le temps discret. Notre étude com mence par un approfondissement des liens entre réseaux de Pe tri\, RdPT et SwPN en fonction de leur sémantique en temps de nse et en temps discret. Nous en déduisons des résultats de décidabilité importants sur les modèles en temps discret\, no tamment la décidabilité de l'accessibilité d'état sur les Sw PN bornés. Nous proposons ensuite une méthode efficace de ca lcul énumératif de l'espace d'états de modèles en temps disc ret. Comme toute méthode purement énumérative\, celle-ci souf fre toutefois de l'explosion combinatoire du nombre d'états. C'est pourquoi nous concevons une méthode symbolique permet tant de calculer l'espace d'états d'un modèle en temps discr et en adaptant les techniques habituellement réservées au te mps dense. Cette procédure nous permet alors de vérifier de s propriétés exprimées dans la logique TCTL sur les SwPN en temps discret. Nous aboutissons à des résultats très encoura geants\, qui permettent d'analyser finement le comportement d e modèles à chronomètres. DTSTART;TZID=Europe/Paris:20080513T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200805131100 UID:semLSV.200805131100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Véronique Cortier - On the use of formal mo dels for proving cryptographic security notions ATTENDEE;CN=Véronique Cortier: MAILTO:no@spam.com DESCRIPTION: Since the 1980s\, two approaches have been developed for ana lyzing 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 se curity\, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are tr eated as black boxes. Since the seminal work of Dolev and Y ao\, it has been realized that this latter approach enables s ignificantly simpler and often automated proofs. However\, th e guarantees that it offers have been quite unclear. In thi s 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/anciens?se m=200805061100 UID:semLSV.200805061100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Deepak D'Souza - Conflict-Tolerant Real-Tim e Features 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 sy stem 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\, which guarantees the "maximal" use of each feature. We provide a formal framework for specifying such features\, and a compos itional technique for verifying systems developed in this fr amework. 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/anciens?se m=200804291100 UID:semLSV.200804291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Claire David - Data Tree Patterns 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 doc ument as a tree labelled by an infinite alphabet to represe nt data values. We consider Boolean combinations of data tre e patterns as a specification and query language for XML doc uments. Data tree patterns are tree patterns plus variable ( in)equalities which express joins between data values. We co nsider the decidability and complexity of two problems. The first one is the model checking problem. We show that it is DP-complete in general and already NP-complete when we consi der a single pattern. The second one is the satisfiability p roblem in the presence of a DTD. We show that it is in gener al undecidable and we identify several decidable fragments. DTSTART;TZID=Europe/Paris:20080408T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200804081100 UID:semLSV.200804081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Cristina Sirangelo - Data Exchange and Sche ma Mappings in Open and Closed Worlds 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 mappi ng). Two semantics of data exchange and schema mappings have been proposed in the literature: an open-world (OWA) seman tics \, which allows target instances to contain arbitrary ex tensions of the data translated from the source\, a closed- world (CWA) semantics\, which only allows to exchange "as muc h data as needed" to satisfy the constraints of the schema mapping. This work proposes a new mixed OWA/CWA semantics that generalizes and unifies the previous ones: it allows d ifferent target attributes to import data according to diffe rent semantics (either open-world or closed-world). This app roach allows more flexibility in the specification of schema mappings and collapses in the known OWA and CWA approaches when target attributes are either all open or all closed. Un der such mixed semantics\, we address two of the main issues in data exchange and schema management: query answering and composition of schema mappings. In particular we study how t heir complexities depend on the number of open attributes an d we identify new conditions under which schema mappings com pose. DTSTART;TZID=Europe/Paris:20080401T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200804011100 UID:semLSV.200804011100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Richard Bonichon - Relational data types an d proofs with Moca 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 generator for OCaml data types. It allows the definition of complex invariants on data typs\, which are then automagical ly managed. This talk will be divided into three parts: - I will first introduce some theoretical background about rela tional data types; - then I will show how one can specify an d use invariants with Moca; - I will end the talk with a dis cussion about how one can apply such a tool in the context o f automated theorem proving. We will in particular evoke the case of deduction modulo [3\, 4] and the zenon automated the orem prover [5\, 6]. [1] On the implementation of construc tor functions for non-free concrete data types. F. Blanqui\, T. Hardin et P. Weis [2] Moca [3] Theorem proving modulo \, revised version. G. Dowek\, Th. Hardin\, and C. Kirchner [ 4] TaMeD: a Tableaud Method for Deduction Modulo. R. Bonicho n [5] Zenon : An Extensible Automated Theorem Prover Produ cing Checkable Proof. R. Bonichon\, D. Delahaye and D. Dolige z [6] Zenon DTSTART;TZID=Europe/Paris:20080325T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200803251100 UID:semLSV.200803251100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : David Teller - Extrapol : Extraction de pol itiques de sécurité depuis C ATTENDEE;CN=David Teller: MAILTO:no@spam.com DESCRIPTION: De nos jours\, les technologies les plus avancées disponible s pour garantir la s-bûret-Aé d'un système Linux vis-à-vis de processus malicieux ou bogués sont SELinux\, AppArmor et quelques autres techniques comparables de pare-feux internes . Dans chacun des cas\, l'approche consiste à surveiller dyna miquement les interactions entre processus ou entre processu s et objets du système et à interdire celles qui ne sont pas explicitement autorisées par une "politique de sécurité". S i l'idée est intéressante\, son implantation se révèle souven t trop complexe pour la mise en oeuvre\, notamment en raison de la difficulté à valider une nouvelle politique de sécurit é sans devoir tester exhaustivement tous les logiciels insta llés. C'est à ce point qu'entre en jeu l'analyse statique : comment\, à partir d'une politique de sécurité\, vérifier sta tiquement la compatibilité avec les logiciels déjà installés sur le système\, ou avec 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èmes de types à la Hindley-Milner et des types dép endants\, nous définissons un mécanisme d'extraction de polit iques de sécurité à partir de bibliothèques et de fonctions écrites en langage C. Au cours de cet exposé\, nous présente rons le modèle de sécurité de SELinux\, la transformation de ce modèle en un jeu de contraintes sur le langage C et le pr ocessus d'extraction. DTSTART;TZID=Europe/Paris:20080318T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200803181100 UID:semLSV.200803181100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Michel de Rougemont - Approximate Satisfiab ility and Equivalence 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 between two formulas\, such that we gain an exponential factor (or m ore) in complexity. A typical case is to decide if two Non-d eterministic automata are equivalent: we decide the approxim ate version in polynomial time whereas the exact version is PSPACE complete. For Pushdown automata\, we decide the approx imate version in exponential time whereas the exact version is undecidable. DTSTART;TZID=Europe/Paris:20080311T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200803111100 UID:semLSV.200803111100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Damiano Mazza - Objets d'interaction et rés eaux différentiels 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 categoriq ue de modele denotationnel des combinateurs d'interaction\, b asée sur la notion d'"objet d'interaction". On terminera en voyant comment cette notion peut etre appliquee aussi aux re seaux d'interaction diffrentiels. DTSTART;TZID=Europe/Paris:20080304T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200803041100 UID:semLSV.200803041100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Thomas Reps - WYSINWYX: What You See Is Not What You eXecute 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 can cause analyses that are performed on source code -- which i s the approach followed by most security-analysis tools -- t o fail to detect bugs and security vulnerabilities. To addre ss the WYSINWYX problem\, we have developed algorithms to rec over information from stripped executables about the memory- access operations that the program performs. These algorithm s are used in the CodeSurfer/x86 tool to construct intermedi ate representations that are used for browsing\, inspecting\, and analyzing stripped x86 executables. Recently\, this infra structure has been used to create a tool for looking for bug s in stripped device-driver executables. Joint work with G. Balakrishnan (UW)\, J. Lim (UW)\, and T. Teitelbaum (Cornell and GrammaTech\, Inc.). DTSTART;TZID=Europe/Paris:20080219T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200802191100 UID:semLSV.200802191100 LOCATION:Salle Condorcet (Bâtiment d'Alembert) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Nathalie Bertrand - On decision problems fo r Probabilistic Büchi Automata ATTENDEE;CN=Nathalie Bertrand: MAILTO:no@spam.com DESCRIPTION: Probabilistic Büchi automata (PBA) are finite-state accepto rs for infinite words where all choices are resolved by fixe d distributions and where the accepted language is defined b y the requirement that the measure of the accepting runs is positive. In this work we describe a complementation operato r 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 transition system satisfies a PBA-specification\, turn out to be undeci dable. An important consequence of these results are several undecidability results for stochastic games with incomplete information\, modelled by partially-observable Markov decisi on processes (POMDP) and w-regular winning objectives. Furt hermore\, we study an alternative semantics for PBA where it is required that almost all runs for an accepted word are a ccepting\, which turns out to be less powerful\, but has a dec idable emptiness problem. This is a joint work with Christe l Baier and Marcus Groesser. DTSTART;TZID=Europe/Paris:20080205T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200802051100 UID:semLSV.200802051100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Colin Riba - Unions of Type Interpretations 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 b iorthogonality. In this talk we compare these different inte rpretations wrt their ability to handle rewriting and wrt th eir 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 sys tems 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 suffic ient 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 ca ndidates are stable by union. DTSTART;TZID=Europe/Paris:20080129T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200801291100 UID:semLSV.200801291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Alexis Bès - Automates et logiques pour les mots sur un alphabet infini ATTENDEE;CN=Alexis Bès: MAILTO:no@spam.com DESCRIPTION: Plusieurs modèles d'automates ont été proposés pour manipul er des mots sur un alphabet infini. Ces mots apparaissent pa r exemple dans l'étude de problèmes de vérification de systè mes distribués ou temporisés\, ou encore de manipulation de d onnées semi-structurées. Un objectif commun est d'obtenir un modèle à la fois simple et expressif\, et qui conserve tant que possible les bonnes propriétés du modèle classique. Dan s cet exposé on présentera un nouveau type d'automate dans l equel l'alphabet A est vu comme le domaine d'une structure M \, et les transitions de l'automate sont des formules du prem ier ordre écrites dans le langage de M. Ce modèle s'inspire directement de la notion de puissance généralisée de structu res introduite par Feferman et Vaught à la fin des années 19 50\, 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écision\, ainsi que plusieurs caractérisati ons logiques. On présentera également une extension du forma lisme 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/anciens?se m=200801081100 UID:semLSV.200801081100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Laurent Doyen - Equivalence of Labeled Mark ov Chains 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 reduction to the equivalence problem for probabilistic automata\, whic h is known to be polynomial. We provide an alternative algor ithm to solve the latter problem\, which is based on a new de finition of bisimulation for probabilistic machines. Then\, we consider the equivalence problem for labeled Markov decis ion processes (LMDPs) which asks given two LMDPs whether for every way of resolving the decisions in each of the process es\, there exists a way of resolving the decisions in the oth er process such that the resulting probabilistic machines ar e equivalent. The decidability of this problem remains open. We show that the strategies used to resolve the decisions c an be restricted to be observation-based\, but may require in finite 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/anciens?se m=200712181100 UID:semLSV.200712181100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Adam Cichon - Ordinal recursive bounds for Higman's lemma 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 characterisation is achieved with reference to known ordinal-recursive hiera rchies of number­theoretic functions.-A DTSTART;TZID=Europe/Paris:20071204T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200712041100 UID:semLSV.200712041100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Graham Steel - Formal Analysis of Security APIs 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 s uch as the keys used to obtain personal identification numbe rs (PINs). These HSMs have a restricted API that is designed to prevent malicious intruders from gaining access to the d ata. However\, several attacks have been found on these APIs\, as the result of painstaking manual analysis by experts suc h as Mike Bond and Jolyon Clulow. I have been carrying out research aimed at formalising and mechanising the analysis o f these APIs. This talk will present some API attacks\, and s ome automated formal analysis using theorem provers\, protoco l analysis tools\, and the PRISM probabilistic model checker. DTSTART;TZID=Europe/Paris:20071113T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200711131100 UID:semLSV.200711131100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Vlad Rusu - Integrating verification\, testi ng\, and learning for cryptographic protocols ATTENDEE;CN=Vlad Rusu: MAILTO:no@spam.com DESCRIPTION: Joint work with Martijn Oostdijk (Riscure\, NL)\, Jan Tretmans (EmbeddedSystems Institute\, NL)\, Rene de Vries (Radboud Uni versity Nijmegen\, NL)and T. Willemse (Eindhoven University o f Technology\, NL) The verification of cryptographic protoco l specifications is an activeresearch topic and has received much attention from the formalverification community. By co ntrast\, the testing of actual black-boximplementations of pr otocols\, which is\, arguably\, as important asverification for ensuring the correct functioning of protocols in the "real" world\, is little studied. We propose an approach for checki ngsecrecy and authenticity properties not only on protocol s pecifications\,but also on black-box implementations. The app roach is compositional andintegrates ideas from verification \, black-box testing\, and learning. Itis illustrated on the B asic Access Control protocol implemented inbiometric passpor ts. DTSTART;TZID=Europe/Paris:20071109T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200711091100 UID:semLSV.200711091100 LOCATION:Amphi 112 (Bât. d'Alembert\, couloir du LPQM) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Kostas Chatzikokolakis - Making Random Choi ces Invisible to the Scheduler 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 cus tomary to introduce the notion of scheduler to resolve the n ondeterminism. It has been observed that for certain applica tions\, notably those in security\, the scheduler needs to be restricted so not to reveal the outcome of the protocol's ra ndom choices\, or otherwise the model of adversary would be t oo strong even for "obviously correct" protocols. In this ta lk I present a process-algebraic framework in which the cont rol on the scheduler can be specified in syntactic terms\, an d I show how to apply it to solve the problem mentioned abov e. I also consider the definition of (probabilistic) may and must preorders\, and show that they are precongruences with respect to the restricted schedulers. Furthermore\, I show th at all the operators of the language\, except replication\, di stribute over probabilistic summation\, which is a useful pro perty for verification. This framework is applied to the din ing cryptographers problem\, where the scheduler problem come s into play. DTSTART;TZID=Europe/Paris:20071030T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200710301100 UID:semLSV.200710301100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Rohit Chadha - Decidability Results for Wel l-Structured Transition Systems with Auxiliary Storage 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 m any control states along with an auxiliary store\, but which have a well-quasi-ordering on the set of control states. Th e set of reachable configurations of the tomaton may themsel ves not be well-quasi-ordered because of the presence of the extra store. consider the coverability problem for such sy stems\, which asks if it is possible to reach a ntrol state ( with some store value) that covers some given control state. Our main result that if control state reachability is deci dable for automata with some store and finitely control sta tes then the coverability problem can be decided for WSTSs ( with infinitely many ntrol states) and the same store\, provi ded the ordering on the control states has some special pro perty. The special property we require is defined in terms o f the existence of a ranking ction compatible with the trans ition relation. We then show that there are several classes of nfinite state systems that can be viewed as WSTSs with an auxiliary storage. These can then be used to both reestabl ish old decidability results\, as well as discover new ones.J oint work with Mahesh Viswanathan. DTSTART;TZID=Europe/Paris:20071023T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200710231100 UID:semLSV.200710231100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : R. Ramanujam - Structured specification of strategies in games on graphs 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\, th is requires each player to know what every other player woul d do in every possible situation\, which is quite unrealistic in large games. We look at situations where players constru ct bounded memory strategies in a structured manner\, where t he opponent's strategy may be known only by its properties. In the new setting we study the algorithmic question of find ing best response for a player. We also present a simple mo dal logic to reason about strategies and show that checking assertion on a game graph is decidable. DTSTART;TZID=Europe/Paris:20070921T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200709211100 UID:semLSV.200709211100 LOCATION:Salle Condorcet (Bât. d'Alembert) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Deepak Kapur - Automatic Generation of Loop Invariants 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-e limination will be reviewed. Methods based on abstract inter pretation and ideal-theoretic semantics of programming langu age constructs will be discussed. An approach based on solvi ng recurrences will be presented. These methods have been im plemented and successfully tried on many programs implementi ng nontrivial number theoretic functions. Some preliminary i deas about how to generalize these approaches to work on dat a types other than numbers will be discussed. DTSTART;TZID=Europe/Paris:20070703T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200707031100 UID:semLSV.200707031100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Roberto Segala - Formal Verification of Sec urity Protocols using Automata 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\, a nd in particular how simulation-based proofs can be employed . The simulation method is useful in general to reduce the a nalysis of global properties to the analysis of local proper ties 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 proba bility of error\, we propose a notion of polynomially accurat e simulation relation for Probabilistic Automata and we illu strate it by analyzing a simple authentication protocol. In particular we show how the negation of the step condition of our simulation relation becomes the definition of a forger for a signature scheme. DTSTART;TZID=Europe/Paris:20070619T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200706191100 UID:semLSV.200706191100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Christoph Weidenbach - Automatic Analysis o f LAN Infrastructures ATTENDEE;CN=Christoph Weidenbach: MAILTO:no@spam.com DESCRIPTION: Important guarantees for LAN infrastructures include connect ivity\, error detection/recovery\, robust changes and security . In the talk I will develop a LAN infrastructure model in f irst-order logic enabling automatic analysis of such propert ies. The model starts at the ethernet layer of the TCP/IP st ack 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/anciens?se m=200706141100 UID:semLSV.200706141100 LOCATION:Amphi 109 N (bât L. de Vinci) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : K. Narayan Kumar - Local Testing of Message Sequence Charts is Difficult 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 Bhat eja\, Paul Gastin and Madhavan Mukund) DTSTART;TZID=Europe/Paris:20070529T110000 DURATION:PT1H URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/anciens?se m=200705291100 UID:semLSV.200705291100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT BEGIN:VEVENT STATUS:CONFIRMED ORGANIZER;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr CONTACT;CN=Séminaires du LSV:MAILTO:seminaire-request@lsv.ens-cachan.fr SUMMARY: SEM : Madhavan Mukund - Local Testing of Message Sequence Charts is Difficult 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 cha rts (TC-MSCs) is generated using an HMSC?a finite-state auto maton 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 s ystem specified as a time-constrained HMSC H and an implemen tation 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-constraine d HMSCs\, whose underlying behaviour is always regular. We al so describe a restricted solution for the general case. Thi s 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/anciens?se m=200705221100 UID:semLSV.200705221100 LOCATION:Salle de Conférence (Pavillon des Jardins) END:VEVENT END:VCALENDAR