
Liste des événements uniques du groupe Modélisation et Verification
20151210  Optimisation souscontraintes appliquée à l'analyse statique de programmes 
11:0012:00 076 
Depuis une dizaine d'années, les techniques d'optimisation
souscontraintes (LP, SDP, SOS...) apparaissent en vérification de programmes
numériques par analyse statique.
Dans ma présentation, je montrerai comment générer des modèles
utilisant ces techniques pour prouver automatiquement des propriétés
sur des programmes numériques grâce à leur représentation par des
systèmes dynamiques à temps discret.

 Plus d'infos 

20150924  Improving search order for reachability testing in timed automata 
11:0012:00 076 
Standard algorithms for reachability analysis of timed automata are sensitive to the order in which the transitions of the automata are taken. To tackle this problem, we propose a ranking system and a waiting strategy.
This paper discusses the reason why the search order matters and shows how a ranking system and a waiting strategy can be integrated into the standard reachability algorithm to alleviate and prevent the problem respectively. Experiments show that the combination of the two approaches gives optimal search order on standard benchmarks
except for one example. This suggests that it should be used instead of the standard BFS algorithm for reachability analysis of timed automata. 
 Plus d'infos 

20150625  Path Logics for Querying Graphs: Combining Expressiveness and Efficiency 
11:0012:00 076 
We study logics expressing properties of paths in graphs that are tailored to querying graph databases. The basic construct of such logics, a regular path query, checks for paths whose labels belong to a regular language. These logics fail to capture two commonly needed features: counting properties, and the ability to compare paths. It is known that regular pathcomparison relations (e.g., prefix or equality) can be added without significant complexity overhead; however, adding common relations often demanded by applications (e.g., subword, subsequence, suffix) results in either undecidability or astronomical complexity.
We propose, as a way around this problem, to use automata with counting functionalities, namely Parikh automata. They express many counting properties directly, and they approximate many relations of interest. We prove that with Parikh automata defining both languages and relations used in queries, we retain the low complexity of the standard path logics for graphs. In particular, this gives us efficient approximations to queries with prohibitively high complexity. This is a joint work with Leonid Libkin. 
 Plus d'infos 

20150611  Abstracting Path Conditions 
11:0012:00 076 
We present a symbolicexecutionbased algorithm that for a given
program and a given program location in it produces a nontrivial
necessary condition on input values to drive the program execution to
the given location. The algorithm is based on computation of loop
summaries for loops along acyclic paths leading to the target
location. We also propose an application of necessary conditions in
contemporary bugfinding and testgeneration tools. Experimental
results on several small benchmarks show that the presented technique
can in some cases significantly improve performance of the tools.

 Plus d'infos 

20150604  Safety of parametrized asynchronous sharedmemory systems is almost always decidable 
11:0012:00 076 
Verification of concurrent systems is a difficult problem in general,
and this is the case even more in a parametrized setting where
unboundedly many concurrent components are considered. Recently,
Hague proposed an architecture with a leader process and unboundedly
many copies of a contributor process interacting over a shared memory
for which safety properties can be effectively verified. All
processes in Hague's setting are pushdown automata.
We extend this setting by considering other formal models and, as a
main contribution, find very liberal conditions on the individual
processes under which the safety problem is decidable: the only
substantial condition we require is the effective computability of the
downward closure for the class of the leader processes.
Furthermore, our result allows for a hierarchical approach to
constructing models of concurrent systems with decidable safety
problem: networks with treelike architecture, where each process
shares a register with its children processes (and another register
with its parent). Nodes in such networks can be for instance pushdown
automata, Petri nets, or multipushdown systems with decidable
reachability problem.
Joint work with Salvatore La Torre and Anca Muscholl. 
 Plus d'infos 

20150528  An Introduction to Software Transactional Memory 
11:0012:00 076 
Software Transactional memory (or STM for short) is a promising programming paradigm that aims at simplifying concurrent programming by using the notion of a transaction. A transaction executes a piece of code containing accesses to data items which are shared by several processes in a concurrent setting. By using transactions, the programmer needs only enhance its sequential code with invocations of special operations to read or write data items. It is guaranteed that if any operation of a transaction takes place, they all do, and that if they do, they appear to other threads to do so atomically, as one indivisible operation.
In this talk, I will present the STM paradigm and the main algorithmic techniques to implement it. 
 Plus d'infos 

20150521  Ideals And Well Quasi Orders (Part III) 
11:0012:00 076 
More than 30 years after their inception, the decidability proofs for
reachability in vector addition systems (VAS) still retain much of
their mystery. These proofs rely crucially on a decomposition of runs
successively refined by Mayr, Kosaraju, and Lambert, which appears
rather magical.
This talk offers a justification for this decomposition technique, by
showing that it emerges naturally in the study of the ideals of well
quasi ordered sets. A lot of applications of this recent breakthrough is
expected on various VAS extensions. This is a joint work with Sylvain
Schmitz.
PART I (45 minutes): Ideals for well quasi ordered sets.
PART II (45 minutes): Ideals of the VAS runs.
PART III (45 minutes): End of Part II. 
 Plus d'infos 

20150507  Ideals And Well Quasi Orders (Part II) 
11:0012:00 076 
More than 30 years after their inception, the decidability proofs for
reachability in vector addition systems (VAS) still retain much of
their mystery. These proofs rely crucially on a decomposition of runs
successively refined by Mayr, Kosaraju, and Lambert, which appears
rather magical.
This talk offers a justification for this decomposition technique, by
showing that it emerges naturally in the study of the ideals of well
quasi ordered sets. A lot of applications of this recent breakthrough is
expected on various VAS extensions. This is a joint work with Sylvain
Schmitz.
PART I (45 minutes): Ideals for well quasi ordered sets.
PART II (45 minutes): Ideals of the VAS runs. 
 Plus d'infos 

20150416  Ideals And Well Quasi Orders (Part I) 
11:0012:00 076 
More than 30 years after their inception, the decidability proofs for
reachability in vector addition systems (VAS) still retain much of
their mystery. These proofs rely crucially on a decomposition of runs
successively refined by Mayr, Kosaraju, and Lambert, which appears
rather magical.
This talk offers a justification for this decomposition technique, by
showing that it emerges naturally in the study of the ideals of well
quasi ordered sets. A lot of applications of this recent breakthrough is
expected on various VAS extensions. This is a joint work with Sylvain
Schmitz.
PART I (45 minutes): Ideals for well quasi ordered sets.
PART II (45 minutes): Ideals of the VAS runs. 
 Plus d'infos 

20150402  Vérification de propriétés MSO sur les pomsets 
11:0012:00 076 
Un comportement d’un système distribué se modélise naturellement par un ensemble d’événements partiellement ordonnées (pomset) : La relation d’ordre définie la relation de causalité entre les événements et deux événements causalement indépendants s’exécutent en parallèle. Dans cet exposé, nous proposons une méthode de vérification de la logique MSO applicable à la plus part des modèles classiques du parallélisme. Nous introduisons la notion Gpomset, une représentation d’un pomset par mot et montrons comment le problème de la vérification de MSO sur les pomsets se ramène à un problème de vérification de MSO sur des mots. 
 Plus d'infos 

20150319  The subtle alchemy of concurrency and realtime 
11:0012:00 076 
Formal models for realtime distributed systems, like time Petri nets and networks of timed automata have proved their interest for the verification of realtime systems. On the other hand, the question of using these models as specifications for designing realtime systems raises several difficulties. Here we focus on the ones that are related to the distributed nature of the system. Implementing a model may be possible at the cost of some transformations, which make it suitable for the target device. In this talk, I present several results about semantics of distributed realtime systems and provide methods for the design of such systems. 
 Plus d'infos 

20150305  Reachability in MDPs: Refining Convergence of Value Iteration 
11:0012:00 075 
Markov Decision Processes (MDP) are a widely used model including both
nondeterministic and probabilistic choices. Minimal and maximal
probabilities to reach a target set of states, with respect to a
policy resolving nondeterminism, may be computed by several methods
including value iteration. This algorithm, easy to implement and
efficient in terms of space complexity, consists in iteratively
finding the probabilities of paths of increasing length. However, it
raises three issues: (1) defining a stopping criterion ensuring a
bound on the approximation, (2) analyzing the rate of convergence, and
(3) specifying an additional procedure to obtain the exact values once
a sufficient number of iterations has been performed. The first two
issues are still open and for the third one a « crude » upper bound on
the number of iterations has been proposed. Based on a graph analysis
and transformation of MDPs, we address these problems. First we
introduce an interval iteration algorithm, for which the stopping
criterion is straightforward. Then we exhibit convergence
rate. Finally we significantly improve the bound on the number of
iterations required to get the exact values. 
 Plus d'infos 

20150122  On the parameterized verification of asynchronous sharedmemory systems 
11:0012:00 076 
I will present a recent paper of Esparza, Ganty and Majumdar (CAV'13, ) showing
that under the assumption of nonatomicity of R/W operations on the shared memory,
parameterized verification of pushdown processes becomes decidable.
Link to the paper: http://arxiv.org/pdf/1304.1185 
 Plus d'infos 

20141218  Cost functions and Value 1 problem in practice 
11:0012:00 076 
I will present a tool implementing algorithms on an algebraic structure called stabilization monoids. This monoids are used to abstract various quantiative behaviours, and allow to solve problems like boundedness of particular weighted automata (namely Bautomata from the theory of cost functions), or the value 1 problem for a special class of probabilistic automata (called leaktight).
I will briefly explain the theory behind these problems, as well as how cost functions were motivated by historical problems like starheight, and finally demonstrate how
the tool works.
This is joint work with Nathanael Fijalkow, a newer optimized version is in progress with Nathanael Fijalkow, Hugo Gimbert and Edon Kelmendi. 
 Plus d'infos 

20141204  Alternating Vector Addition Systems with States 
11:0012:00 076 
Vector addition systems with the ability to `fork' into independent
computations were originally defined in the study of propositional
linear and relevance logics. Recently, more ties with
multidimensional energy games, finitesystem simulations, and
zeroreachability games were noticed. I shall survey both these
relationships and complexity results.
Based on work with JeanBaptiste Courtois presented at MFCS (with a
full paper available on HAL: ),
and on ongoing work with Marcin Jurdzinski and Ranko Lazic. 
 Plus d'infos 

20141127  IC3: model checking avec SAT, 2ème partie 
11:0012:00 076 

 Plus d'infos 

20141106  Reachability In Vector Addition with States and Split/Join Transitions 
11:0012:00 076 
We define Vector Addition with States and Split/Join Transitions, a new model that extends VASS. Nonnegative reachability in this model without join transitions is known to be equivalent to the decidability of MELL, and to be TOWERhard. As a first step towards a reachability result, we define a suitable notion of covering graph for the model, and prove its finiteness and effective constructibility. 
 Plus d'infos 

20141023  IC3: model checking avec SAT 
11:0012:00 075 

 Plus d'infos 

20141016  Zeno, Hercules and the Hydra 
11:0012:00 076 
Metric temporal logic (MTL) is one of the most prominent specification
formalisms for realtime systems. Over infinite timed words, full MTL
is undecidable, but satisfiability for its safety fragment was proved
decidable several years ago. The problem is also known to be
equivalent to a fair termination problem for a class of channel
machines with insertion errors. However, the complexity has remained
elusive, except for a nonelementary lower bound. Via another
equivalent problem, namely termination for a class of rational
relations, we show that satisfiability for safety MTL is not primitive
recursive, yet is Ackermannian, i.e., among the simplest nonprimitive
recursive problems. This is surprising since decidability was
originally established using Higman's Lemma, suggesting a much higher
nonmultiply recursive complexity.
Joint work with Joel Ouaknine and James Worrell.

 Plus d'infos 

20140918  Branching bisimulation for normed commutative context free grammars 
11:0012:00 076 
Bisimulation is known and well studied equivalence relation between states of a labeled transition system, however there is no canonical extension of it to systems with epsilon transitions.
There are several candidates among which the best known are weak and branching bisimulation. During the talk I will present some ideas behind one of algorithms to compute branching bisimulation for infinite state systems, namely those induced by normed commutative context free grammars. I will start from basic definitions and then I will go to the sketch of the proof.
This talk bases on a joint work with Wojciech Czerwinski and Slawomir Lasota published on Concur 2011. 
 Plus d'infos 

20140605  Sequentialization and Bounded Modelchecking 
11:0012:00 076 
Bounded model checking (BMC) has successfully been used
for many practical program verification problems, but concurrency still
poses a challenge. Sequentializations have emerged as an efficient technique
to obtain analysis tools for concurrent programs by reusing tools designed for sequential programs.
In this talk, we describe some recent results concerning the design and the implementation of
efficient sequentializations targeted to using BMC tools as backends.
The presented sequentializations are implemented in the tool CSeq
(http://users.ecs.soton.ac.uk/gp4/cseq/cseq.html). 
 Plus d'infos 

20140602  Why Amazon Chose TLA+ 
11:3012:30 Amphi du LaBRI 
Since 2011, engineers at Amazon have been using TLA+ to help solve difficult
design problems in critical systems. This talk describes the reasons why we
chose TLA+ instead of other methods, how we’ve applied it so far, and areas in which we would welcome further progress. 
 Plus d'infos 

20140522  Analysis of Concurrent Programs via Sequentialization 
11:0012:00 076 

 Plus d'infos 

20140417  Monotonicity in OneCounterSystems: what gives? 
11:0012:00 076 
I will discuss several basic problems involving onecounter automata (OCA)
with special focus on the impact of monotonicity.
First we will recall a characterization of reachability based on Valiant's
classic "hill cutting" argument, which leads to an NL decision procedure.
Not surprisingly, many problems involving two OCA are already undecidable:
(Trace) inclusion and equivalence, simulation preorder, weak (and branching)
bisimulation and so on.
Forbidding zerotests in OCA results in a model called onecounter nets (OCN)
which corresponds to 1dimensional VASS and lies in the intersection of VASS
and pushdown systems. Due to the monotonicity of the step relation in OCN,
some of the problems mentioned above become decidable.
I will discuss our technique for deciding strong simulation for OCN and
mention some implications, generalizations and open problems.
Keywords: counterautomata, reachability, simulation, energy games. 
 Plus d'infos 

20140313  The Power of Priority Channel Systems 
11:0012:00 076 
We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higherpriority messages can supersede lowerpriority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a wellquasiordering that has not previously been used in wellstructured systems. We then show how Priority Channel Systems can compute FastGrowing functions and prove that the aforementioned verification problems are F_{epsilon_{0}}complete.
Joint work with Christoph Haase and Philippe Schnoebelen. A short version was presented at Concur 2013; see http://arxiv.org/abs/1301.5500 for the full paper. 
 Plus d'infos 

20140220  Static analysis of programs manipulating arrays 
11:0012:00 076 
Static analysis is a key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs, ...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections)
Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition.
The choice of this partition is a difficult problem and each method has its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes.
We generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.

 Plus d'infos 

20140213  Binary Analysis: Theory and Practice 
11:0012:00 205, bât A29 
Since now, program analysis was performed only on
mathematical models of the program or highlevel source code. We aim at
performing an analysis only based on the binary form of the program and,
if possible deduce useful properties of the program (either for software
verification or reverseengineering purposes). In this talk, we will
define and present the main problems encountered when dealing with the
binary format of programs. 
 Plus d'infos 

20140206  The Power of WellStructured Systems 
11:1512:15 076 
Wellstructured systems, aka WSTS, are computational models where the set of possible configurations is equipped with a wellquasiordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying wellstructured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some "bad" sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterizing the power, in a complexitytheoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems.
[ Paper ]
Joint work with Sylvain Schmitz.

 Plus d'infos 

20140123  Towards distributed monitoring (of Android applications) 
11:0012:00 076 
In this talk, I will present some recent results on the topic of monitoring. The first part presents a solution for monitoring distributed systems. The second part presents what the techniques of runtime monitoring allow when trying to improve the security, safety and reliability of Android applications.
Part 1: Decentralized LTL Monitoring. Users wanting to monitor distributed or componentbased systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behavior as opposed to many components displaying many local behaviors that together constitute the system's global behavior. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system's global behavior in terms of an LTL formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components' local behaviors are observable.
Part 2: Runtime Verification and Enforcement for Android Applications with RVDroid. RVDroid is an implemented framework dedicated to runtime verification (RV) and runtime enforcement (RE) of Android applications. RVDroid consists of an Android application that interacts closely with a cloud. Running RVDroid on their devices, users can select targeted Android applications from Google Play (or a dedicated repository) and a property. RVDroid is generic and currently works with two existing runtime verification frameworks for (pure) Java programs: with Java MOP and (partially) with RuleR. RVDroid does not require any modification to the Android kernel and targeted applications can be retrieved offtheshelf. We carried out several experiments that demonstrated the effectiveness of RVDroid on monitoring (security) properties. 
 Plus d'infos 

20140116  Meet Your Expectations With Guarantees: Beyond WorstCase Synthesis in Quantitative Games 
11:0012:00 076 
We extend the quantitative synthesis framework by going beyond the worstcase. On the one hand, classical analysis of twoplayer games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees. On the other hand, stochastic models like Markov decision processes represent situations where the system is faced to a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worstcase synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worstcase while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. We study the beyond worstcase synthesis problem for two important quantitative settings: the meanpayoff and the shortest path. In both cases, we show how to decide the existence of finitememory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements. 
 Plus d'infos 

20131219  Contribution à la vérification d'automates temporisés: déterminisation et vérification quantitative 
11:0012:00 076 
Cet exposé porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes tempsréel. L'exposé est constitué de deux parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (surapproximation, sousapproximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes tempsréel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure nondéterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. 
 Plus d'infos 

20131212  Verification of Concurrent Programs: Decidability, Complexity, Reductions 
11:0012:00 076 
Concurrency is present at different levels, from applications using high level synchronization mechanisms and abstract data structures under atomicity and isolation assumptions, to low level code implementing concurrent/distributed data structures and system services over multicore architectures/large scale networks.
We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity: We will show the difficulties that raise in addressing this problem at the different levels mentioned above (huge amount of computations, complex control due to recursion and dynamic task creation, weak memory models, etc.), and we will overview existing approaches for tackling these issues. We will show in particular how the verification problems that must be considered in this context can be reduced to "simpler" problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already known verification algorithms and tools. 
 Plus d'infos 

20131205  Knowledge Compilation for Model Counting: Afﬁne Decision Trees 
11:0012:00 076 
Counting the models of a propositional formula is a key issue for many AI problems, but few propositional languages offer the possibility to count models efficiently. In order to fill the gap, we recently introduced the extended affine decision tree language (EADT). An extended affine decision tree simply is a tree with affine decision nodes and some
specific decomposable conjunction or disjunction nodes. Unlike standard decision trees, the decision nodes of an EADT formula are not labeled by variables but by affine clauses. During this talk, a brief overview of the different compilation languages and their theoritical caracteristics will be done. Then, we will focus on EADT and several of its subsets regarding the knowledge compilation map. We also describe a CNFtoEADT compiler and present some experimental results. 
 Plus d'infos 

20131128  [Discussion] Exploitation de la structure dans les modèles 
11:0012:00 076 
Nous manipulons dans l'équipe de nombreux modèles assez différents
mais dans lesquels la structuration joue toujours un rôle important.
Certaines structurations aident à la conception et à la maintenance de
modèles, d'autres à la conception d'algorithmes efficaces.
Cette discussion ouverte à tous a pour but de réfléchir aux
utilisations possibles des structures qu'on peut trouver ou
découvrir dans un modèle en échangeant les bonnes recettes que les
uns et les autres ont pu rencontrer dans leurs domaines respectifs. 
 Plus d'infos 

20131121  Hyper Ackermannian Bounds for Pushdown Vector Addition Systems 
11:0012:00 076 
We study the complexity of deciding boundedness of Well Structured
Transition Systems equipped with a stack. We introduce a general
scheme of induction for bounding lengths of bad nested words over a well
quasi ordered set. We use this scheme to show that lengths of bad
nested words over vectors of natural numbers is bounded by a
function in the class F_ω^ω of the extended
Gregorczyk hierarchy. This upper bound is used to derive an upper
bound for the running time of an algorithm we give, which is an
extension of the classical Karp & Miller algorithm for deciding
boundedness. We give a matching lower bound to show that the worst
case running time of this extended algorithm can not be below F_ω^ω.

 Plus d'infos 

20131114  Inclusion problems for OneCounter Nets 
11:0012:00 205, bât A29 
A fundamental question in formal verification is the inclusion problem, that
asks if the behaviour of one process can be reproduced by another. Just as
equivalence and model checking problems, inclusion has been extensively studied
for various notions of behavioural preorders and for many computational models.
This talk will focus on OneCounter Nets (OCN), which consist of a finite
control and a single integer counter that cannot be fully tested for zero.
OCN form a natural subclass of both OneCounter Automata and thus Pushdown
Systems, which allow explicit zerotests and Petri Nets/VASS, which allow
multiple such weak counters. They are arguably the simplest model of discrete
infinitestate systems but make an interesting case study for different
settings of the inclusion problem.
I will highlight recent results on trace/language inclusion for OCN. This
problem is NLcomplete if only one of the given processes is deterministic.
At the same time, trace universality for (nondeterministic) OCN is already
Ackermanian. 
 Plus d'infos 

20131107  Multistack Pushdown Systems: formal languages theories 
11:0012:00 076 
Multistack pushdown systems are natural models for capturing the control flow of multithreaded programs. The intuition of exploring computations up to a bounded number of context switches has stimulated a series of interesting results in program verification, such as for example the possibility of sequentializing concurrent programs without maintaining the crossproduct of the involved threads, and the study of the formal theory of decidable subclasses.
In this talk, we focus on the formal languages theory of the classes of MPS with the boundedcontext switching, scopebounded, phasebounded, and stackordered restrictions. We also discuss some related results in verification. 
 Plus d'infos 

20131024  AltaRica 
11:0012:00 076 
AltaRica est un langage, basé sur une description arborescente d'automates à contraintes, pour la description des aspects fonctionnels et dysfonctionnels de systèmes réactifs.
La première partie de l'exposé rappellera les objectifs et les choix initiaux du langage et son évolution à travers différents projets.
La seconde partie décrira et justifiera les choix technologiques retenus lors des différentes versions des outils.
La fin de l'exposé sera consacrée aux problèmes rencontrés actuellement pour traiter certains exemples industriels, et aux pistes envisagées pour les résoudre. 
 Plus d'infos 

20131017  SAT Solvers and Model Checking 
11:0012:00 076 
Since the first complete SAT solvers (DPLL62, based on classical backtracksearch), major breakthroughs were observed in the practical – and theoretical – study of SAT. Nowadays, SAT solvers can be used in many critical systems, from very hard problems (Formal Verification, Biology, Cryptology) with potentially long runs, to more reactive applications (were a SAT solver can be called many times per second). In this talk, we will review the progresses made since the first breakthrough of 2001, with the introduction of CDCL solvers, called “modern solvers”. We will show how the field is slowly moving from a “complete” vision of Solvers to a more “uncomplete” one. We will end the talk by some open questions on the future of SAT Solvers, and the recent trends in "incremental SAT Solving", where SAT solvers are called thousand times for each run. 
 Plus d'infos 

20131003  Disjunctive Interpolants for HornClause Verification 
11:0012:00 076 
One of the main challenges in software verification is efficient and
precise compositional analysis of programs with procedures and loops.
Interpolation methods remain one of the most promising techniques for
such verification, and are closely related to solving Horn clause
constraints. In this talk, I introduce a new notion of interpolation,
disjunctive interpolation, which solves a more general class of
interpolation problems in one step, compared to previous notions of
interpolants, such as tree interpolants or inductive sequences of
interpolants. I present algorithms and complexity for construction of
disjunctive interpolants, as well as their use within an
abstractionrefinement loop. We have implemented Horn clause
verification algorithms that use disjunctive interpolants and evaluate
them on benchmarks expressed as Horn clauses over the theory of integer
linear arithmetic.
This talk presents joint work with Hossein Hojjat and Viktor Kuncak. 
 Plus d'infos 

20130620  Splitwidth technique for the verification of concurrent programs with data structures 
11:3012:30 076 
We consider systems of concurrent boolean programs equipped with several data structures. The data structures can be unbounded stacks or unbounded queues. Each data structure allows write access to only one process (call it writer), and read access to only one (possibly different) process (call it reader). A stack whose writer and reader are the same corresponds to an unbounded local stack of the writer. A queue serves as an unbounded reliable FIFO channel from its writer to its reader. As these systems are very powerful, they render most verification problems undecidable.
We introduce a parameter called splitwidth for its underapproximate verification. Splitwidth is a notion similar to treewidth, but more handy for the systems we consider. Restricting to bounded splitwidth behaviors gives an EXPTIME decision procedure for model checking these systems against temporal logics and propositional dynamic logics, and a decision procedure for model checking against MSO. We show that splitwidth can capture several interesting and relaxed scheduling policies.
This is a joint work with Paul Gastin and K. Narayan Kumar.

 Plus d'infos 

20130613  Acceleration For Presburger Petri Nets 
11:3012:30 076 
The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flatable, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set. 
 Plus d'infos 

20130606  On the Contextfreeness Problem for Vector Addition Systems 
11:3012:30 076 
Petri nets, or equivalently vector addition systems (VAS),
are widely recognized as a central model for concurrent systems.
Many interesting properties are decidable for this class,
such as boundedness, reachability, regularity,
as well as contextfreeness, which is the focus of this paper.
The contextfreeness problem asks whether the trace language
of a given VAS is contextfree.
This problem was shown to be decidable by Schwer in 1992,
but the proof is very complex and intricate.
The resulting decision procedure relies on five technical conditions over
a customized coverability graph.
These five conditions are shown to be necessary,
but the proof that they are sufficient is only sketched.
In this paper, we revisit the contextfreeness problem for VAS,
and give a simpler proof of decidability.
Our approach is based on witnesses of noncontextfreeness,
that are bounded regular languages satisfying a nesting condition.
As a corollary,
we obtain that the trace language of a VAS is contextfree if,
and only if,
it has a contextfree intersection with every bounded regular language. 
 Plus d'infos 

20130530  Exact algorithms for stochastic games and real algebraic geometry 
11:3012:30 076 
Shapley's discounted stochastic games and Everett's recursive games are classical
models of game theory describing twoplayer zerosum games of potentially infinite
duration. We present an exact algorithm for solving such games based on separation
bounds from real algebraic geometry. When the number of positions of the game is
constant, the algorithm runs in polynomial time and is the first with this property.
We also present lower bounds on the algebraic degree of the values of stochastic
games induced from the irreducibility of polynomials that have coefficients that
depend on the combinatorial parameters of the games, based on a generalization
of Eisenstein criterion. 
 Plus d'infos 

20130516  Path Analysis in OTAWA Framework 
11:3012:30 076 
OTAWA (Open Tool for Adaptive WCET Analysis) is an open framework dedicated to the computation of WCET (Worst Case Execution Time). To be sound, effective and precise, this type of analysis must be performed at the machine code level that requires to decode and build back the execution paths of the program.
A challenging and interesting issue of path analysis is that the embedded realtime systems, targeted by the OTAWA, exhibit a lot of different ISA (Instruction Set Architecture) like PowerPC, Sparc, ARM, TriCore, etc. As it would be a possible but a tedious and errorprone solution to implement these backends by hand, OTAWA reuse a wellknown technology based on ADL (Architecture Description Language). Basically, ADL were developed to allow automatic and safe generation of ISS (Instruction Set Simulator) including the ability of decoding instructions from the binary code. In OTAWA, we have adapted an existing ADL generator, called GLISS, not only to get an instruction decoder but also to provide other useful information items like target of branches, used registers, type of instructions, etc.
Decoding instructions is necessary to build back execution paths but we need also to get a simple and concise representation of the execution paths. CFG (Control Flow Graph) is good and common candidate: starting from the function entry points, they are build by following the instruction control flow to get edges and by grouping instruction in basic blocks to improve compactness of the representation. Yet, it remains some constructions that are hard to handle, i.e. indirect or computed branches, whose target can not be obtained by just looking to the instructions. This constructions are induced by the use of function pointers or by optimization of switchlike statements in highlevel languages. The determination of the possible target of such branches requires to perform data flow analysis based on machine code and once again, the ADL have been used in OTAWA to easily produce semantics of machine code instruction making the data flow analysis independent of the actual ISA.
The presentation will be followed by a demonstration of the OTAWA plugin in the Eclipse environment. 
 Plus d'infos 

20130425  Automatic security proof of cryptographic primitives: public encryption, symmetric encryption modes, MAC 
11:3012:30 076 
Our aim is to develop a formal method in order to prove cryptographic primitives. We consider cryptographic primitives as small programs, usually it is just few lines of code. In the last century Tony Hoare provided mechanisms in order to prove that a program is correct, socalled Hoare logic.
Our approach consists in the three following steps:
Modeling properties that studied primitives have to ensure by proposing some invariants.
Defining the language which represent the small set of commands used to construct a primitives at the good abstract level.
Proving Logics rules, that allows us to generate and propagate invariants according to the commands executed in the program.
Once the language fixed, the invariants developed and the rules of the Hoare Logic established, we can verify a primitive. Using this approach we have developed three logics to prove security of several public encryption schemes, symmetric encryption modes and also several MAC. 
 Plus d'infos 

20130404  The Insight binary analysis framework 
11:3012:30 076 
In this talk, we will present the current status of the Insight
project which is aimed at analysing binary code.
Binary code analysis is challenging because of the inherent
difficulties of analysing code where the control flow graph is not
explicitly given, where datatypes are not available, compounded with
the technical challenge of decoding mnemonics of real processors as
complex as the Intel 32bit architecture.
The formal model used in Insight will be presented, and an application
to CFG recovery will be detailed. Further work will be discussed. 
 Plus d'infos 

20130328  Costoptimal factored planning using weighted automata calculus 
11:3012:30 076 
Factored planning is a relatively new domain in planning. It consists in exploiting the possible decompositions of many planning problems into exponentially smaller subproblems in order to efficiently solve them by parts. Even if, in the worst case, the complexity of factored planning is the same as the complexity of classical planning, in many cases of interest it is much more efficient. However, before this work, no factored planning method existed to compute costoptimal solutions to planning problems. In this talk we will present an approach to factored planning allowing to find costoptimal solutions thanks to the use of weighted automata calculus. The principle of this approach is to represent the set of solutions of each subproblem as a weighted automaton and apply a standard message passing algorithm to the network constituted by all these automata. This allows to compute new automata representing exactly those solutions of subproblems which are part of solutions of the global planning problem, and from that to give a globally optimal solution of this planning problem in a modular way. 
 Plus d'infos 

20130307  A semidecidable approach for determining language inclusion for timed automata 
11:3012:30 076 
Language inclusion for timed automata is known to be undecidable. The
universality problem can be considered to be a special case of the
language inclusion problem. Given a universal timed automaton A and any
other timed automaton B, the language inclusion problem asks if the timed
language accepted by A is included in the timed language accepted by B.
Solving this problem implies deciding the universality problem for B which
is known to be undecidable!
In this work, we present a semidecidable algorithm which gives three
outputs as follows: 'yes' indicates that we conclude that the language
accepted by A is a subset of the language accepted by B. 'no' indicates
that the language accepted by timed automaton B does not include the
language accepted by A. 'do not know' indicates that we do not know how
the langauges accepted by A and B are related.
The language inclusion problem for timed automata is known to be decidable
when timed automaton B is deterministic or determinizable or when timed
automaton B (strongly time) simulates timed automaton A or when B is a
single clock timed automaton. We show that our method works in many cases
where B cannot simulate A or B cannot be determinized.

 Plus d'infos 

20130221  Equivalence Checking of Pushdown Automata and OneCounter Automata 
11:3012:30 076 
The first part of my talk will be about bisimilarity of onecounter automata (which are pushdown automata over a singleton stack symbol with a bottomofstack symbol). I will show that this problem is PSPACEcomplete, improving the previously bestknown 3EXPSPACE upper bound by Yen (joint work with Stanislav Böhm and Petr Jancar).
The second part of the talk will be about the complexity of bisimilarity checking of pushdown automata. While decidability of this problem has been shown by Sénizergues, no complexitytheoretic upper bound of this problem is known to date. I will present a recent nonelementary lower bound for this problem, improving the previously bestknown EXPTIMEhardness result of Kucera and Mayr (joint work with Michael Benedikt, Stefan Kiefer and Andrzej Murawski). 
 Plus d'infos 

20130131  Reasoning about Data Repetitions with Counter Systems 
11:3012:30 076 
We study lineartime temporal logics interpreted
over data words with multiple attributes. We restrict the atomic
formulas to equalities of attribute values in successive positions
and to repetitions of attribute values in the future or past.
We demonstrate correspondences between satisfiability problems
for logics and reachabilitylike decision problems for counter
systems. We show that allowing/disallowing atomic formulas
expressing repetitions of values in the past corresponds to the
reachability/coverability problem in Petri nets. This gives us
2EXPSPACE upper bounds for several satisfiability problems. We
prove matching lower bounds by reduction from a reachability
problem for a newly introduced class of counter systems. This
new class is a succinct version of vector addition systems with
states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further
the correspondences between data logics and counter systems
by characterizing the complexity of fragments, extensions and
variants of the logic. For instance, we precisely characterize the
relationship between the number of attributes allowed in the logic
and the number of counters needed in the counter system.
This is joint work with Stephane Demri and Diego Figueira.

 Plus d'infos 

20130124  Underapproximation of Procedure Summaries for Recursive Integer Programs 
11:3012:30 076 
We show how to underapproximate the procedure summaries of recursive programs
over the integers using offtheshelf analyzers for nonrecursive programs. The
novelty of our approach is that the nonrecursive program we compute may capture
unboundedly many behaviors of the original recursive program for which stack
usage cannot be bounded. Moreover, we identify a class of recursive programs on
which our method terminates and returns the precise summary relations without
underapproximation. Doing so, we generalize a similar result for nonrecursive
programs to the recursive case. Finally, we present experimental results of an
implementation of our method applied on a number of examples.
Joint work with Pierre Ganty (IMDEA) and Filip Konecny (EPFL). 
 Plus d'infos 

20130117  Beautiful Games You Cannot Stop Playing 
11:3012:30 076 
Parity games are simple two player games played on a finite arena that have all that it takes to attract the attention of researchers: it is a simple problem which is hard to analyse. A pocket version of P vs. NP.
Parity games are known to be in UP, CoUP, and some weirder classes besides, but whether or not they are in P has proven to be a rather elusive question. What is more, when you work with them, you will have the constant feeling that there is a polynomial time solution just around the corner, although it dissolves into nothingness when you look more closely. This talk is about the beauty of these games, the relevant algorithmic approaches and their complexity and development over time. But be careful: they are addictive, don't get hooked!

 Plus d'infos 

20130110  Timebounded reachability for monotonic hybrid automata 
11:3012:30 076 
Hybrid automata (HA) form a very popular class of model for describing hybrid systems, i.e. systems that exhibit both discrete and continuous behaviors. An HA is roughly speaking a finite automaton augmented with a finite set of realvalued variables, whose values evolve continuously with time elapsing. The rate of growth of those variables can change along time and depends on the current location of the automaton. Unfortunately, HA are notoriously hard to analyse: even the reachability problem is undecidable on the very restricted subclass of stopwatch automata (where variables can have rates 0 or 1 only).
However, most of the undecidability results on HA rely on the unboundedness of time to encode runs of undecidable models such as twocounter machines. A natural question is thus to study the timebounded variant of the verification problems on HA, hoping that this additional requirement will allow to recover decidability. A further incentive is the recent line of research by Ouaknine, Worrell, et al., who have shown the benefits of considering timebounded variants of classical problems in the case of (alternating) timed automata.
In this talk, we study the timebounded reachability problem for monotonic rectangular hybrid automata (MRHA). An MRHA is a rectangular hybrid automata where the rate of each clock is either alway nonnegative, or always nonpositive. We show that this problem is decidable (even though the unbounded reachability problem for even very simple classes of hybrid automata is wellknown to be undecidable), and give a precise characterisation of its complexity: it is NExpTimec. We also show that extending this class by either allowing a clock to have positive and negative rates in the same HA, or by allowing diagonal guards, leads to undecidability, even in bounded time. Finally, we present a more practical extension of our positive result, by showing that we can effectively compute fixpoints characterising the sets of states that are reachable (resp. coreachable) within T time units from a given state.
This is joint work with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, JeanFrançois Raskin and James Worrell.

 Plus d'infos 

20121220  Runtime Enforcement of Timed Properties 
11:3012:30 076 
Runtime enforcement is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies to a property. Runtime enforcement has been extensively studied over the last decade in the context of untimed properties. In this talk, we introduce runtime enforcement of timed properties. We revisit the foundations of runtime enforcement when time between events matters. We discuss how runtime enforcers can be synthesized for a safety or cosafety timed property. Proposed runtime enforcers are time retardant: to produce an output sequence, additional delays are introduced between the events of the input sequence to correct it. 
 Plus d'infos 

20121206  A perfect model for bounded verification 
10:1511:15 Salle Patio  Bat C4 "Hautcarré" 
A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for contextfree languages is undecidable, no class containing them can be perfect.In practice, verification problems for language classes that are not perfect are often underapproximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages. A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language.We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multihead pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multithreaded programs, recursive counter machines, and communicating finitestate machines can be encoded as multihead pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages. 
 Plus d'infos 

20121206  Multidimension Quantitative Games: Complexity and Strategy Synthesis 
11:1512:15 Salle Patio  Bat C4 "Hautcarré" 
In meanpayoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multimeanpayoff and multienergy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resourcebounded processes with multiple resources. In this talk, I will summarize several recent results that we have obtained recently: We prove the finitememory determinacy of multienergy games and show the interreducibility of multimeanpayoff and multienergy games for finitememory strategies. We improve the computational complexity for solving both classes of games with finitememory strategies: while the previously best known upper bound was ExpSpace, and no lower bound was known, we give an optimal coNPcomplete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NPcomplete. We provide an optimal symbolic and incremental algorithm to synthesis strategies in multienergy games. We present the first solution of multimeanpayoff games with infinitememory strategies. We show that multimeanpayoff games with meanpayoffsup objectives can be decided in NP and in coNP, whereas multimeanpayoff games with meanpayoffinf objectives are coNPcomplete. 
 Plus d'infos 

20121129  Safety Verification of Communicating OneCounter Machines 
11:3012:30 076 
In order to verify protocols that tag messages with integer
values, we investigate the decidability of the reachability
problem for systems of communicating onecounter machines. These
systems consist of local onecounter machines that asynchronously
communicate by exchanging the value of their counters via, a
priori unbounded, FIFO channels. This model extends communicating
finitestate machines (CFSM) by infinitestate local processes
and an infinite message alphabet. The main result of the paper
is a complete characterization of the communication topologies
that have a solvable reachability question. As already CFSM
exclude the possibility of automatic verification in presence of
mutual communication, we also consider an underapproximative
approach to the reachability problem, based on rendezvous
synchronization.
Joint work with Alexander Heußner and Tristan Le Gall. 
 Plus d'infos 

20121108  Coarse abstractions make Zeno behaviors difficult to detect 
11:3012:30 076 
An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are nonZeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NPcompleteness for the LUextrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LUextrapolation that satisfies these conditions. 
 Plus d'infos 

20121004  Reachability of Communicating Timed Processes 
11:3012:45 076 
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises au tomata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topologypreserving reductions between timed automata and (untimed) counter automata.

 Plus d'infos 

20120927  Strategy Synthesis (From Specification to Implementation) 
11:3012:30 076 
This is a short jeurney from the pitfalls and beauty of Church's problem from an automata theoretic angle. We will admire the simplicity of the problems and some funny effects, from forcing the branching mode of the automata involved to the cost incurred. After looking at how we can keep our life simple for a price too hight to pay, we return more and more to the real problem and see with (maybe) some surprise that the it is even simpler. Probably. But we will prove that it is unlikely that we will ever discover the truth. 
 Plus d'infos 

20120607  Parameterized Complexity of some Petri Net Problems 
11:3012:30

Parameterized complexity is the branch of complexity theory that seeks to identify in the computational complexity of some problems the dependence on different parameters of the input. The coverability and boundedness problems for Petri nets are known to be EXPSPACEcomplete. Previous work [Ex: L.E. Rosier and H.C. Yen. A multiparameter analysis of the boundedness problem for vector addition systems. JCSS 32, 1986] has already been done to analyse the dependency of this complexity on different parameters, such as the number of places, maximum arc weight etc. We continue this work and study the dependency of the complexity on two parameters called benefit depth and vertex cover. If k denotes a parameter and n denotes the size of the input for a problem, then the problem is said to be in the parameterized complexity class PARAPSpace if there is an algorithm to solve the problem that uses memory space O(f(k)poly(n)), where f(k) is any computable function of the parameter and poly(n) is some polynomial of the input size. We show PARAPspace results for the coverability and boundedness problems using the parameters mentioned above. We also show PARAPspace results for model checking a logic that can express some extensions of coverability and boundedness. This is joint work with Kamal Lodaya. 
 Plus d'infos 

20120524  Querying Schemas With Access Restrictions 
11:0012:00 076 
We study verification of systems whose transitions consist of
accesses to a Webbased datasource. An access is a lookup
on a relation within a relational database, fixing values for
a set of positions in the relation. For example, a transition
can represent access to a Web form, where the user is restricted
to filling in values for a particular set of fields. We
look at verifying properties of a schema describing the possible
accesses of such a system. We present a language where
one can describe the properties of an access path, and also
specify additional restrictions on accesses that are enforced
by the schema. Our main property language, AccLTL, is
based on a firstorder extension of lineartime temporal logic,
interpreting access paths as sequences of relational structures.
We also present a lowerlevel automaton model, Aautomata,
which AccLTL specifications can compile into.
We show that AccLTL and Aautomata can express static
analysis problems related to “querying with limited access
patterns” that have been studied in the database literature
in the past, such as whether an access is relevant to answering
a query, and whether two queries are equivalent in
the accessible data they can return. We prove decidability
and complexity results for several restrictions and variants
of AccLTL, and explain which properties of paths can be
expressed in each restriction. 
 Plus d'infos 

20120510  Tagging Make Local Testing of MessagePassing Systems Feasible 
11:3012:30 076 
The only practical way to test distributed messagepassing systems is
to use local testing. In this approach, used in formalisms such as
concurrent TTCN3, some components are replaced by test
processes. Local testing consists of monitoring the interactions
between these test processes and the rest of the system and comparing
these observations with the specification, typically described in
terms of message sequence charts. The main difficulty with this
approach is that local observations can combine in unexpected ways to
define implied scenarios not present in the original
specification. Checking for implied scenarios is known to be
undecidable for regular specifications, even if observations are made
for all but one process at a time. We propose an approach where we
append tags to the messages generated by the system under test. Our
tags are generated in a uniform manner, without referring to or
influencing the internal details of the underlying system. These
enriched behaviours are then compared against a tagged version of the
specification. Our main result is that detecting implied scenarios
becomes decidable in the presence of tagging.
This is joint work with Puneet Bhateja.

 Plus d'infos 

20120503  Bounded Phase Analysis of MessagePassing Programs 
11:3012:30 076 
We describe a novel technique for bounded analysis of asynchronous
messagepassing programs with ordered message queues. Our bounding
parameter does not limit the number of pending messages, nor the
number of “contextsswitches” between processes. Instead, we limit the
number of process communication cycles, in which an unbounded number
of messages are sent to an unbounded number of processes across an
unbounded number of contexts. We show that remarkably, despite the
potential for such vast exploration, our bounding scheme gives rise to
a simple and efficient program analysis by reduction to sequential
programs. As our reduction avoids explicitly representing message
queues, our analysis scales irrespectively of queue content and
variation. 
 Plus d'infos 

20120412  Model Checking Languages of Data Words 
11:3012:30 076 
We consider the modelchecking problem for data multi pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic secondorder (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as firstorder logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.
This is a joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar. 
 Plus d'infos 

20120405  Forward Analysis for WSTS : Beyond Regular Accelerations 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
The wellknown Karp and Miller algorithm constructs the
coverability tree of a Vector Addition System, obtaining a finite representation
of the cover (the downward closure of the reachability set).
The series "Forward analysis in WSTS" aims to generalize this procedure for
arbitrary wellordered state spaces. I'll first recall the earlier works by Finkel
and GoubbaultLarrecq, that introduced the notion of complete WSTS, in
which a finite representation of the cover as set of maximal elements exists.
Then, i'll present our formalization of acceleration strategy and a parameterized Karp Miller procedure that relies on these strategy in order to compute this
set of maximal elements.
As an illustration of these ideas, I'll present an acceleration strategy for
Vector Addition Systems with two resets that allows the previously defined
procedure to terminate, effectively computing the finite representation of the cover.
This is joint work with Alain Finkel. 
 Plus d'infos 

20120329  The Quantitative LinearTime–BranchingTime Spectrum 
11:3012:30 076 
We present a distanceagnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a gamebased framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic lineartime–branchingtime spectrum to a quantitative setting, parametrized by trace distance. We also provide fixedpoint characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent. 
 Plus d'infos 

20120322  Exploiting Structure in LTL Synthesis 
11:3012:30 076 
The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the lowlevel programming tasks, by replacing them with the design of highlevel specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for generalpurpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent datastructures.
Reactive systems are nonterminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safetycritical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2Exptime complete problem.
In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded modelchecking, and show that the high worstcase time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem 
 Plus d'infos 

20120315  Compositional Specification Theories for Stochastic Systems 
11:3012:30 076 
Markov Chains (MCs) and Probabilistic Automata (PAs) are
widelyrecognized mathematical frameworks for the specification and
analysis of systems with nondeterministic and/or stochastic behaviors.
Notions of specification, implementation, satisfaction, and refinement,
together with operators supporting stepwise design, constitute a
specification theory. In the early 1990's, an abstraction of Markov
Chains, called Interval Markov Chains (IMCs) has been proposed as a
specification theory. This talk shows why IMCs are not perfectly suited
to play their role as a specification theory and instead introduces a
new, more permissive, abstraction called Constraint Markov Chains
(CMCs). We introduce all the operators that make CMCs a complete
specification theory and discuss computability and complexity. We then
show how to extend CMCs by mixing them with Modal Transition Systems in
order to propose a specification theory for Probabilistic Automata. 
 Plus d'infos 

20120308  The Cost of Repairing Regular Specifications 
11:3012:30 Amphi 
What do you do if a computational object (e.g., a document, a program trace) fails a specification?
An obvious approach is to perform a "repair": modify the object minimally to get something that
satisfies the constraints. This approach has been extensively investigated in the database community
for relational integrity constraints, and in the AI community for propositional logics. Different modification
operators have been considered on the basis of the application scenarios. For instance, a repair of an
XML document usually consists of applying to the underlying tree structure a certain number of editing
operations such as relabelings, deletions, and insertions of nodes.
In this talk I will survey some results related to the worstcase cost of repairing documents between
regular specifications. Precisely, I will focus on the number of edits that are needed to get from a
document (i.e., a word or a tree) that satisfies a source specification (i.e., a regular language S) to
some document that satisfies a target specification (i.e., a regular language T). As this number may
well be unbounded, I will consider the problem of determining those pairs of languages (S,T) such
that one can get from any word/tree in S to a word/tree in T using a finite, uniformly bounded number
of editing operations. I will give effective characterizations of these pairs when S and T are given by
finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity
bounds for the corresponding problems.
The presentation is based on joint works with Michael Benedikt, Cristian Riveros, and Sławek Staworko.

 Plus d'infos 

20120216  Fixedword simulations and ranks 
11:3012:30 Amphi 
Minimization of Buchi automata is an intriguing topic in automata theory,
both for a theoretical understanding of automata over infinite words, and for practical applications.
Ideally, for a given language, one would like to find an automaton recognizing it with the least number of states.
Since exact minimization is computationally hard (e.g., PSPACEcomplete),
we concentrate on quotienting, which is a statespace reduction technique which works by "glueing together" certain states.
Which states can be merged is dictated by suitable preorders:
In this talk, we study fixedword simulations, which are simulationlike preorders sound for quotienting.
We show that fixedword simulations are coarser than previously studied simulationlike preorders,
by characterizing it with a natural (but nontrivial) ranking argument.
Our ranking construction is related to the socalled KupfermanVardi construction for complementing Buechi automata.

 Plus d'infos 

20120209  Abstract Domains for Automated Reasoning about ListManipulating Programs with Infinite Data 
11:3012:30 Salle 076, LaBRI, Rezdechaussée 
We introduce a framework based on abstract interpretation for reasoning about programs with lists carrying integer numerical data.
In this framework, abstract domains are used to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, and on the data stored in the lists.
We consider a domain where data is described by formulas in a universally quantified fragment of the firstorder logic over sequences, as well as a domain where data is described using constrains on the multisets of data in the lists.
Moreover, we provide powerful techniques for automatic validation of Hoaretriples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular interprocedural analysis. The approach has been implemented in a tool called CELIA and experimented successfully on a large benchmark of programs. 
 Plus d'infos 

20120126  Forest Automata for Verification of Heap Manipulation 
11:3012:30 076 
We consider verification of programs manipulating
dynamic linked data structures such as various forms of singly and doublylinked
lists or trees. We consider important properties for this kind of systems like
no nullpointer dereferences, absence of garbage, shape properties, etc. We
develop a verification method based on a novel use of tree automata to represent
heap configurations. A heap is split into several ``separated'' parts such that
each of them can be represented by a tree automaton. The automata can refer to
each other allowing the different parts of the heaps to mutually refer to their
boundaries. Moreover, we allow for a hierarchical representation of heaps by
allowing alphabets of the tree automata to contain other, nested tree automata.
Program instructions can be easily encoded as operations on our representation
structure. This allows verification of programs based on a symbolic statespace
exploration together with refinable abstraction within the socalled abstract
regular tree model checking. A motivation for the approach is to combine
advantages of automatabased approaches (higher generality and flexibility of
the abstraction) with some advantages of separationlogicbased approaches
(efficiency). We have implemented our approach and tested it successfully on
multiple nontrivial case studies.
(joint work with Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar) 
 Plus d'infos 

20120119  Optimizing Buechi Automata Inclusion Checking with Subsumption Preorders 
11:3012:30 076 
Inclusion checking is a central algorithmic problem in the theory of automata, with important applications, e.g., in formal methods.
The problem is PSPACEcomplete, thus under standard complexitytheoretic assumptions no deterministic algorithm with worst case polynomial time can be expected.
We optimize the socalled Ramseybased approach to inclusion checking.
In this approach, one explores a semigroup of exponential size for a counterexample to inclusion.
The exploration starts from a small set of generators, and all elements of the semigroup are progressively computed by composition.
On the way, a test operation is used to check for counterexamples.
The exploration stops if a counterexample is found; otherwise, all elements are generated.
Clearly, exhaustive exploration of the semigroup is in general infeasible, due to its exponential size.
We show how coarse simulationbased subsumption preorders between elements of the semigroup can be designed,
allowing one to prune away significant parts of the search space.
Subsumption allows us to solve inclusion checking for automata with thousand states, which was unthinkable before.
More details can be found on http://www.languageinclusion.org/. 
 Plus d'infos 

20120112  Robustness and Implementability of Timed Automata 
11:3012:30 076 
Timed automata are a well established model in realtime system design. They offer an automatatheoretic framework to design, verify and synthesize systems with timing constraints. The theory behind timed automata has been extensively studied and mature modelchecking tools are available. However, this model makes unrealistic assumptions on the system, such as the perfect continuity of clocks and instantaneous reaction times, which are not preserved in implementation even in digital hardware with arbitrary finite precisions. While these assumptions are natural in the design phase, they must be validated before implementing the system.
In this talk, I will first outline recent results on robustness analysis of timed automata, that is, deciding/computing an upper bound on the imprecisions under which a given property holds. I will then concentrate on the implementability problem, by presenting algorithms that render timed automata implementable: given a timed automaton, the goal is to construct a new timed automaton whose behavior under imprecisions is equivalent to the behavior of the first automaton.
Based on joint works with Patricia Bouyer, Kim Larsen, Nicolas Markey, Claus Thrane.

 Plus d'infos 

20111208  Propriétés de séparation dans la hiérarchie du mucalcul sur les arbres (3) 
11:3012:30 Salle 076, LaBRI, Rezdechaussée 
Description: Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mucalcul sur les arbres. Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que EC est aussi dans Gamma, et A inclus dans C, B inclus dans EC. Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie. A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009] Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2). Auparavant, le problème de la séparation dans la hiérarchie des omegalangages reconnus par des automates __déterministes__ à parité sera entièrement traité. 
 Plus d'infos 

20111201  Propriétés de séparation dans la hiérarchie du mucalcul sur les arbres (2) 
11:3012:30 076 

 Plus d'infos 

20111124  Propriétés de séparation dans la hiérarchie du mucalcul sur les arbres 
11:3012:30 076 
Description:
Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mucalcul sur les arbres.
Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que EC est aussi dans Gamma, et A inclus dans C, B inclus dans EC.
Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie.
A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009]
Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2).
Auparavant, le problème de la séparation dans la hiérarchie des omegalangages reconnus par des automates __déterministes__ à parité sera entièrement traité.

 Plus d'infos 

20111117  Visibly Pushdown Transducers: Functionality, kValuedness and Streamability 
11:3012:30 075 
Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly pushdown languages form a robust subclass of contextfree languages. Along the same line, we show that word transductions defined by VPTs enjoy strong properties, in contrast to PTs. In particular, functionality is decidable in PTIME, kvaluedness is in NPTIME and equivalence of (nondeterministic) functional VPTs is EXPTIMEC.
In a second part, we study the problem of evaluating in streaming (i.e. in a single lefttoright pass) the transduction realized by a functional VPT. A transduction is said to be height bounded memory (HBM) if it can be evaluated with a memory that depends only on the height of the input word (and not on its length). We show that it is decidable in coNTPTime whether such a transduction is HBM. In this case, the required amount of memory may depend exponentially on the height of the input word. We exhibit a sufficient, decidable condition for a VPT to be evaluated with a memory that depends quadratically on the height of the input word. This condition defines a class of transductions that strictly contains all determinizable VPTs.
This talk is based on the two following papers :
Properties of Visibly Pushdown Transducers. Emmanuel Filiot, JeanFrançois Raskin, PierreAlain Reynier Reynier, Frédéric Servais and JeanMarc Talbot. In Proc. MFCS’10.
Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, PierreAlain Reynier and Frédéric Servais. In Proc. FSTTCS’11. 
 Plus d'infos 

20111110  Vpraxis et évolution d'application internet 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
Pratiquement toutes les applications s’exécutent aujourd’hui sur Internet,
quel que soit leur usage et quel que soit leur domaine. Une application qui
s’exécute sur internet fait partie d’un réel écosystème d’applications. Elle
utilise et propose des ressources (donnée et/ou traitement) qui forment
l’écosystème. Ces ressources, qui étaient il y a quelques années encore du
simple texte, des images ou des vidéos, sont aujourd’hui beaucoup plus
complexes, tels que des données sémantiques ou des services web par exemple.
Cette complexité croissante fait que le développement des applications
internet, et donc de l’écosystème, ne peut plus se faire par des équipes
bien structurées, maîtres des artefacts logiciels qu’elles produisent et
appliquant des cycles de développement traditionnels. Nous soutenons que le
développement d’application internet doit nécessairement prendre en
considération le concept d’écosystème logiciel. Les applications de demain
seront de plus en plus dépendantes de leur écosystème. Sans une forte
réactivité de développement face aux évolutions de l’écosystème, une
application deviendra vite dépassée et donc inutilisable ou extrêmement
couteuse en maintenance.
Le thème Sphere du LaBRI (http://sphere.labri.fr) développe l’approche
VPraxis qui vise à contrôler l’évolution des applications internet. Notre
objectif est de modéliser les histoires des différents composants des
applications internet afin de contrôler leur interdépendance. Cette
présentation portera sur VPraxis et montrera le modèle qu’il propose afin de
modéliser l’évolution d’un écosystème logiciel. 
 Plus d'infos 

20111103  Controlling distributed systems 
11:3012:30 076 
We consider the problem of controlling distributed automata that cooperate via
shared variables (rendezvous). The setting corresponds to the framework of
Ramadge and Wonham, where certain actions (controllable ones) can be forbidden
by the local controller. Although the general question is still open, we
show that the problem is decidable on acyclic architectures, albeit of
nonelementary complexity.
Joint work with B. Genest, H. Gimbert and I. Walukiewicz. 
 Plus d'infos 

20111013  Weighted Expressions and Pebble Automata over Nested Words 
11:3012:30 L'Amphi 
We introduce a calculus over nested words (or equivalently, trees) to express quantitative properties of XML documents or recursive programs. Our weighted expressions borrow purely logical constructs from XPath, but they also involve rational arithmetic expressions. The latter allow us to perform computations in an arbitrary (commutative) semiring. For instance, one can count how often a given entry occurs in an XML document, or compute the memory consumption of a program execution. We characterize a fragment of weighted expressions in terms of a new class of weighted automata. In the spirit of treewalking automata, our device traverses a nested word along its edges and may place pebbles during a traversal.
After proving this expressiveness result, we give a list of interesting decision or computation problems, with some hints on their resolution, and a set of possible applications of these problems, depending of the chosen semiring. 
 Plus d'infos 

20111006  Model Checking the Quantitative muCalculus on Infinite Transition Systems 
11:3012:30 076 
We consider the modelchecking problem for a quantitative
extension of the modal mucalculus on two classes of infinite
quantitative transition systems. The first class, initialized linear
hybrid systems, is motivated by verification of systems which
exhibit continuous dynamics. We show that the value of a formula
of the quantitative mucalculus can be approximated with arbitrary
precision on initialized linear hybrid systems. The other class,
increasing tree rewriting systems, is motivated by efforts to allow
counting formulas in discrete verification. On such systems, we
show that the value of a quantitative formula can be computed
exactly. For both these classes of systems, the problem in the end
reduces to solving a new form of parity games with counters. 
 Plus d'infos 

20110929  Quantitative Verification and Synthesis 
11:3012:30 076 
Quantitative constraints have been successfully used to state and
analyze nonfunctional properties such as energy consumption,
performance, or reliability. Functional properties are typically
viewed in a purely qualitative sense. Desired properties are written
in temporal languages and the outcome of verification is a simple Yes
or No answer stating that a system satisfies or does not satisfy the
desired property. We believe that this black and white view is
insufficient both for verification and for synthesis. Instead, we
propose that specifications should have a quantitative aspect.
Our recent research shows that quantitative techniques give new
insights into qualitative specifications. For instance,
averagereward properties allow us to express properties like default
behavior or preference relations between implementations that all
satisfy the functional property. These additional properties are
particularly useful in a synthesis setting, where we aim to
automatically construct a system that satisfies the specification,
because they allow us to guide the synthesis process making the outcome
of synthesis more predictable.
In this talk I will give an overview of
(1) how classical specification can be augmented with quantitative constraints,
(2) list different quantitative constraints that arise in this way, and
(3) show how to verify and synthesize systems that satisfied the
initial specification and optimize such quantitative constraints.
This is joint work with R. Bloem, K. Chatterjee, K. Greimel, T. Henzinger,
A. Radhakrishna, R. Singh, and C. von Essen.

 Plus d'infos 

20110922  Model checking vector addition systems with one zerotest 
11:3012:30 076 
We design a variation of the KarpMiller algorithm to compute a
finite representation of the cover (i.e., the downward closure of
the reachability set) of a vector addition system with one
zerotest. This algorithm yields decision procedures for several
problems on these systems, open until now, such as
placeboundedness or LTL modelchecking.
The proof techniques to handle the zerotest are based on two new
notions of cover: the refined and the filtered cover. The refined
cover is hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality
of two refined covers is undecidable, even for usual Vector
Addition Systems (with no zerotest), but the refined cover of a
Vector Addition System is a recursive set. The second notion of
cover, called the filtered cover, is the central tool of our
algorithms. It inherits properties of the classical cover, and in
particular, one can effectively compute a finite representation
of this set, even for Vector Addition Systems with one zerotest. 
 Plus d'infos 

20110630  A game approach to determinize timed automata 
11:3012:30 Salle 076 
Timed automata are frequently used to model realtime systems.
Their determinization is a key issue for several validation problems.
However, not all timed automata can be determinized, and determinizability
itself is undecidable. In this talk, we will present a gamebased algorithm
which, given a timed automaton,
tries to produce a languageequivalent deterministic timed automaton,
otherwise a deterministic overapproximation. Our method subsumes two
recent contributions: it is at once more general than a recent determinization
procedure and more precise than the existing overapproximation algorithm.Then, we will explain how this method can be adapted to be usefull for test generation.
This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers will be presented at FoSSaCs'11 and TACAS'11. 
 Plus d'infos 

20110623  Génération de séquences de pannes de modèles AltaRica 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
Les analyses de sûreté visent à réduire la probabilité
d'occurrence d'incidents critiques dans un système. Un des moyens
d'évaluer cette probabilité est de calculer les principales
combinaisons de pannes des composants du système qui engendrent
l'incident critique étudié. Cet ensemble de combinaisons permet
ensuite d'évaluer, éventuellement de manière pessimiste, la
probabilité de défaillance du système.
Lors de ce séminaire je présenterai comment nous avons utilisé de
vieilles recettes pour calculer l'ensemble des séquences critiques
d'un système modélisé en langage AltaRica.
Ces algorithmes sont désormais disponibles dans ARC, le modelchecker
pour AltaRica.
La présentation sera en français.

 Plus d'infos 

20110609  Vers un modèle de contrôle tempsréels, hiérarchique, concurrent et réactifs 
11:3012:30 076 
A priori, tout et dans le titre, les mots clés qui le composent et les questions qui en découlent. Quelles peuvent être les motivations pour définir de tels contrôleurs ? Comment ordonner les paradigmes (parfois transversaux) de modélisation qu'ils doivent inclure ? Que saiton déjà de ce type de contrôleurs ? Comment le modèle qui s'impose peutil être relié aux notions déjà existantes d'automates d'états finis, d'automates synchrones, d'automates à piles, de diagrammes d'états (statecharts), d'automates temps réels, de modèles de flux synchrones, etc....
Dans cet exposé, à travers la définition d'un modèle de contrôleurs qui tente d'intégrer tout les paradigmes évoqués, je tâcherais d'illustrer par l'exemple quelques éléments de réponses à ces questions en m'appuyant notamment sur la problématique de "la modélisation à visée applicative" qui agit comme un filtre à concepts selon le principe "si ça marche, ça doit avoir des propriétés mathématiques intéressantes".

 Plus d'infos 

20110519  Power of Randomization in Finite State Monitoring 
11:3012:30 076 
We introduce the model of finite state probabilistic monitors (FPM), which are finite state automata on infinite strings that have probabilistic transitions and an absorbing reject state. FPMs are a natural automata model that can be seen as either randomized runtime monitoring algorithms or as models of open, probabilistic reactive systems that can fail. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of languages recognized by FPMs. We also study the emptiness and universality problems for such automata and give exact complexity bounds for these problems. Joint work with A. Prasad Sistla and Mahesh Viswanathan. 
 Plus d'infos 

20110512  Hybrid syntactic/semantic computer virus detection scheme 
11:3012:30 076 
The detection problem in computer virology is known to be undecidable. Nonetheless, a large body of work is still devoted to the subject. We will present the state of the art on detection schemes: the syntactic and semantic detection schemes.
Subsequently, we will introduce a new hybrid syntactic/semantic detection scheme, where the extraction of the virus signature is performed through abstract interpretation techniques while virus detection is let to efficient syntactic detectors. We will present a new abstract domain that is able to automatically extract the signature of a polymorphic virus as a context free grammar. Preliminary results on some real polymorphic virus samples will also be shown. 
 Plus d'infos 

20110505  Computing Optimal Strategies for Markov Decision Processes with Parity and PositiveAverage Conditions 
11:3012:30 076 
We study Markov decision processes (oneplayer stochastic games)
equipped with parity and positiveaverage conditions.
In these games, the goal of the player is to maximize the probability that both the
parity and the positiveaverage conditions are fulfilled.
We show that the values of these games are computable in polynomial time.
We also show that optimal strategies exist, require only finite memory and can be effectively computed.
Joint work with Hugo Gimbert and Soumya Paul. 
 Plus d'infos 

20110428  A lazy reachability algorithm for timed automata 
11:3012:30 076 
We consider the classic reachability problem for timed automata:
given an automaton, decide if there exists a path from its initial state
to a given target state. The standard solution to this problem involves
computing the *zone graph* of the automaton, which in principle could be
infinite. In order to make the graph finite, zones are approximated using
an extrapolation operator. For reasons of efficiency it is required that an
extrapolation of a zone is always a zone; and in particular that it is *convex*.
We propose a new solution to the reachability problem that uses no
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the
*region closure* of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.
The structure of this new algorithm permits to calculate
approximating parameters onthefly during exploration of the zone
graph, as opposed to the current methods which do it by a static
analysis of the automaton prior to the exploration. This allows for
further improvements in the algorithm. Promising experimental results
are presented.
Joint work with Frédéric Herbreteau, Dileep Kini, Igor Walukiewicz

 Plus d'infos 

20110407  Contraintes sur le temps logique dans la conception de systemes embarques 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
Je presenterai un langage de contrainte permettant d'exprimer des contraintes chronologiques et causales
sur les evenements du systeme (horloges logiques) et certains de mes travaux en cours sur ce langage: d'une
part la comparaison de ce langage avec la logique temporelle lineaire et d'autre part l'extension de ce langage
avec un systeme de priorites. 
 Plus d'infos 

20110217  Unfoldings of contextual Petri nets 
07:0007:00 Salle 076, LaBRI, Rezdechaussée 
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finitestate) Petri nets, which can be used for verification purposes.
Contextual nets are a generalisation of Petri nets suited to model systems with readonly access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan's construction to a suitable encoding of the contextual net into an ordinary net.
However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. We propose a an unfolding algorithm that works for arbitrary semiweighted, bounded contextual nets.
The talk is based on joint work with Paolo Baldan, Andrea Corradini, and Barbara Koenig. 
 Plus d'infos 

20110203  Global Model Checking of Ordered MultiPushdown Systems 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
In this talk, we address the verification problem of ordered multipushdown systems, a multistack extension of pushdown systems that comes with a constraint on stack operations: a pop can only be performed on the first nonempty stack (which implies that we assume a linear ordering on the collection of stacks). First, we show that for an ordered multipushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multipushdown system that satisfy a given wregular property (expressible in lineartime temporal logics or the lineartime µcalculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of wregular properties for ordered multipushdown systems (matching its lowerbound).

 Plus d'infos 

20101216  Energy and MeanPayoff Games 
11:3012:30 Salle 076, LaBRI, Rezdechaussée 
We consider game models for the design of reactive systems
working in ressourceconstrained environments.
In meanpayoff games, the ressource usage is computed as
the longrun average ressource level.
In energy games, the ressource usage is the intial amount
of ressource necessary to maintain the ressource level positive.
The resource can be memory, battery, or network usage for example.
While meanpayoff games are a wellestablished model in game theory
and computer science, energyy games have received attention only recently.
The talk reviews recent results about these games and their relationship.
Although they differ very basically in their definition,
it is known that energy and meanpayoff games are equivalent for
the simple decision problem of existence of a winning strategy.
This observation provides new complexity results for solving
meanpayoff games, and new insights for meanpayoff games combined
with other conditions such as fairness, imperfect information,
or multiressource systems, though the strong equivalence with
energy games usually breaks in such cases.

 Plus d'infos 

20101209  What Can You Verify and Enforce at Runtime ? 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
Runtime verification is an effective technique to ensure at execution time that a system meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together untrusted software components. In runtime verification, a run of the system under scrutiny is analyzed incrementally using a decision procedure: a monitor. This monitor may be generated from a userprovided high level specification (e.g. a temporal property, an automaton). Runtime enforcement is an extension of runtime verification aiming to circumvent property violations. In runtime enforcement the monitors watch the current execution sequence and modify the execution sequence of the underlying program whenever it deviates from the desired property. More than simply halting an underlying program, some enforcement mechanisms can also ``suppress'' (i.e. freeze) and ``insert'' (frozen) actions in the current execution sequence. Runtime verification and enforcement have
proved to be effective techniques to achieve software reliability.
The questions we consider in this talk are the following: what are the classes of properties that can be verified and enforced at runtime, and is there a difference between the techniques we are interested in? These questions are not new, but we propose here to address them within a unified framework: the SafetyProgress classification of properties introduced by Manna and Pnueli.
In this talk, we start first by customizing the SafetyProgress classification in a runtime verification and enforcement context. Then we revisit the existing classical definition of monitorability, and
characterize the set of monitorable properties according to this definition. Then, we parameterize this definition according to the truthdomain under consideration. Moreover, we introduce a new definition of monitorability based on distinguishability of ``good'' and ``bad'' execution sequences. This definition is weaker than the classical one, but we believe that it better corresponds to practical needs and tool implementations. Furthermore, we characterize the set of enforceable properties in a way that is independent from any enforcement mechanism. A consequence is that the proposed set of enforceable properties is an upper bound of any enforcement mechanism.
This is joint work with Pr. JeanClaude Fernandez and Dr. Laurent Mounier from Vérimag (Grenoble).

 Plus d'infos 

20101202  Efficient Emptiness Check for Timed Büchi Automata 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
The Büchi nonemptiness problem for timed automata concerns deciding
if a given automaton has an infinite nonZeno run satisfying the
Büchi accepting condition. The standard solution to this problem involves
adding an auxiliary clock to take care of the nonZenoness. In this talk, we
show that this simple transformation may sometimes result in an
exponential blowup. Then, we propose a method avoiding this blowup.
However, in many cases, no extra construction is needed to ascertain
nonZenoness. Hence, we finally present an onthefly algorithm for the
nonemptiness problem, using an efficient nonZenoness construction
only when required. 
 Plus d'infos 

20101021  The complexity of Nash Equilibria in Reward Games 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
We study the complexity of Nash equilibria in games with limitaverage objectives. While an arbitrary Nash equilibrium of such a game can be found in polynomial space, we show that deciding whether a game has an equilibrium whose payoff meets certain constraints is, in general, undecidable. A more refined analysis takes into account the complexity of the strategies that realise the equilibrium. While for stochastic games, the above problem is undecidable for both pure and randomised strategies, the problem becomes decidable when one looks for a purestrategy equilibrium in a nonstochastic game. 
 Plus d'infos 

20101014  Expected ReachabilityTime Games 
11:3012:45 Salle 178, LaBRI 
In an expected reachabilitytime game (ERTG) two players, Min and
Max, move a token along the transitions of a probabilistic timed automaton,
so as to minimise and maximise, respectively, the expected time to reach a
target. We show that ERTGs are positionally determined. Using the boundary
region graph abstraction, and a generalisation of Asarin and Maler’s
simple function,
we show that the decision problems related to computing the value of ERTGs
are decidable and their complexity is in NEXPTIME ∩ coNEXPTIME. 
 Plus d'infos 

20101007  Traitement et programmation synchrone des flux musicaux 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
Notre exposé repose sur le couplage de deux thématiques souvent
considérées comme distinctes, mais qui sont indissociables dans un
contexte musical :
(1) Traitement et reconnaissance temps réel des flux sonores
(2) Langage de programmation synchrone pour l'informatique musicale
Ce couplage émerge de la pratique musicale et compositionnelle,
faisant appel aux formalismes d'écriture synchrone et concurrente,
comme un système réactif aux jeux des musiciens en temps réel. Le
premier volet nous ramène aux problèmes des représentations
hétérogènes propres à l'information musicale avec des solutions
proposées venant de la littérature émergeant de la géométrie de
l'information. Le deuxième au temps hétérogène dans écriture des
processus musicaux et des systèmes hybrides. L'incarnation actuelle de
ces deux thématiques est la recherche et développement autour de
l'environnement Antescofo, un jeune langage de programmation synchrone
pour la composition musicale couplée avec la reconnaissance des
paramètres musicaux lors d'une performance temps réel.
liens: http://imtr.ircam.fr/imtr/Score_Following
http://imtr.ircam.fr/imtr/Music_Information_Geometry 
 Plus d'infos 

20100930  The Vector Addition System Reachability Problem 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical KosarajuLambertMayrSacerdoteTenney decomposition. Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of nonreachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semialgorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the nonreachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the classical KosarajuLambertMayrSacerdoteTenney decomposition. The new proof is based on the notion of productive sequences inspired from Hauschildt that directly provides the existence of Presburger inductive invariants. 
 Plus d'infos 

20100916  Distributed Timed Automata with Independently Evolving Clocks 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
We propose a model of distributed timed systems where each component is a
timed automaton with a set of local clocks that evolve at a rate independent
of the clocks of the other components. A clock can be read by any component in
the system, but it can only be reset by the automaton it belongs to. Since we
have unrelated time values on different components, we are interested in the
underlying untimed behaviors of these distributed timed automata rather than
their timed behaviors. Thus, the clocks (and time itself) are synchronization
tools rather than being a part of the observation.
There are two natural semantics for such systems. The universal semantics
captures behaviors that hold under any choice of clock rates for the
individual components. Thus, it can be considered as an underapproximation
of the actual behavior. This is a natural choice when checking that a system
always satisfies a positive specification. However, to check if a system
avoids a negative specification, it is better to use the existential
semantics (an overapproximation of the actual system behavior): the set of
behaviors that the system can possibly exhibit under some choice of clock
rates.
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness or
universality turns out to be undecidable, which is shown by a reduction from
Post’s correspondence problem. This result is further strengthened to some
bounded cases, where we have restrictions on the relative time rates such as
fixed slopes.
As an alternative to the universal semantics, we propose a gamebased
reactive semantics that allows us to check positive specifications and yet
describes a regular set of behaviors.
This is joint work with S. Akshay, Paul Gastin, Madhavan Mukund, and
K. Narayan Kumar. 
 Plus d'infos 

20100701  Solving Simple Stochastic Tail Games 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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 perfectinformation stochastic tail games, in particular the existence of optimal strategies. We apply these results to games whose winning conditions are boolean combinations of meanpayoff and Buchi conditions. 
 Plus d'infos 

20100603  A formal framework for social Networking 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
The talk presents Popar, an ongoing project that aims at using several formal
methods tools and techniques to develop a fullfledged socialnetwork service implementing stipulated policies. The system includes a B method definition for social networking, modelling socialnetwork content, privacy policies, socialnetworks friendship relations, and how these relations affect users' policies. This core is expected to be extended by thirdparty plugins in such a way that adherence to system policies is guaranteed by formal techniques such as proofcarrying code. 
 Plus d'infos 

20100527  Static analysis of positional and non positional properties of arrays 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
(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: onedimensional
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.

 Plus d'infos 

20100520  Implicit Real Vector Automata 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
This work addresses the efficient handling of nonconvex 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 nonconvex
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 JeanFrançois Degbomont 
 Plus d'infos 

20100422  Datalogbased Program Analysis with BES and RWL 
10:0011:15 Salle 050, LaBRI, Rezdechaussée 
In this talk, we present two powerful, fully automated methods to
evaluate Datalog queries in the context of objectoriented 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 lineartime complexity; the second approach
transforms Datalog programs into Rewriting Logic and produces an
efficient rewrite system exploiting the main features of the
highlevel 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 realworld
Datalogbased analyses. 
 Plus d'infos 

20100415  Volume and entropy of regular timed languages 
11:3012:30 Salle 076, LaBRI, Rezdechaussée 
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 socalled “1 1/2clock" automata, and two numerical ones: one using techniques of functional analysis, another based on discretization.
(joint work with Aldric Degorre, Concur'09+ Formats'09) 
 Plus d'infos 

20100401  When ModelChecking Freeze LTL over Counter Machines Becomes Decidable 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
We study the decidability status of modelchecking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (onecounter machines, reversalbounded counter machines, vector additions systems with states, ﬂat 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 classiﬁcation for the modelchecking 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 ﬂat 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).

 Plus d'infos 

20100311  Static Analysis of x86 Executables 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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.

 Plus d'infos 

20100225  Craig Interpolation for QuantifierFree Presburger Arithmetic 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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 quantifierfree
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.

 Plus d'infos 

20100218  On nondeterministic automata for Presburger arithmetic. 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
A wellknown decision procedure for Presburger arithmetic (PA)
uses deterministic finitestate automata. While the complexity
of the decision procedure for PA based on quantifier elimination
is known (tripleexponential), the exact complexity of the
automatabased procedure was unknown. We show that it is tripleexponential
as well by analysing the structure of the nondeterministic automata
obtained during the construction building on results from Klaedtke.
Furthermore, we analyse the sizes of deterministic and nondeterministic
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 nondeterministic automata
called residual finitestate automata introduced by Denis, Lemay and Terlutte. 
 Plus d'infos 

20100211  Towards a Computational Modeling of an Heterogeneous System for Interactive Musical Scores 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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 Nondeterministic 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. 
 Plus d'infos 

20100204  Recurrence and Transience for Probabilistic Automata 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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 nonhomogenes.

 Plus d'infos 

20100114  L'approche SAT pour lpour automates temporisés avec étapes parallèles 
11:3012:45 Salle 076, LaBRI, Rezdechaussée 
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 contreintuitives, parce que le temps, représenté par des nombres réels, est un ordre total.
D'un autre coté, pour des systèmes nontemporisé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.

 Plus d'infos 

20100107  Un Langage Synchrone pour les Systèmes Embarqués Critiques Temps Réel 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
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ôleCommande. 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 multirythme 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.

 Plus d'infos 

20091217  Automatic Synthesis of Robust and Optimal Controllers  An Industrial Case Study 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
In this talk, we show how to apply recent tools for the automatic synthesis of robust and nearoptimal 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 veriﬁcation, and SIMULINK for simulation, in a complementary way.

 Plus d'infos 

20091210  Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents. 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
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 GoubaultLarrecq 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). 
 Plus d'infos 

20091203  Alternatingtime Temporal Logic: Expressivity, Complexity, Extensions 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
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 boundedmemory 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 modelchecking
for these logics.
Joint work with: Th. Brihaye, A.. Da Costa, N. Markey. 
 Plus d'infos 

20091126  Games on Infinite Domains and Approximation 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
I'll give an overview of research I have been
doing over the last few years in semantic models
of mixed nondeterministic and probabilistic choice.
One can also see this as models for twoplayer
turnbased (stochastic) games, where the state space
X is infinite. The approach is topological and
domaintheoretical. 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 capacitybased
models, prevision models, simulation and (if time
permits) simulation (hemi)metrics. 
 Plus d'infos 

20091112  Reachability Analysis of Communicating Pushdown Systems 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
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 nonempty 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 
 Plus d'infos 

20091105  On the Verification Problem for Weak Memory Models 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
We address the verification problem of finitestate concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multiprocessor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performancecritical system services employing lockfree 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 wellknown 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) 
 Plus d'infos 

20091022  Control of Infinite Symbolic Transition Systems under Partial Observation 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
We propose algorithms for the synthesis of statefeedback
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 overapproximations 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. 
 Plus d'infos 

20090929  Parity Games on Multistack Systems 
11:0012:15 Salle 075, LaBRI, Rezdechaussée 
In this talk we present higher order multistack
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. 
 Plus d'infos 

20090618  Edition Collaborative d'arbres XML 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
L'edition collaborative consiste à travailler sur un document commun de
manière distribuée et concurrente. Un problème essentiel est d'assurer la
cohérence du processus, car des opérations concurrentes peuvent etre
conflictuelles (ajouter ou supprimer une lettre à la meme position). De
nombreux systèmes reposent sur une centralisation implicite (par des
timestamps par exemple) ou explicite (existence d'un site maitre comme avec
svn). L'approche Pair à Pair ne permet pas cette centralisation, et à tout
moment de nouveaux sites peuvent rejoindre le processus d'édition. Dans ce
cadre l'approche optimiste considère que toutes les opérations doivent etre
prises en compte, et utilise une approche transformationnelle pour intégrer
les opérations concurrentes: au lieu d'effectuer l'opération o2 concurrente à
o1, on effectue une opération modifiée IT(o1,o2). Quand l'opérateur de
transformation IT satisfait deux propriétés TP1 et TP2, il existe un
algorithme qui assure la convergence du processus (chaque site a la meme
copie du document à la fin du processus). Pour le cas des mots aucun des
jeux
d'opérations et des transformations proposées ne satisfont ces propriétés et
des contreexemples montrent qu'ils n'assurent pas la convergence (cf thèse
d'A. Imine). Dans cet exposé nous nous intéressons à l'édition des arbres
étiquetés nonordonnés avec des opérations d'ajout, suppression ou
réétiquetage. Le premier résultat est de montrer qu'il n'existe pas de
transformation satisfaisant TP1 et TP2 dans ce cadre. Le deuxième résultat
consiste à étendre la structure de données par des informations fournies
naturellement par le processus d'édition qui garantissent l'unicité des
étiquettes et de montrer que les propriétés TP1 et TP2 sont satisfaites ce
qui autorise l'edition collaborative sur cette structure. Finalement, nous
montrons comment garder ces propriétés en ajoutant une opération de
déplacement de sousarbres à condition de modifier la structure de donnée en
ajoutant une mémoire. Nous terminerons en discutant le cas des arbres
ordonnés et le problème du undo (annulation d'une opération).
Travail en commun avec Stéphane Martin.

 Plus d'infos 

20090604  Contrôleurs non déterministes de processus non déterministes 
11:0012:15 Salle 076 
Arnold, Vincent, Walukiewicz en 2003, puis Briand en 2006, on tracé une frontière entre les cas où la synthèse (centralisée ou décentralisée) de contrôleurs déterministes de processus déterministes est effective et ceux où elle est indécidable, lorsque les contrôleurs et le système contrôlé sont soumis à des contraintes d'inobservabilité et d'indiscernabilité exprimables dans un mucalcul modal étendu.
En 2008 Arnold et Walukiewicz ont étendu ces résultats au cas où les contrôleurs et les processus ne sont pas nécessairement déterministes.
Ce sont ces extensions qui seront présentées. 
 Plus d'infos 

20090528  When are Timed Automata Determinizable? 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
We describe an abstract procedure which, given a timed automaton, produces a languageequivalent deterministic infinite timed tree. Under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition we exhibit is satisfied by several subclasses of timed automata, some of them were known to be determinizable (eventclock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly nonZeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACEcomplete for strongly nonZeno timed automata).
This is a joint work with C. Baier, P. Bouyer and T. Brihaye. 
 Plus d'infos 

20090514  What's decidable for Asynchronous Programs ? 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
An asynchronous or "eventdriven'' program is one that contains
procedure calls which are not directly executed from the call site,
but stored and executed later by an external scheduler.
By providing a lowoverhead way to manage concurrent interactions,
asynchronous programs form the core of many server programs, embedded
systems, and popular programming styles for the web (Ajax).
Unfortunately, such programs can be hard to write and maintain as
sequential control flow needs to be split into several disjoint
handlers.
They are a challenge for static analysis tools as they are infinite
state: both the program stack and the number of outstanding
asynchronous requests may be unbounded.
We show that safety and liveness properties can be checked effectively
for the class of Boolean asynchronous programs, thus enabling
automatic static techniques to check for correctness or for errors. 
 Plus d'infos 

20090507  Well Structured Transition Systems everywhere and everytime ! 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
The theory of Well Structured Transition Systems provides the good structure for computing a finite basis of the set of predecessors of the upward closure of a finite set of states. We address here the dual problem which is to compute a finite representation of the set of successors of the downward closure of a finite set of states (called the cover). This last problem is, a priori, more difficult because in general, the cover has no finite basis.
It is possible to complete any wellordered set to obtain a cpo in which every downward closed set has a finite representation.
We then define the framework of Complete Well Structured Transition Systems and we propose a simple and a conceptual procedure for computing the covering set and the covering graph. This procedure terminates more often than the generalized KarpMiller tree procedure when applied on extended Petri nets and lossy channel systems.

 Plus d'infos 

20090430  Algorithmes de théorie des jeux en analyse statique de programme 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
Nous ferons un tour d’horizon de résultats portant sur la
correspondance entre les équations de point fixe rencontrées en
analyse statique de programme par interprétation abstraite et celles
qui apparaissent dans l’approche par programmation dynamique des
jeux répétés à somme nulle. Cette correspondance permet en
particulier d’appliquer des algorithmes de type itération sur les
politiques afin de déterminer des invariants de nature numérique sur
le programme analysé (par exemple des invariants polyédraux).
Cependant, deux difficultés apparaissent. La première, très
inhabituelle, est que les jeux considérés peuvent avoir un taux
d’escompte négatif (l’ensemble des points fixes n’est plus alors
nécessairement connexe). Une seconde difficulté est que l’algorithme
d’itération sur les politiques le plus simple peut terminer avec un
point fixe non minimal, alors que c’est le point fixe minimal qui
fournit le meilleur invariant. Nous montrons cependant comment
utiliser des techniques de théorie de PerronFrobenius nonlinéaire
(rayons spectraux, calcul semidifférentiel) pour obtenir toujours
le plus petit point fixe, à condition que le taux d’escompte ne soit
pas négatif. Ces résultats sont issus d’une série de travaux avec
Éric Goubault, Matthieu Martel, Sylvie Putot, Alexandru Costan,
Ankur Taly, et Assale Adjé. 
 Plus d'infos 

20090423  Robustesse environnementale dans les réseaux d'automates à seuil : théorie et application en biologie. 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
Nous allons nous intéresser à l'influence des conditions de bords dans les réseaux d'automates booléens à seuil, objets mathématiques pertinents pour la modélisation des réseaux de régulation biologique. L'objectif est de montrer que les bords (qui peuvent représenter des potentiels électriques externes dans les réseaux de neurones et des flux d'hormones ou encore des microARN dans les réseaux de régulation génétique) sont des éléments qui peuvent changer radicalement le comportement dynamique de tels réseaux, aussi bien dans le cas de réseaux théoriques tels que les automates cellulaires que dans celui des réseaux biologiques réels. La démarche scientifique proposée est de se focaliser dans un premier temps sur des réseaux dits "parfaits", énormément contraints sur la nature des interactions et la topologie de manière à obtenir des résultats théoriques sur Z^d. Ensuite, en relâchant progressivement les contraintes, nous mettrons en évidence, par simulation, des domaines d'influence des conditions de bord pour des réseaux plus complexes sur Z2. Enfin, pour faire un pas de plus en direction de la biologie, nous verrons que les conditions de bord jouent un rôle dans les réseaux réels. Nous présenterons alors une méthode générique d'étude de la robustesse environnementale des systèmes dynamiques réels (basée sur la notion de bassin d'attraction). Nous terminerons en présentant les résultats que cette méthode permet d'obtenir, dans le contexte des réseaux de régulation génétique, à propos de la morphogenèse florale de la plante Arabidopsis thaliana. 
 Plus d'infos 

20090402  Extrapol, des systèmes de types dépendants à la sécurité système 
11:0012:15

Dans le domaine de la sécurité, l'un des problèmes récurrents est celui
de déterminer quels effets l'exécution d'un programme peut avoir sur le
système qui l'héberge. Ces effets peuvent prendre la forme de
modification de fichiers, de communication avec des processus,
d'installation de services web... Dans d'autres cas, c'est
l'installation d'un programme ou d'une bibliothèque qui pourra donner à
d'autres programmes des points d'entrée pour avoir ce même genre
d'effets, de manière potentiellement accidentelle et potentiellement
malicieuse.
Le plus fréquemment, pour détecter les effets d'un programme ou les
points d'entrée d'une bibliothèque, l'administrateur d'un système a le
choix entre des outils dynamiques (bacs à sable) et des outils
postmortem (analyse de trace)  mais pas réellement d'outils d'analyse
statique.
Au cours de notre exposé, nous présenterons une technique d'analyse
statique pour les propriétés de sécurité de code source écrit en langage
C. Nous partirons du modèle de sécurité SELinux, tel qu'intégré à de
nombreuses distributions de Linux, et nous avancerons progressivement
jusqu'à une notion de types avec effets et de types dépendants. La
technique a été implantée en OCaml, sous la forme d'un outil de
diagnostic automatique, Extrapol. 
 Plus d'infos 

20090319  AltaRica : passé, présent et futur. 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
AltaRica est un formalisme qui a été défini pour la description fonctionnelle
et dysfonctionnelle des systèmes industriels critiques. Depuis la première
version du langage en 2000, différentes variantes et outils associés ont été
proposés. Aujourd'hui, ces outils sont réellement utilisés de façon
productive dans certaines entreprises.
Dans la première partie de l'exposé, je présenterai le formalisme initial et
sa sémantique. Je donnerais ensuite les diverses évolutions et les raisons
pour lesquelles elles ont été introduites.
La dernière partie de l'exposé listera des travaux futurs possibles dans le
cadre "AltaRica, un formalisme d'aide à la conception sûre de systèmes
critiques". 
 Plus d'infos 

20090312  How to get decidability of distributed synthesis ? 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
The distributed synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification.
Our general aim is to define natural conditions under which synthesis or control are decidable for distributed systems. It is known that these problems are undecidable for most synchronous systems. So in this work we study asynchronous systems which communicate through signals  actions that are immediately received by the target process. Another main cause of undecidability comes from the specifications. Here, we consider emph{external} specifications over emph{partial orders}. External means that specifications only relate input and output actions from and to the environment and not internal signals exchanged by processes. We also ask for some natural closure properties of the specification. We obtain decidability for the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures. 
 Plus d'infos 

20090305  Modal Logics with Presburger constraints 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
In this talk, we present an extended modal logic EML with regularity constraints and
full Presburger constraints on the number of children that generalize graded modalities,
also known as number restrictions in description logics.
We show that the satisfiability problem for EML can be solved with polynomial space.
This extends a wellknown and nontrivial PSPACE upper bound for graded modal logic.
Furthermore, we provide a detailed comparison with logics that contain
Presburger constraints and that are dedicated to query XML documents. As an
application, we provide a reduction from Sheaves logic SL into EML,
which allows to improve the best known upper bound for SL satisfiability.
This is a joint work with Denis Lugiez (LIF, Marseille, France).

 Plus d'infos 

20090212  Spécification et Contrôle des Systèmes tempsréel faibles 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
Nous introduisons la Logique $WT_mu$ pour décrire les propriétés des systèmes tempsréel faibles et nous synthétisons les contrôleurs des ces systèmes lorsque les propriétés sont écrites en $WT_mu$.

 Plus d'infos 

20090123  Maxregular languages 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
A new class of languages of infinite words is introduced, called the
maxregular languages, extending the class of omegaregular languages.
The class has two equivalent descriptions: in terms of automata (a
type of deterministic counter automaton), and in terms of logic (weak
monadic secondorder logic with a bounding quantifier). Effective
translations between the logic and automata are given. 
 Plus d'infos 

20090108  Génération Automatique d'Approximations Régulières 
11:0012:15 Salle 076, LaBRI, Rezdechaussée 
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ême pour des systèmes de réécritures simples. Une approche pour
résoudre ce problème consiste alors à utiliser des approximations de
R*(I). Nous montrerons dans cet exposé comment une technique manuelle
d'approximations introduite par Th. Genet en 98 peut être automatisée,
notamment pour la vérification de protocoles cryptographiques.

 Plus d'infos 

Liste des événements répétitifs du groupe Modélisation et Verification
RetourRetour à l'index
 