| Date (YYYY-MM-DD) | Orateur/Animateur | Titre |
|---|---|---|
| 2010-07-01 | Florian Horn (LIAFA (Paris)) | Solving Simple Stochastic Tail Games |
| 2010-06-03 | Camilo Rueda (Universidad Javeriana-Cali) | A formal framework for social Networking |
methods tools and techniques to develop a full-fledged social-network service implementing stipulated policies. The system includes a B method definition for social networking, modelling social-network content, privacy policies, social-networks friendship relations, and how these relations affect users' policies. This core is expected to be extended by third-party plug-ins in such a way that adherence to system policies is guaranteed by formal techniques such as proof-carrying code. | ||
| 2010-05-27 | Nicolas Halbwachs (Verimag, Grenoble) | Static analysis of positional and non positional properties of arrays |
Although array bound checking was a motivation of the very first work on abstract interpretation, there are only few proposals about dealing with array *contents* in program analysis. The reason is, of course, that the general problem is difficult: array indexing induces complex semantics, and in particular the possibility of aliasing; moreover, since the size of an array can be large or unknown, it represents a large or unbounded number of variables. In this talk, we present two complementary analyses dealing with properties of array contents in some simple cases: one-dimensional arrays, traversed by simple "for" loops. Both analyses are based on abstract interpretation: - the first one aims at discovering positional properties of arrays elements. For instance, it is able to discover that the result of an insertion sort is a sorted array. - the second one addresses non positional properties, like the fact that, at some point of a program, the content of an array is a permutation of its initial content. | ||
| 2010-05-20 | Bernard Boigelot (Institut Montefiore (Liège, Belgique)) | Implicit Real Vector Automata |
polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop a symbolic data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of non-convex polyhedra, is closed under Boolean operators, and admits an efficient decision procedure for testing the membership of a vector. Joint work with Julien Brusten and Jean-François Degbomont | ||
| 2010-04-22 | Christophe Joubert (Technical University of Valencia, Spain ) | Datalog-based Program Analysis with BES and RWL |
evaluate Datalog queries in the context of object-oriented program analyses: the first approach transforms the Datalog program in an implicit Boolean Equation Systems (BESs) solved by existing general purpose verification toolboxes, such as CADP, providing local BES resolutions with linear-time complexity; the second approach transforms Datalog programs into Rewriting Logic and produces an efficient rewrite system exploiting the main features of the high-level programming language Maude. Datalog is used as a specification language for expressing both complex interprocedural program analyses involving dynamically created objects and queries. We confirm our results experimentally by applying it to some real-world Datalog-based analyses. | ||
| 2010-04-15 | Eugene Asarin (LIAFA (Paris)) | Volume and entropy of regular timed languages |
(joint work with Aldric Degorre, Concur'09+ Formats'09) | ||
| 2010-04-01 | Arnaud Sangnier (Dipartimento di Informatica Università degli studi di Torino, Italy) | When Model-Checking Freeze LTL over Counter Machines Becomes Decidable |
This is a joint work with Stéphane Demri (LSV, CNRS, ENS de Cachan) and Ranko Lazic (Department of Computer Science, University of Warwick). | ||
| 2010-03-11 | Johannes Kinder (TU Darmstadt, Allemagne) | Static Analysis of x86 Executables |
suffer from the problem that a complete control flow graph of the program is not available. Data flow analysis has been proposed before to statically determine branch targets in many cases, yet a generic strategy without assumptions on compiler idioms or debug information was missing. We have devised a framework for generic low level programs with indirect jumps which safely combines a pluggable abstract domain with the notion of partial control flow graphs. Using our framework, we were able to show that the control flow reconstruction algorithm of our disassembly tool Jakstab produces the most precise overapproximation of the control flow graph with respect to the used abstract domain. Based on this rigorous approach to disassembly, Jakstab has evolved into a flexible program analysis framework on binaries. Preliminary experiments with Windows driver binaries show that it can successfully check API specifications with higher precision than existing approaches, while achieving complete independence from source code. | ||
| 2010-02-25 | Philipp Ruemmer (Oxford University, Computing Laboratory, UK) | Craig Interpolation for Quantifier-Free Presburger Arithmetic |
for instance to generate intermediate assertions for safety analysis. Interpolants are often determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this talk, I consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which until recently no efficient interpolation procedures were known. As one such procedure, I introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. In particular, the complexity of extracting interpolants from proofs is discussed. Finally, I add support for uninterpreted predicates to the calculus, thus extending it to important theories such as arrays and uninterpreted functions. The talk describes joint work with Angelo Brillout, Daniel Kroening, and Thomas Wahl. | ||
| 2010-02-18 | Peter Habermehl (LIAFA) | On non-deterministic automata for Presburger arithmetic. |
uses deterministic finite-state automata. While the complexity of the decision procedure for PA based on quantifier elimination is known (triple-exponential), the exact complexity of the automata-based procedure was unknown. We show that it is triple-exponential as well by analysing the structure of the non-deterministic automata obtained during the construction building on results from Klaedtke. Furthermore, we analyse the sizes of deterministic and non-deterministic automata built for several subclasses of Presburger arithmetic. To retain a canonical representation which is one of the strengths of the use of automata we use a class of non-deterministic automata called residual finite-state automata introduced by Denis, Lemay and Terlutte. | ||
| 2010-02-11 | Mauricio Toro (LaBRI) | Towards a Computational Modeling of an Heterogeneous System for Interactive Musical Scores |
*This is one of the objectives to accomplish in my doctorate, which I started on october 2009. | ||
| 2010-02-04 | Mathieu Tracol (LRI) | Recurrence and Transience for Probabilistic Automata |
condition d'acceptation classique (de Buchi) pour un run est qu'il passe infiniment souvent sur un etat acceptant. Un mot est alors accepté s'il existe un run acceptant pour ce mot. Dans un contexte d'automates probabilistes (PBA), un mot est accepté si la probabilité de l'ensemble des runs pour ce mot qui passent infiniment sur un etat acceptant est strictement positive. Avec cette definition, il devient indecidable de decider si le language d'un PBA est vide ou non. On relaxe la definition d'acceptation d'un run en demandant maintenant que la proportion du temps passé sur un des etats acceptants ne tend pas vers zero. Decider le vide du language devient alors decidable. Nous etudions la complexité du probleme de decision associé (PSPACE complet), et nous etudions les propriétés de cloture de notre nouvelle classe d'automates probabilistes. L'essentiel de l'etude se ramene à l'etude de la notion de recurrence dans le cas des chaines de Markov non-homogenes. | ||
| 2010-01-14 | Peter Niebert (LIF, Marseille) | L'approche SAT pour lpour automates temporisés avec étapes parallèles |
D'un autre coté, pour des systèmes non-temporisés, on connaît des réductions SAT qui utilisent une sémantique avec transitions parallèles : la possibilité d'exécuter plusieurs transitions indépendantes en parallèle raccourcit des séquences témoin et permet ainsi d'aller plus loin avec la vérification bornée. Dans notre travail, nous combinons les deux améliorations, ordres partiels pour automates temporisés et transitions parallèles pour une meilleure réduction SAT. Il se pose alors la question de ce que sont des « transitions parallèles » pour un automate temporisé. Autre que la réponse intuitive « en parallèle est en même temps » nous explorons deux autres sémantiques avec des notions plus relâchées pour les transitions parallèles. Il s'avère que les trois sémantiques ont des performances incomparables, selon les exemples considérés. À l'occasion, je présente aussi le vérificateur POEM, qui est la plate forme expérimentale avec laquelle nous avons réalisé le prototype et les expériences. | ||
| 2010-01-07 | Julien Forget (LaBRI) | Un Langage Synchrone pour les Systèmes Embarqués Critiques Temps Réel |
L'exposé porte sur la programmation de systèmes de Contrôle-Commande. Ces systèmes sont constitués d'une boucle de contrôle qui acquiert l'état actuel du système par des capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Ces systèmes sont critiques, leur implantation doit donc être déterministe, sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates). Nous définissons un langage de description d'architecture logicielle temps réel et son compilateur pour programmer de tels systèmes. Il permet d'assembler les composants fonctionnels d'un système multi-rythme avec une sémantique formelle synchrone. Un programme consiste en un ensemble d'opérations importées, reliées par des dépendances de données. Des contraintes de périodicité ou d'échéance peuvent être spécifiées sur les opérations et un ensemble réduit d'opérateurs de transition de rythme permet de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes. Des analyses statiques assurent que la sémantique d'un programme est bien définie. Un programme correct est ensuite compilé en un ensemble de tâches temps réel concurrentes implantées sous forme de threads C communicants. Le code généré préserve la sémantique du programme original et s'exécute à l'aide d'un Système d'Exploitation Temps Réel standard disposant de la politique d'ordonnancement EDF. | ||
| 2009-12-17 | Pierre-Alain Reynier (LIF, Marseille) | Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study |
| 2009-12-10 | Stéphane Demri (LSV, ENS-Cachan) | Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents. |
formel de calcul qui est utilisé par exemple en linguistique ou pour la vérification de protocoles cryptographiques. Ce modèle a aussi des liens étroits avec des logiques de données interprétées sur des arbres avec valeurs mais aussi avec la logique linéaire MELL. La décidabilité du problème d'accessibilité pour ces systèmes demeure encore aujourd'hui ouverte, et ce problème est équivalent à divers problèmes essentiels des domaines cités plus haut. Récemment, Verma et Goubault-Larrecq ont réussi à montrer que les problèmes de finitude et de couverture pour les BVAS sont décidables. Dans cet exposé, je vais présenter comment caractériser la complexité des problèmes de couverture et de finitude pour les BVAS. Une partie de la preuve consiste à raffiner les travaux de Rackoff dans le cas linéaire correspondant au modèle des réseaux de Petri. Ce travail a été mené conjointement avec Marcin Jurdzinski, Oded Lachish et Ranko Lazic (University of Warwick, UK). | ||
| 2009-12-03 | François Laroussinie (LIAFA) | Alternating-time Temporal Logic: Expressivity, Complexity, Extensions |
expressing properties over games (modeled with Concurrent Game Structures). We will present ATL, ATL* and also two extensions: with strategy contexts and with memory constraints. The first extension makes strategy quantifiers to not ``forget'' the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We will first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms ATL, ATL*, Game Logic, AMC, Strategy Logic,... We will also address the problem of model-checking for these logics. Joint work with: Th. Brihaye, A.. Da Costa, N. Markey. | ||
| 2009-11-26 | Jean Goubault-Larrecq (LSV, ENS-Cachan) | Games on Infinite Domains and Approximation |
doing over the last few years in semantic models of mixed non-deterministic and probabilistic choice. One can also see this as models for two-player turn-based (stochastic) games, where the state space X is infinite. The approach is topological and domain-theoretical. In particular, X need not be Hausdorff, which leads to interesting models where the knowledge of the current state can itself be approximate. We shall give a brief tour of these, through capacity-based models, prevision models, simulation and (if time permits) simulation (hemi-)metrics. | ||
| 2009-11-12 | Alexander Heussner (LaBRI) | Reachability Analysis of Communicating Pushdown Systems |
over asynchronous and reliable fifo channels calls for restrictions to ensure decidability. We extend here a model proposed by La Torre, Madhusudan and Parlato [TACAS08], based on communicating pushdown systems that can dequeue with empty stack only. Our extension adds the dual modality, which allows to dequeue with non-empty stack, thus modelling interrupts for working threads. We study (possibly cyclic) network architectures under a semantic assumption (mutex communication) that ensures the decidability of reachability for finite state systems. Subsequently, we determine precisely how pushdowns can be added to this setting while preserving the decidability; in the positive case we obtain exponential time as the exact complexity bound of reachability. A second result is a generalization of the doubly exponential time algorithm of [LaTorre et al: TACAS08] for bounded context analysis to our symmetric queueing policy. We provide here a direct (and simpler) proof. Joint work with Jérôme Leroux, Anca Muscholl, Grégoire Sutre | ||
| 2009-11-05 | Mohamed-Faouzi Atig (LIAFA) | On the Verification Problem for Weak Memory Models |
We consider in this work combinations of three well-known program order relaxations. We consider first the "write to read" relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the "write to write" relaxation (leading to a model which is essentially PSO), or (2) the "read to read/write" relaxation, or (3) both of them (as it is done in the RMO model for instance). We define abstract operational models for these weak memory models based on state machines with (potentially unbounded) FIFO buffers, and we investigate the decidability of their reachability and their repeated reachability problems. We prove that the reachability problem is decidable for the TSO model, as well as for its extension with "write to write" relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the "read to read/write" relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. As for the repeated reachability problem, we prove that it is undecidable already for the TSO model. (Joint work with Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi) | ||
| 2009-10-22 | Tristan Le Gall (ULB, Bruxelle, Belgique) | Control of Infinite Symbolic Transition Systems under Partial Observation |
controllers through partial observation of infinite state systems modelled by Symbolic Transition Systems. To obtain algorithms for solving these problems, we use abstract interpretation techniques which provide over-approximations of the transitions set to be disabled. We implemented those algorithm in a tool and made an empirical validation of our methods to show their feasibility and usability. Keywords: Symbolic Transition Systems, Control Synthesis, Partial Observation, Abstract Interpretation. Joint work with Gabriel Kalyon, Tristan Le Gall, Hervé Marchand and Thierry Massart. | ||
| 2009-09-29 | Anil Seth (IIT Kanpur, India) | Parity Games on Multistack Systems |
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. | ||