|
|
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:
|
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:
- 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:
|
|
Click to enlarge ! |
Links to other seminars
|
|