Groupe de travail

Modélisation et Vérification

Salle 076 tous les jeudis 11H30

Date (YYYY-MM-DD)Orateur/AnimateurTitre
2010-07-01Florian Horn (LIAFA (Paris)) Solving Simple Stochastic Tail Games
Stochastic games are a natural model for open reactive processes: one player represents the controller and his opponent represents a hostile environnment. The evolution of the system depends on the decisions of the players, supplemented by random transitions. There are two main algorithmic problems on such games: computing the values (quantitative analysis) and deciding whether a player can win with probability 1 (qualitative analysis). In this paper we reduce the quantitative analysis to the qualitative analysis: we provide an algorithm for computing values which uses qualitative analysis as a sub- procedure. The correctness proof of this algorithm reveals several nice properties of perfect-information stochastic tail games, in particular the existence of optimal strategies. We apply these results to games whose winning conditions are boolean combinations of mean-payoff and Buchi conditions.
2010-06-03Camilo Rueda (Universidad Javeriana-Cali) A formal framework for social Networking
The talk presents Popar, an ongoing project that aims at using several formal
methods tools and techniques to develop a full-fledged social-network service implementing stipulated policies. The system includes a B method definition for social networking, modelling social-network content, privacy policies, social-networks friendship relations, and how these relations affect users' policies. This core is expected to be extended by third-party plug-ins in such a way that adherence to system policies is guaranteed by formal techniques such as proof-carrying code.
2010-05-27Nicolas Halbwachs (Verimag, Grenoble) Static analysis of positional and non positional properties of arrays
(joint work with Mathias Péron and Valentin Perrelle)

Although array bound checking was a motivation of the very first
work on abstract interpretation, there are only few proposals about
dealing with array *contents* in program analysis. The reason is,
of course, that the general problem is difficult: array indexing
induces complex semantics, and in particular the possibility of
aliasing; moreover, since the size of an array can be large or
unknown, it represents a large or unbounded number of variables.

In this talk, we present two complementary analyses dealing with
properties of array contents in some simple cases: one-dimensional
arrays, traversed by simple "for" loops. Both analyses are based
on abstract interpretation:
- the first one aims at discovering positional properties of arrays
elements. For instance, it is able to discover that the result of
an insertion sort is a sorted array.
- the second one addresses non positional properties, like the
fact that, at some point of a program, the content of an array is
a permutation of its initial content.
2010-05-20Bernard Boigelot (Institut Montefiore (Liège, Belgique)) Implicit Real Vector Automata
This work addresses the efficient handling of non-convex real
polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean
combinations of linear constraints. We develop a symbolic data
structure for representing such sets, based on an implicit and concise
encoding of a known structure, the Real Vector Automaton. The
resulting formalism provides a canonical representation of non-convex
polyhedra, is closed under Boolean operators, and admits an efficient
decision procedure for testing the membership of a vector.

Joint work with Julien Brusten and Jean-François Degbomont
2010-04-22Christophe Joubert (Technical University of Valencia, Spain ) Datalog-based Program Analysis with BES and RWL
In this talk, we present two powerful, fully automated methods to
evaluate Datalog queries in the context of object-oriented program
analyses: the first approach transforms the Datalog program in an
implicit Boolean Equation Systems (BESs) solved by existing general
purpose verification toolboxes, such as CADP, providing local BES
resolutions with linear-time complexity; the second approach
transforms Datalog programs into Rewriting Logic and produces an
efficient rewrite system exploiting the main features of the
high-level programming language Maude. Datalog is used as a
specification language for expressing both complex interprocedural
program analyses involving dynamically created objects and queries. We
confirm our results experimentally by applying it to some real-world
Datalog-based analyses.
2010-04-15Eugene Asarin (LIAFA (Paris)) Volume and entropy of regular timed languages
For timed languages, we define measures of their size: volume for a fixed finite number of events, and entropy (growth rate) as asymptotic measure for an unbounded number of events. These measures can be used for comparison of languages, and the entropy can be viewed as information contents of a timed language. In case of languages of deterministic timed automata, we give exact formulas for volumes. Next we characterize the entropy, using methods of functional analysis, as a logarithm of the leading eigenvalue (spectral radius) of a positive integral operator. We devise several methods to compute the entropy: a symbolical one for so-called “1 1/2-clock" automata, and two numerical ones: one using techniques of functional analysis, another based on discretization.

(joint work with Aldric Degorre, Concur'09+ Formats'09)
2010-04-01Arnaud Sangnier (Dipartimento di Informatica Università degli studi di Torino, Italy) When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (one-counter machines, reversal-bounded counter machines, vector additions systems with states, flat counter machines). Freeze LTL is an extension of the linear temporal logic to which registers are added. In this logic, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. We provide a systematic classification for the model-checking problem of freeze LTL over counter machines that distinguishes determinism vs. nondeterminism and we also consider subclasses of formulae by restricting the set of atomic formulae or/and the polarity of the occurrences of the freeze operators, leading to the flat fragment.

This is a joint work with Stéphane Demri (LSV, CNRS, ENS de Cachan) and Ranko Lazic (Department of Computer Science, University of Warwick).
2010-03-11Johannes Kinder (TU Darmstadt, Allemagne) Static Analysis of x86 Executables
Due to indirect branch instructions, analyses on executables commonly
suffer from the problem that a complete control flow graph of the
program is not available. Data flow analysis has been proposed before
to statically determine branch targets in many cases, yet a generic
strategy without assumptions on compiler idioms or debug information
was missing.

We have devised a framework for generic low level programs with
indirect jumps which safely combines a pluggable abstract domain with
the notion of partial control flow graphs. Using our framework, we
were able to show that the control flow reconstruction algorithm of our
disassembly tool Jakstab produces the most precise overapproximation
of the control flow graph with respect to the used abstract domain.

Based on this rigorous approach to disassembly, Jakstab has evolved
into a flexible program analysis framework on binaries. Preliminary
experiments with Windows driver binaries show that it can successfully
check API specifications with higher precision than existing
approaches, while achieving complete independence from source code.
2010-02-25Philipp Ruemmer (Oxford University, Computing Laboratory, UK) Craig Interpolation for Quantifier-Free Presburger Arithmetic
Craig interpolation has become a versatile tool in formal verification,
for instance to generate intermediate assertions for safety
analysis. Interpolants are often determined by annotating the steps
of an unsatisfiability proof with partial interpolants. In this
talk, I consider Craig interpolation for full quantifier-free
Presburger arithmetic (QFPA), for which until recently no efficient
interpolation procedures were known. As one such procedure, I introduce
an interpolating sequent calculus for QFPA and prove it to be sound
and complete. In particular, the complexity of extracting interpolants
from proofs is discussed. Finally, I add support for uninterpreted
predicates to the calculus, thus extending it to important theories such
as arrays and uninterpreted functions.

The talk describes joint work with Angelo Brillout, Daniel Kroening, and
Thomas Wahl.
2010-02-18Peter Habermehl (LIAFA) On non-deterministic automata for Presburger arithmetic.
A well-known decision procedure for Presburger arithmetic (PA)
uses deterministic finite-state automata. While the complexity
of the decision procedure for PA based on quantifier elimination
is known (triple-exponential), the exact complexity of the
automata-based procedure was unknown. We show that it is triple-exponential
as well by analysing the structure of the non-deterministic automata
obtained during the construction building on results from Klaedtke.
Furthermore, we analyse the sizes of deterministic and non-deterministic
automata built for several subclasses of Presburger arithmetic.
To retain a canonical representation which is one of the strengths of
the use of automata we use a class of non-deterministic automata
called residual finite-state automata introduced by Denis, Lemay and Terlutte.
2010-02-11Mauricio Toro (LaBRI) Towards a Computational Modeling of an Heterogeneous System for Interactive Musical Scores
Interactive scores (IS) are a formalism for composition and performance of musical pieces composed by temporal objects, temporal structures and discrete interactive events. IS may be used for the composition and performance of Electroacoustic music; to control image, video, audio and lights on live spectacles and interactive museums; and to help handicapped and begginer musicians to perform a difficult piece. Currently, there is not an IS model that allows temporal constraints, logical branching, global constraints, and audio/video streams simultaneusly. We propose using the FAUST system to process audio/video streams and the Non-deterministic Timed Concurrent Constraint (ntcc) calculus to cope with the other phenomena. We plan to develop a model for IS, where ntcc and FAUST interact, and to use model checking techniques to verify it*.

*This is one of the objectives to accomplish in my doctorate, which I started on october 2009.
2010-02-04Mathieu Tracol (LRI) Recurrence and Transience for Probabilistic Automata
Dans le context des automates de Buchi sur les mots infinis, la
condition d'acceptation classique (de Buchi) pour un run est qu'il passe
infiniment souvent sur un etat acceptant. Un mot est alors accepté s'il
existe un run acceptant pour ce mot. Dans un contexte d'automates
probabilistes (PBA), un mot est accepté si la probabilité de l'ensemble
des runs pour ce mot qui passent infiniment sur un etat acceptant est
strictement positive. Avec cette definition, il devient indecidable de
decider si le language d'un PBA est vide ou non. On relaxe la definition
d'acceptation d'un run en demandant maintenant que la proportion du temps
passé sur un des etats acceptants ne tend pas vers zero. Decider le vide
du language devient alors decidable. Nous etudions la complexité du
probleme de decision associé (PSPACE complet), et nous etudions les
propriétés de cloture de notre nouvelle classe d'automates probabilistes.
L'essentiel de l'etude se ramene à l'etude de la notion de recurrence dans
le cas des chaines de Markov non-homogenes.
2010-01-14Peter Niebert (LIF, Marseille) L'approche SAT pour lpour automates temporisés avec étapes parallèles
Plusieurs travaux ont exploré la possibilité d'améliorer les algorithmes d'exploration d'états symboliques (zones) pour automates temporisés par une sémantique d'ordres partiels. A priori, ces sémantiques sont contre-intuitives, parce que le temps, représenté par des nombres réels, est un ordre total.
D'un autre coté, pour des systèmes non-temporisés, on connaît des réductions SAT qui utilisent une sémantique avec transitions parallèles : la possibilité d'exécuter plusieurs transitions indépendantes en parallèle raccourcit des séquences témoin et permet ainsi d'aller plus loin avec la vérification bornée.
Dans notre travail, nous combinons les deux améliorations, ordres partiels pour automates temporisés et transitions parallèles pour une meilleure réduction SAT. Il se pose alors la question de ce que sont des « transitions parallèles » pour un automate temporisé. Autre que la réponse intuitive « en parallèle est en même temps » nous explorons deux autres sémantiques avec des notions plus relâchées pour les transitions parallèles. Il s'avère que les trois sémantiques ont des performances incomparables, selon les exemples considérés.
À l'occasion, je présente aussi le vérificateur POEM, qui est la plate forme expérimentale avec laquelle nous avons réalisé le prototype et les expériences.
2010-01-07Julien Forget (LaBRI) Un Langage Synchrone pour les Systèmes Embarqués Critiques Temps Réel
Ce séminaire sera l'occasion de présenter les travaux effectués au cours de ma thèse.
L'exposé porte sur la programmation de systèmes de Contrôle-Commande. Ces systèmes sont constitués d'une boucle de contrôle qui acquiert l'état actuel du système par des capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Ces systèmes sont critiques, leur implantation doit donc être déterministe, sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates).

Nous définissons un langage de description d'architecture logicielle temps réel et son compilateur pour programmer de tels systèmes. Il permet d'assembler les composants fonctionnels d'un système multi-rythme avec une sémantique formelle synchrone. Un programme consiste en un ensemble d'opérations importées, reliées par des dépendances de données. Des contraintes de périodicité ou d'échéance peuvent être spécifiées sur les opérations et un ensemble réduit d'opérateurs de transition de rythme permet de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes.

Des analyses statiques assurent que la sémantique d'un programme est bien définie. Un programme correct est ensuite compilé en un ensemble de tâches temps réel concurrentes implantées sous forme de threads C communicants. Le code généré préserve la sémantique du programme
original et s'exécute à l'aide d'un Système d'Exploitation Temps Réel standard disposant de la politique d'ordonnancement EDF.
2009-12-17Pierre-Alain Reynier (LIF, Marseille) Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study
In this talk, we show how to apply recent tools for the automatic synthesis of robust and near-optimal controllers for a real industrial case study. We show how to use three different classes of models and their supporting existing tools, UPPAAL - TIGA for synthesis, PHAVER for verification, and SIMULINK for simulation, in a complementary way.
2009-12-10Stéphane Demri (LSV, ENS-Cachan) Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents.
Les systèmes d'addition de vecteurs arborescents (BVAS) forment un modèle
formel de calcul qui est
utilisé par exemple en linguistique ou pour la vérification de protocoles
cryptographiques. Ce modèle a
aussi des liens étroits avec des logiques de données interprétées sur des
arbres avec valeurs mais aussi
avec la logique linéaire MELL. La décidabilité du problème d'accessibilité
pour ces systèmes demeure
encore aujourd'hui ouverte, et ce problème est équivalent à divers
problèmes essentiels des domaines
cités plus haut.
Récemment, Verma et Goubault-Larrecq ont réussi à montrer que les
problèmes de finitude et de
couverture pour les BVAS sont décidables.

Dans cet exposé, je vais présenter comment caractériser la complexité des
problèmes de couverture
et de finitude pour les BVAS. Une partie de la preuve consiste à raffiner
les travaux de Rackoff dans le
cas linéaire correspondant au modèle des réseaux de Petri.

Ce travail a été mené conjointement avec Marcin Jurdzinski, Oded Lachish
et Ranko Lazic
(University of Warwick, UK).
2009-12-03François Laroussinie (LIAFA) Alternating-time Temporal Logic: Expressivity, Complexity, Extensions
In this talk we will consider several temporal logics for
expressing properties over games (modeled with
Concurrent Game Structures).
We will present ATL, ATL* and also two extensions:
with strategy contexts and with memory constraints.
The first extension makes strategy quantifiers to
not ``forget'' the strategies being executed by the other players.
The second extension allows strategy quantifiers to restrict to
memoryless or bounded-memory strategies.

We will first consider expressiveness issues. We show that our logics can
express important properties such as equilibria, and we formally
compare them with other similar formalisms ATL, ATL*, Game Logic, AMC,
Strategy Logic,... We will also address the problem of model-checking
for these logics.

Joint work with: Th. Brihaye, A.. Da Costa, N. Markey.
2009-11-26Jean Goubault-Larrecq (LSV, ENS-Cachan) Games on Infinite Domains and Approximation
I'll give an overview of research I have been
doing over the last few years in semantic models
of mixed non-deterministic and probabilistic choice.
One can also see this as models for two-player
turn-based (stochastic) games, where the state space
X is infinite. The approach is topological and
domain-theoretical. In particular, X need not
be Hausdorff, which leads to interesting models
where the knowledge of the current state can itself
be approximate.
We shall give a brief tour of these, through capacity-based
models, prevision models, simulation and (if time
permits) simulation (hemi-)metrics.
2009-11-12Alexander Heussner (LaBRI) Reachability Analysis of Communicating Pushdown Systems
The reachability analysis of recursive programs that communicate
over asynchronous and reliable fifo channels calls for restrictions
to ensure decidability. We extend here a model proposed by La Torre,
Madhusudan and Parlato [TACAS08], based on communicating pushdown
systems that can dequeue with empty stack only. Our extension adds
the dual modality, which allows to dequeue with non-empty stack, thus
modelling interrupts for working threads. We study (possibly cyclic)
network architectures under a semantic assumption (mutex
communication) that ensures the decidability of reachability for
finite state systems. Subsequently, we determine precisely how
pushdowns can be added to this setting while preserving the
decidability; in the positive case we obtain exponential time as the
exact complexity bound of reachability. A second result is a
generalization of the doubly exponential time algorithm of [LaTorre
et al: TACAS08] for bounded context analysis to our symmetric
queueing policy. We provide here a direct (and simpler) proof.

Joint work with Jérôme Leroux, Anca Muscholl, Grégoire Sutre
2009-11-05Mohamed-Faouzi Atig (LIAFA) On the Verification Problem for Weak Memory Models
We address the verification problem of finite-state concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multi-processor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performance-critical system services employing lock-free synchronization, as well as for the correctness of compiler backends that generate code targeted to run on such architectures.

We consider in this work combinations of three well-known program order relaxations. We consider first the "write to read" relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the "write to write" relaxation (leading to a model which is essentially PSO), or (2) the "read to read/write" relaxation, or (3) both of them (as it is done in the RMO model for instance).

We define abstract operational models for these weak memory models based
on state machines with (potentially unbounded) FIFO buffers, and we
investigate the decidability of their reachability and their repeated
reachability problems.

We prove that the reachability problem is decidable for the TSO model, as well as for its extension with "write to write" relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the "read to read/write" relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. As for the repeated reachability problem, we prove that it is undecidable already for the TSO model.

(Joint work with Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi)
2009-10-22Tristan Le Gall (ULB, Bruxelle, Belgique) Control of Infinite Symbolic Transition Systems under Partial Observation
We propose algorithms for the synthesis of state-feedback
controllers through partial observation of infinite state systems
modelled by Symbolic Transition Systems.

To obtain algorithms for solving these problems, we use abstract
interpretation techniques which provide over-approximations of the
transitions set to be disabled.

We implemented those algorithm in a tool and made an empirical validation of our
methods to show their feasibility and usability.


Keywords: Symbolic Transition Systems, Control Synthesis,
Partial Observation, Abstract Interpretation.


Joint work with Gabriel Kalyon, Tristan Le Gall, Hervé Marchand and Thierry Massart.
2009-09-29Anil Seth (IIT Kanpur, India) Parity Games on Multistack Systems
In this talk we present higher order multi-stack
pushdown systems (hmpds). We show that parity games
over bounded phase hmpds are effectively solvable and
winning strategy in these games can be effectively
synthesized.
The proof is by reducing the parity games over bounded
phase hmpds to finite state parity games. We shall
describe this reduction in some detail.


Responsables


Hugo GIMBERT
Jérôme LEROUX
first.LAST@labri.fr