Abstract : Number Decision Diagrams (NDD) are the automata-based symbolic representation for manipulating regular sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969, we know that any Presburger-definable set (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed. However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 with a quadruply-exponential time algorithm. In this presentation, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set.
The slides of the talk are available here.
The seminar is based on the following technical report.
Jeux infinis.
Olivier Serre
(LIAFA, Paris 7, France & RTWH Aachen, Germany)
Abstract : Two-player games on infinite graphs provide a natural model for infinite open systems: the program is represented by the first player, Eve, and the environment is represented by the second player, Adam. In this framework, Eve has a winning strategy if and only if there exists a controller for the program that ensures that a property, described by the winning condition, is satisfied.
In this setting, the (infinite) system is described by an infinite (game) graph and the specification by a language of infinite winning play (i.e. path) in the previous graph. Therefore, the choice of the graph and the one of the winning condition are crucial for expressiveness but also for decidability and complexity.
In this survey, we present various classes of infinite graphs for which (some) games are decidable: pushdown graphs, prefix-rewriting graphs and high-order pushdown graphs. All these graphs allow to model programs using recursivity.
We also give a large variety of decidable winning conditions for these games, and particularly for pushdown games. A special attention will be devoted to winning conditions of practical interest for verification of infinite systems, in particular to those concerning the height of the stack.
Here are the slides in PDF or in PostScript.
Material: the talk is based on material of several papers. See e.g.
Abstract : Within this talk I will provide background on how to deal with the arithmetic in real world programming languages such as Java or current implementations of C where integer types are meant to take values in modular rings Zm where m=2w. Clearly, these rings are finite but obviously tremendously large for realistic values of w (e.g., 32 or 64). Also for w>1, these rings have zero divisors. I will show that, nonetheless, all affine relations which are valid at program points of affine programs can be determined in polynomial time - only using arithmetic within the ring Zm itself. Thus, any potential swell of intermediately occurring large numbers is banned.
The talk is based on the following paper,
to appear in the Proceedings of ESOP 2005.
Weakly relational abstract domains and the efficient inference of
numerical properties in large and infinite systems
Antoine Miné
(LIENS, Paris, France)
Abstract :
In this presentation, we wish to share our experience with the design of
numerical domains for the analysis of real-life embedded critical avionic
softwares.
The main difficulties were: the correct abstraction of floating-point and
machine-integer arithmetics, the need for relational invariants able to
precisely abstract assignments, guards, and loop invariants, and,
finally, the scalability to programs of hundreds of thousands lines long.
To achieve our goal, that is, prove the absence of run-time errors, we
designed many techniques that work together.
We will present some of them that are of general interest:
the octagon domain, specific abstract transfer functions and widenings,
expression linearization, symbolic constant propagation, and variable
packing.
The Verification of Probabilistic Timed Systems.
Christel Baier
(Univ. Bonn, Germany)
Abstract : In this talk, I will provide an overview of the techniques that have been developed for the algorithmic analysis of probabilistic systems with real-time constraints. The underlying model is a probabilistic extension of timed automata. The properties are specified by probabilistic real-time logics which allow one to formalize properties such as "with probability at least 0.99, the message is correctly delivered within 10 ms". In essential, the verification problem for such quantitative properties can be reduced to the model checking problem for finite-state probabilistic systems using region- or zone graph constructions as they are known for non-probabilistic systems.
Material: The talk is based on material of several papers. See e.g.
Abstract :
In the last years we have used
pushdown automata as an abstract formalism for the analysis
and verification of programs with possibly recursive procedures,
and other authors have used equivalent models. Tools based on
our results are being used as back end verifiers in several projects.
An interesting challenge is the extension of these techniques to
probabilistic programs. Probabilities can be an
intrinsic part of the program (as in randomized algorithms),
or be added to a program in order to model the behaviour of
the environment.
Probabilistic pushdown automata and recursive Markov chains
are two equivalent and natural models for
probabilistic procedural programs. In the talk we survey recent
results on the decidability and complexity of verification problems
for these models, pointing out the differences with the finite-state
case.
Here are the slides from the FST&TCS 2004 talk, and the corresponding
paper. There also is a LICS 2004 paper.
Asychronously Communicating Systems
Anca Muscholl
(LIAFA, Paris 7, France)
Abstract : Message sequence charts (MSC, formerly known as timing diagrams) are a popular visual notation for describing asynchronous communication protocols at early design stages in form of scenarios. MSC and high-level MSC (HMSC) is a standard of the ITU (CCITT) and integrated in the specification formalism UML.
The use of MSC and HMSC for early specification of protocol behaviors has raised several algorithmic questions related to the automatic validation of properties. Two basic problems are model-checking (testing whether the specification satisfies some positive/negative property) and implementability (checking whether the specification can be implemented by some machine-like model, e.g. communicating finite state machines).
This talk gives a survey on the two validation problems mentioned above. We discuss the expressivity of various MSC classes and their relationship with other distributed automata models. We also present extensions of the original MSC notation, that aim at supporting the design process and the algorithmic validation at reasonable costs.
Here are the PowerPoint slides. An interesting survey is available here.
Abstract : Timed automata are a widely used model for real-time systems, which has been defined at the beginning of the 90s by Alur & Dill. Since many properties (reachability, properties expressed in timed extensions of temporal logics, etc...) are decidable for it, this model has attracted a lot of attention. In particular, several works have studied the decidability (of rechability properties) for extensions of timed automata. In this talk we will give an overview of decidability results for slight extensions of timed automata, ranging from features that can be added to timed automata (e.g. operations on clocks) to more structural extensions (e.g. alternation).
Here are the slides of the presentation.
Flat Acceleration: the Theory Behind FAST.
S. Bardin
(LSV, ENS de Cachan, France)
Abstract : Symbolic model-checking provides partially effective procedures to perform reachability analysis, even when the system under consideration has an infinite state space. So-called ``acceleration techniques'' enhances convergence by computing the transitive closure of some transitions. In this paper we introduce a generic framework for accelerated symbolic model-checking. We identify three main levels of acceleration and provide corresponding symbolic procedures. For the level of flat acceleration, we propose several algorithmic and/or heuristic refinements to improve efficiency. These refinements have been implemented and validated in FAST, a tool for verification of counter systems.
This is joint work with A. Finkel, J. Leroux and Ph. Schnoebelen.
The
slides of the presentation are available here.