To: mvtsi-gt@labri.fr
Cc:
Subject: [GT MVTsi -- Séminaire]
Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2009-09-17).
Jérôme,
========================================================================
La page du groupe de travail:
http://www.labri.fr/~leroux/seminaire/
========================================================================
Date (YYYY-MM-DD) | Orateur/Animateur | Titre |
---|---|---|
2009-06-18 | Denis Lugiez (LIFM, Marseille) | Edition Collaborative d'arbres XML |
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 time-stamps 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 contre-exemples 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 non-ordonné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 sous-arbres à 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. | ||
2009-06-04 | André Arnold () | Contrôleurs non déterministes de processus non déterministes |
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. | ||
2009-05-28 | Nathalie Bertrand (IRISA, Rennes, France) | When are Timed Automata Determinizable? |
This is a joint work with C. Baier, P. Bouyer and T. Brihaye. | ||
2009-05-14 | Pierre Ganty (UCLA, Los Angeles, California) | What's decidable for Asynchronous Programs ? |
procedure calls which are not directly executed from the call site, but stored and executed later by an external scheduler. By providing a low-overhead 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. | ||
2009-05-07 | Alain Finkel (LSV, Cachan, France) | Well Structured Transition Systems everywhere and everytime ! |
It is possible to complete any well-ordered 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 Karp-Miller tree procedure when applied on extended Petri nets and lossy channel systems. | ||
2009-04-30 | Stéphane Gaubert (INRIA and CMAP, Ecole Polytechnique) | Algorithmes de théorie des jeux en analyse statique de programme |
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 Perron-Frobenius non-linéaire (rayons spectraux, calcul semi-diffé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é. | ||
2009-04-23 | Sylvain Sené (LIRIS, Villeurbanne) | Robustesse environnementale dans les réseaux d'automates à seuil : théorie et application en biologie. |
2009-04-02 | David Teller-Rajchenbach (université d'Orléans) | Extrapol, des systèmes de types dépendants à la sécurité système |
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 post-mortem (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. | ||
2009-03-19 | Alain Griffault (LaBRI, Bordeaux, France) | AltaRica : passé, présent et futur. |
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". | ||
2009-03-12 | Paul Gastin (LSV, Cachan, France) | How to get decidability of distributed synthesis ? |
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. | ||
2009-03-05 | Stéphane Demri (LSV, Cachan, France) | Modal Logics with Presburger constraints |
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 well-known and non-trivial 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). | ||
2009-02-12 | Omer NGUENA (LaBRI, Bordeaux, France) | Spécification et Contrôle des Systèmes temps-réel faibles |
2009-01-23 | Mikolaj Bojanczyk (Institute of Informatics, Warsaw University) | Max-regular languages |
max-regular languages, extending the class of omega-regular languages. The class has two equivalent descriptions: in terms of automata (a type of deterministic counter automaton), and in terms of logic (weak monadic second-order logic with a bounding quantifier). Effective translations between the logic and automata are given. | ||
2009-01-08 | Pierre Cyril Heam (LIFC, Université de Franche0Compté) | Génération Automatique d'Approximations Régulières |
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. | ||
2008-12-18 | Alexander Heussner (LaBRI, Bordeaux, France) | CEGAR for Communicating Fifo Systems |
protocols demands for methods that are able to process infinite state spaces and emergent behaviour. Communicating fifo systems are a standard model for distributed processes which are represented by a set of finite automata that exchange messages over a network of reliable, unbounded fifo channels. We utilize the counterexample-guided abstraction refinement technique (CEGAR) for the automatic verification of communicating fifo systems regarding safety properties. This is accomplished with the help of predicate abstraction and a predicate refinement strategy relying on the computation of path invariants based on an additional extrapolation operator for recognizable languages. The presentation of the verification algorithm is completed by a brief presentation of a prototypical implementation. | ||
2008-12-11 | Pawel Parys (Warsaw University, Poland) | XPath evaluation in linear time |
2008-12-04 | Ahmed Bouajjani (LIAFA, Paris) | Analyzing Asynchronous Programs with Preemption |
an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of these models where tasks may be of different priority level, and can be preempted at any point of their execution by tasks of higher priority. We investigate the control point reachability problem for these models. Our main result is that this problem is decidable by reduction to the reachability problem for a decidable class of Petri nets with inhibitor arcs. We also identify two subclasses of these models for which the control point reachability problem is reducible respectively to the reachability problem and to the coverability problem for Petri nets (without inhibitor arcs). This is a joint work with Mohamed Faouzi Atig and Tayssir Touili. | ||
2008-11-27 | Tayssir Touili (LIAFA, Paris) | On the Reachability Analysis of Acyclic Networks of Pushdown Systems |
communication based either on shared memory or on message passing through unbounded lossy channels. We prove mainly that the reachability problem between recognizable sets of configurations (i.e., definable by a finite union of products of finite-state automata) is decidable for such networks, and that for lossy channel pushdown networks, the channel language is effectively recognizable. This fact holds although the set of reachable configurations (including stack contents) for a network of depth (at least) 2 is not rational in general (i.e., not definable by a multi-tape finite automaton). Moreover, we prove that for a network of depth 1, the reachability set is rational and effectively constructible (under an additional condition on the topology for lossy channel networks). This is a joint work with Mohamed Faouzi Atig and Ahmed Bouajjani | ||
2008-11-20 | Xavier ALLAMIGEON (EADS) | Inferring Min and Max Invariants Using Max-plus Polyhedra |
the program variables, based on max-plus polyhedra. Our abstraction is more precise than octagons, and allows to express non-convex properties without any disjunctive representations. We have defined sound abstract operators, evaluated their complexity, and implemented them in a static analyzer. It is able to automatically compute precise properties on numerical and memory manipulating programs such as algorithms on strings and arrays. | ||
2008-11-13 | Arnaud Sangnier (LSV, ENS-Cachan) | Reversal-Bounded Counter Machines Revisited |
This is a joint work with Alain Finkel. | ||
2008-11-06 | Blaise Genest (IRISA, Rennes, France) | Quasi-Static Scheduling of Communicating Tasks |
This is a joint work with philippe Darondeau, P.S. Thiagarajan and Shaofa Yang. | ||
2008-10-16 | Serge Haddad (LSV, Cachan, France) | Logiques pour le model checking des chaînes de Markov à temps continu |
balance between being able to adequately model the system's behavior and being able to afford the cost of the model solution. Systems can be modelled directly as Markov chains, or with a higher-level formalism for which Markov chains represent the underlying semantics. Markov chains are widely used to study the performance of computer and telecommunication systems. The definition of stochastic temporal logics like Continuous Stochastic Logic (CSL) and its variant asCSL, and of their model-checking algorithms, allows a unified approach to the verification of systems, allowing the mix of performance evaluation and probabilistic verification. In this talk we present the stochastic logic CSLTA, which is more expressive than CSL and asCSL, and in which properties can be specified using automata (more precisely, timed automata with a single clock). The extension with respect to expressiveness allows the specification of properties referring to the probability of a finite sequence of timed events. A typical example is the responsiveness property ``with probability at least 0.75, a message sent at time 0 by a system A will be received before time 5 by system B and the acknowledgment will be back at A before time 7'', a property that cannot be expressed in either CSL or asCSL. Furthermore, the choice of using automata rather than the classical temporal operators Next and Until should help in enlarging the accessibility of model checking to a larger public. We also present a model-checking algorithm for CSLTA. | ||
2008-10-09 | Hélène Kirchner (INRIA Bordeaux - Sud-Ouest) | A rewrite-based approach for security policies |
for the compositional design, maintenance and verification of security policies. Rewrite rules transform input terms representing policy requests into decision terms. Strategies are used to explicitly control the rule application. Parameterized queries are solved by narrowing. Relying on the correspondences between the properties of the rewrite system and the policy it implements, we are able to reuse existing proof techniques and analysis tools in the security policies context. Joint work with Claude Kirchner and Anderson Santana de Oliveira | ||
2008-09-25 | Jérôme Leroux (LaBRI, Bordeaux, France) | An Easy Algorithm For The General Vector Addition System Reachability Problem |
2008-09-18 | (1) Jean-Christophe Filliâtre et (2) Sylvain Conchon (LRI, Université Paris Sud, France) | (1) Utilisation de prouveurs SMT pour la preuve de programmes et (2) Vérification de propriétés de programmes avec Alt-Ergo |
Cet exposé présente l'utilisation de prouveurs SMT pour la preuve de programmes C et Java dans le cadre de la plateforme Why (http://why.lri.fr/). En particulier, on justifie le choix d'une logique du premier ordre polymorphe comme langage d'entrée pour utiliser les différents prouveurs SMT, et on explique comment cette logique est encodée lorsque le prouveur SMT ne l'implante pas nativement. Cet exposé indique également quelles sont les théories pertinentes pour la vérification de programmes, et comment leur absence dans certains prouveurs SMT peut être contournée à l'aide de modèles axiomatiques. Enfin, on explique comment les prouveurs SMT peuvent être utilisés depuis l'assistant de preuve Coq, lorsque la preuve interactive devient nécessaire. (2) Alt-Ergo est un démonstrateur automatique de théorèmes dédié à la vérification de propriétés de programmes. Les formules logiques envoyées à Alt-Ergo sont écrites dans la logique du 1er ordre polymorphe multi-sortée de l'outil Why. Dans cet exposé nous décrirons l'architecture d'Alt-Ergo. Elle est composée d'un SAT-solver qui interagit avec un algorithme de combinaison de procédures de décision et un mécanisme d'instanciation pour traiter les formules quantifiées. Le code d'Alt-Ergo est très court (environ 4000 lignes d'Ocaml) ce qui en fait un bon candidat pour réaliser la preuve en Coq d'un démonstrateur automatique. Alt-Ergo est disponible à http://alt-ergo.lri.fr |