Centre Fédéré en Vérification






2002-2003 Seminars

  • Infinite Games: Fundamental Results and Some Perspectives
    • Speaker: Wolfgang Thomas, RWTH Aachen
    • Date: January 17, 2003
    • Abstract:

      The purpose of this lecture is to survey the essentials of the algorithmic theory of infinite games, its role in program synthesis and verification, and some challenges of current research. More specifically, the following topics will be addressed: Finite-state games, the topological classification of winning conditions, game reductions, positional versus finite-state strategies, games over finitely presented infinite transition graphs.

    • Photograph of the seminar:
      Picture of W. Thomas
      Click to enlarge !
  • Automatic verification of unbounded security protocols
    • Speaker: Yassine Lakhnech, VERIMAG, Grenoble
    • Date: February 21, 2003
    • Abstract:

      At the heart of any computer security system are security protocols, also called cryptographic protocols. The design and implementation of these protocols is an error prone activity. Moreover, most of the errors are not due to weakness in the cryptographic system but rather in the logic underlying the protocol. In other words, most of the errors remain even when assuming idealized cryptographic primitives. Defining a semantic model for security protocols and formally defining what "secrecy", " authentification" etc.. mean is a difficult task. Moreover, these protocols are infinite state systems: the intruder knowledge is unbounded, the number of sessions is unbounded, the size of messages is unbounded, the number of principals is unbounded, etc... In this talk, we will survey the main results concerning the modeling and verification of security protocols. In particular, we will explain a new automatic verification method for security protocols that is applicable to unbounded protocols.

  • The Verification of Probabilistic Lossy Channel Systems
    • Speaker: Philippe Schnoebelen, LSV, ENS Cachan
    • Date: March 21, 2003
    • You can donwload here the slides of the seminar (PDF, 223 Kb).
    • Abstract:

      Lossy Channel Systems (LCS's) are systems of finite-state automata that communicate via unbounded fifo channels along which messages can be lost without any notification (hence the "Lossy"). They are a natural model for asynchronous protocols that are supposed to tolerate unreliable communication, of the kind one meets in embedded systems, in mobile systems, or on the WWW. Recently, several papers have proposed versions of LCS's where the losses of messages follow probabilistic rules. Sometimes the motivation is to obtain a finer view of the behaviour, where quantitative properties can be stated. Sometimes the goal is to circumvent undecidability by randomization. In this talk we will survey these different proposals and assess their interest. Special emphasis will be put on explaining the underlying algorithmic ideas in general terms that can be understood by computer scientists with no background in probabilistic systems.

    • Photographs of the seminar:
      Picture of P. Schnoebelen Picture of P. Schnoebelen Picture of B. De Wachter
      Click to enlarge !
  • Automata-theoretic techniques for the analysis of multithreaded programs
    • Speaker: Ahmed Bouajjani, LIAFA, Université de Paris 7
    • Date: May 9, 2003
    • Abstract:

      We consider the verification problem of programs with unbounded (1) recursive procedure calls, and (2) dynamic creation of concurrent processes. We show different models for programs based on extended automata and process rewrite systems, and show different approaches for tackling their verification problem.

      In a first approach, programs are modeled using term rewrite systems called PRS (for process rewrite systems). These models are more powerful than pushdown automata and Petri nets, two common models for reasoning about, respectively, recursive programs without process creation, and multi-threaded programs without recursive calls. A PRS can actually be seen as the nesting of prefix rewrite system and a multiset rewrite system. We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is effectively semilinear (preserves semilinearity). We represent PRS reachability sets by means of a class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to various reachability analysis procedures for classes of PRSs.

      In a second approach, programs are modeled using a more general class of rewrite systems (including concurrent pushdown systems). The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths for which emptiness can be decided. Our method allows to compute such abstractions as least solutions of a system of language constraints. Given a program, (1) we build a system of constraints which characterizes precisely the set of its computation paths, and then (2) this system can be solved in various abstract domains leading to abstract analysis with different precision and cost. We show how to construct this set of constraints using automata-theoretic techniques for reachability analysis of process rewrite systems, and how to solve this set of constraints in a framework based on abstract interpretation.

  • Performance Evaluation and Model Checking: a Perfect Match
    • Speaker: Joost-Pieter Katoen, University of Twente
    • Date: June 13, 2003
    • Please note that this seminar will be held at room NO7.07, at the 7th floor of the NO building (which is the usual one).
    • Abstract:

      Markov chains are one of the most important stochastic processes. They have been widely used to determine system performance and dependability characteristics such as the throughput of production lines, the mean time between failure in safety-critical systems, and bottleneck analysis for high-speed communication networks. Their analysis most often concerns the computation of steady-state and transient-state probabilities.

      In this talk, we present branching temporal logics for expressing real-time probabilistic properties over Markov chains and show how such properties can be checked in a fully automated way. These logics can express standard steady-state and transient-state probabilities in a lucid and abstract way and allow for the specification of more involved, non-trivial performance measures. The algorithms used are a combination of numerical analysis methods (such as uniformization and techniques for solving linear systems of equations), graph algorithms and -- most importantly -- model checking. We show how this approach can be applied to discrete-time and continuous- time Markov chains and reward extensions thereof and show some practical applications.

    • Photographs of the seminar:
      Picture of J-P Katoen Picture of J-P Katoen
      Click to enlarge !

Links to other seminars




Thu Dec 18 10:46:35 CET 2003