Uli Fahrenberg (IRISA Rennes) — The Quantitative Linear-Time–Branching-Time Spectrum2012-04-05 14:30 salle 1073
We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point 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.
Tobias Heindel (CEA, LIST) — Adhesive Categories and Related Concepts2012-03-14 10:30 salle 1073
This talk presents the application relevant results of my thesis, which I would summarize as follows.
My thesis discusses the formal semantics for a family of rewriting formalisms that have arisen as category theoretical abstractions of the so-called algebraic approaches to graph rewriting. The latter in turn generalize and combine features of term rewriting and Petri nets. Two salient features of (the abstract versions of) graph rewriting are a suitable class of categories which captures the structure of the objects of rewriting, and a notion of independence or concurrency of rewriting steps – as in the theory of Petri nets.
Category theoretical abstractions of graph rewriting such as double pushout rewriting encapsulate the complex details of the structures that are to be rewritten by considering them as objects of a suitable abstract category, for example an adhesive one. The main difficulty of the development of appropriate categorical frameworks is the identification of the essential properties of the category of graphs which allow to develop the theory of graph rewriting in an abstract framework. The motivations for such an endeavor are twofold: to arrive at a succint description of the fundamental principles of rewriting systems in general, and to apply well-established verification and analysis techniques of the theory of Petri nets (and also term rewriting systems) to a wide range of distributed and concurrent systems in which states have a “graph-like” structure.
The contributions of the thesis thus can be considered as two sides of the same coin: on the one side, concepts and results for Petri nets (and graph grammars) are generalized to an abstract category theoretical setting; on the other side, suitable classes of “graph-like” categories which capture the essential properties of the category of graphs are identified. Two central results are the following: first, (concatenable) processes are faithful partial order representations of equivalence classes of system runs which only differ w.r.t. the rescheduling of causally independent events; second, the unfolding of a system is established as the canonical partial order representation of all possible events (following the work of Winskel). Weakly ω-adhesive categories are introduced as the theoretical foundation for the corresponding formal theorems about processes and unfoldings.
The main result states that an unfolding procedure for systems which are given as single pushout grammars in weakly ω-adhesive categories exists and can be characetrised as a right adjoint functor from a category of grammars to the subcategory of occurrence grammars. This result specializes to and improves upon existing results concerning the coreflective semantics of the unfolding of graph grammars and Petri nets (under an individual token in- terpretation). Moreover, the unfolding procedure is in principle usable as the starting point for static analysis techniques such as McMillan’s finite complete prefix method.
2012-03-07 10:30 salle 1068
Cet exposé présente un retour d'expérience sur l'analyse à base de traces que nous avons implémentée dans notre analyseur de code binaire. Ce modèle nous permet d'analyser un code embarqué au niveau binaire de 30kloc en une dizaine de secondes et ce sans effort particulier sur le développement de la représentation mémoire. Si ce modèle a été implémenté dans un cadre d'analyse très bas niveau, nous pensons qu'il peut s'appliquer dans un cadre bien plus général, en pouvant supporter des aspects composition et raffinement.
La première partie définit les traces associées à une analyse statique, l'ordre partiel qu'elles définissent ainsi que leur construction.
Ensuite nous montrons des utilisations de ce modèle de traces, notamment pour optimiser les opérations de split et de fusion sur l’état mémoire d'une analyse par interprétation abstraite, et ce sans conséquence sur les résultats de l'analyse elle-même. Les traces servent également à implémenter relativement efficacement une analyse arrière à la volée, se déclenchant sur chaque problème de précision que peut rencontrer l'analyse avant. Le résultat est une analyse qui, en une seule passe, construit le graphe de contrôle et effectue une analyse de valeurs tout en stockant les informations nécessaires aux calculs des dépendances de données.
Enfin nous évoquerons des pistes de réflexions pour utiliser ce modèle dans un cadre d'analyse modulaire par interprétation abstraite et/ou dans un cadre d'analyse du parallélisme, ces deux derniers points étant sujets à discussions.
Michael Farber (Warwick Mathematics Institute) — Topics of applied algebraic topology2012-02-16 14:00 salle 1044
I will make a brief survey of my recent work on topological robotics and stochastic topology. Specifically I will mention the theory of topological complexity of robot motion planning algorithms, solution of Walker conjecture concerning configuration spaces of linkages, probabilistic approach to linkages, and results about random simplicial complexes (Linial - Meshulam model).
Jacques-Henri Jourdan (CEA, LIST) — Validation d'analyseur syntaxique LR(1) à l'aide de Coq2012-02-15 10:30 salle 1068
Le compilateur C CompCert, formellement vérifié grâce à l'assistant de preuves Coq, a amélioré la confiance que nous pouvons accorder à un compilateur. Cependant, certaines parties ont toujours besoin d'être prouvées : mon travail a pour but de créer un analyseur syntaxique prouvé pour CompCert.
Je vais présenter une méthode permettant d'obtenir des analyseurs syntaxique LR(1) vérifiés : j'utilise une version modifiée du générateur d'analyseur syntaxique Menhir pour générer la description d'un automate LR(1). Puis, j'ai prouvé correct en Coq un validateur et un interpréteur d'une telle description. En utilisant ce procédé, il est possible de construire un analyseur de performances raisonnables pour la grammaire du C99 (presque) toute entière.
S'il nous reste du temps (et selon vos envies), on pourra étudier plus en détails quelques problèmes survenus lors de ce travail : la non-terminaison des automates LR, la sensibilité au contexte de la grammaire C99....
Stefan Schwoon (LSV) — McMillan meets SAT: Détection d'interblocage dans des réseaux de Petri2012-01-25 14:00 salle 1044
La détection d'interblocage dans des systemes concurrents et distribués est un problème fondamental et reste important. Une technique standard pour les spécifications basée sur les réseaux de Petri est le préfix complet de McMillan, c'est à dire une partie initiale de son dépliage qui est assez grande pour que tous les états accessibles soient représentés; l'avantage de la technique est la répresentation compacte de l'espace d'états en exploitant la concurrence dans le réseau donné. En utilisant les SAT solvers, la détection des interblocages devient assez efficace (rélatif à la taille du préfix).
L'exposé présente un survol des résultats et discute quelques développements actuels. S'il reste de temps, une discussion de l'extension vers les interblocages locaux et des problèmes réliés conclure l'exposé.
Assalé Adje (LMeASI) — Programmation semi-infinie et invariants numériques convexes fermés2012-01-18 10:30 salle 1044
Un ensemble convexe fermé peut être vu comme l'intersection des demi-espaces le contenant. On peut ainsi calculer des invariants numériques convexes fermés en manipulant une infinité de formes linéaires via les gabarits ("templates"). Le calcul de ceux-ci fait intervenir des problèmes d'optimisation semi-infinie. Dans ma présentation, je présenterai cette classe de problèmes d'optimisation et mon travail en cours sur son application en interprétation abstraite.
Olivier Mullier (LMeASI) — Sous-approximation du range d’une fonction vectorielle ayant des dimensions différentes pour ses domaine et codomaine2011-10-05 10:30 salle 1044
Mon attention s'est portée sur le problème de détermination du range d'une fonction vectorielle f : R^m → R^n avec m potentiellement différent de n. A. Goldsztejn et L. Jaulin ont défini une méthode de calcul de sous-approximation pour ce problème lorsque les dimensions du domaine et du codomaine sont égaux. Dans cette présentation, je montrerai une extension de cette méthode dans le cas générique. Cette extension nous emmène vers un sous problème : l'extraction d'une sous matrice de rang maximum pour une matrice intervalle contenant la Jacobienne de f . Une partie de ma présentation sera donc dédiée à la résolution de ce problème en utilisant la programmation linéaire et l'implémentation sera montrée au travers d'exemples simples.
Tristan Le Gall (LMeASI) — Abstract cofibered domains: Application to the alias analysis of untyped programs2011-09-26 14:00 salle 31
Présentation d'un article d'Arnaud Venet.
We present a class of domains for Abstract Interpretation, the cofibered domains, that are obtained by "glueing" a category of partially ordered sets together. The internal structure of these domains is well suited to the compositional design of approximations and widening operators, and we give generic methods for performing such constructions. We illustrate the interest of these domains by developing an alias analysis of untyped programs handling structured data. The results obtained with this analysis are comparable in accuracy to those obtained with the most powerful alias analyses existing for typed languages.
2011-09-20 10:30 salle '?'
L'exposé portera sur la caractérisation des systèmes complexes à base de composants au travers de la présence de propriétés émergentes, qui soit entrent en conflit avec les propriétés attachées aux composants les constituant, soit sont directement issues de la coopération ou de l'interaction des composants.
La problématique de la caractérisation de systèmes complexes par les propriétés émergentes fait écho à un souci récurrent du génie logiciel : est-il possible de concevoir un système en le structurant de telle sorte que les propriétés attachées aux composants ou modules le constituant puissent être héritées systématiquement par le système tout entier ? Cette propriété est souvent perçue comme un préalable à la réutilisation des composants.
Au-delà de la conception des systèmes logiciels, les systèmes complexes sont omniprésents et font l'objet d'études dans plusieurs disciplines : la biologie, la physique, les sciences humaines les sciences cognitives. Dans le contexte de la biologie, les réseaux de régulation génétique sont bel et bien un exemple de tels systèmes complexes si l'on considère qu'un sous-réseau construit avec quelques gènes constitue un sous-système. En effet, conformément à l'idée commune à propos de la régulation des gènes, le comportement d'un réseau peut être remis en cause lorsqu'il est plongé dans un réseau plus grand.
Dans cet exposé, je vais présenter un cadre de spécifications au sein duquel il sera possible de caractériser formellement ce qu'est un système complexe. Le cadre est général puisqu'il est défini au-dessus des institutions. Nous considérons ici qu'un système est complexe dès lors qu'il est composé de plusieurs sous-systèmes interconnectés entre eux et que ses propriétés ne sont pas déductibles de celles des sous-systèmes le composant. Dans le cas contraire, c'est-à-dire, dans le cas où les propriétés du système sont déductibles de celles des composants, le système est qualifié de modulaire.
Je vais illustrer ce cadre générique sur deux exemples concrets de nature différente pour appuyer mes propos : les systèmes réactifs et les réseaux de régulation génétique
Cinzia Di Giusto (INRIA Rhône-Alpes) — ?2011-09-05 14:00 salle 31
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes. As such, they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime. This allows to express a wide range of evolvability patterns for processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that at most k consecutive errors will arise in future states, the latter ensures that if the system enters in an error state then it will eventually reach a correct state. We study the (un)decidability of these two adaptation properties in different fragments of the calculus. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.
Olivier Bouissou (CEA LIST) — Une sémantique opérationnelle de Simulink2011-06-29 10:30 salle 31
Le logiciel Simulink joue souvent un rôle majeur lors du développement de systèmes de contrôle-commande. Grâce à sa grande expressivité et facilité d'utilisation, il est souvent utilisé pour simuler le comportement d'un système comportant une partie continue (l'environnement physique) et une partie discrète (l'algorithme de contrôle). Le design de l'algorithme de contrôle (choix des paramètres, de la fréquence d'échantillonnage, ...) dépend fortement du résultat de ces simulations. Cependant, ces simulations peuvent contenir de nombreuses erreurs et donner une image fausse du comportement réel du système de contrôle-commande. Par exemple, la solution des équations différentielles est calculée via un schéma numérique (souvent de type Runge-Kutta) qui peut s'éloigner de la solution réelle que suivra le système physique. En Simulink, ce genre d'erreur apparaît fréquemment et pour des raisons diverses (bloc intégrateur, phénomène de zero-crossing, calcul à virgule flottante, ...).
Pour améliorer le processus de design des algorithmes de contrôle commande, il convient donc de mesurer ces erreurs pour s'assurer de la pertinence des simulations calculées par Simulink. Dans cet exposé, nous présentons des travaux préliminaires dans cette direction en donnant une sémantique formelle de Simulink. Cette sémantique opérationnelle définit formellement, sous la forme d'un système de transitions, le résultat de la simulation de Simulink et prend en compte à la fois les aspects continus et discrets du langage. Nous considérons également des aspects importants de Simulink comme le choix du solver numérique, la détection et la localisation des zero-crossing, le choix des périodes de sampling...
Simon Bliudze (CEA LIST) — Fondements et une application de l'analyse non standard2011-06-22 14:00 salle '?'
Dans les 17e et 18e siècles, Leibnitz et Newton se servaient de la notion de « différentiel » pour raisonner sur les grandeurs physiques et leur évolutions. Cette approche rend certaines notions de l’analyse très intuitive, mais souffrait, à l’époque, de l’absence de fondements formels. Par conséquence elle a été abandonnée au début du 19ème siècle suite au développement de l’analyse tel que l’on connait aujourd’hui. Dans les années 1960, Abraham Robinson a proposé une formalisation de l’analyse non standard, qui déclenché plusieurs travaux théoriques et de applicatifs.
Dans cette présentation, qui fait écho à celle donnée au LMeASI par Marc Pouzet, je vais présenter quelques notions de base de la théorie de l’analyse non standard, puis parler de l’application que nous en avons faite pour la modélisation des systèmes réactifs hybrides. Cette modélisation suit la démarche similaire à celle des machines de Turing avec la définition des notions de système (machine) et de calculabilité sur les réels.
Jean Goubault-Larrecq (LSV (ENS Cachan)) — A Smell of Orchids2011-06-09 10:30 salle 31
Orchids is an intrusion detection tool based on techniques for fast, on-line model-checking that we developed at LSV (ENS Cachan, CNRS; also project-team SECSI, INRIA). Orchids detects complex, correlated strands of events with very low overhead in practice, although its detection algorithm has worst-case exponential time complexity. With the help of a few attacks, I'll explain the salient features of the basic model-checking algorithm. I'll also explain how we tame the complexity of the procedure, using abstract interpretation techniques to safely kill useless monitors.
I'll also explain some of the new directions we are now taking with Orchids. Its integrated Prolog engine, for one, allows us to do forensics in a particularly elegant way.
This is joint work with Julien Olivain, and more recently Baptiste Gourdin and Hedi Benzina
Tom Hirschowitz (LAMA, Univ. de Savoie) — Sheaves and duality for directed spaces2011-05-25 10:30 salle 31
Directed topology is a refinement of standard topology, where spaces may have non-reversible paths. It has been put forward as a candidate approach to the analysis of concurrent processes. Recently, a wealth of different frameworks for, i.e., categories of, directed spaces have been proposed.
The present paper defines an abstract construction which produces, from a so-called orienting object on a given Grothendieck site, a category of directed objects. When applied to topological spaces, with appropriate Grothendieck topology and orienting object, this process yields a category which we relate via an adjunction to Grandis's category of d-spaces. This yields a categorical interpretation of the stability conditions required for non-reversible paths to form a valid d-space.
The Grothendieck topology we use to obtain this is the so-called canonical topology on the category of spaces, which is the largest topology making representables into sheaves. We obtain a new characterisation of this topology.
Arnault Ioualalen (Université de Perpignan) — Efficient Transformation of Arithmetic Expressions for Program Safety2011-05-18 14:30 salle 31
Floating-point arithmetic is an important source of errors in programs because of the loss of accuracy it induces. Even if we can bind statically the roundoff error due to the evaluation of a numerical expression, it is still difficult to transform one expression into another that is more accurate. It is well known that an expression could be transformed in many ways using the usual laws of arithmetic, like associativity or commutativity.
The goal of this talk is to introduce a new abstract interpretation-based framework to efficiently approximate sets of mathematically equivalent evaluation traces of expressions. Compared to previous approaches, this technique strongly improves the variety of expressions that we can capture in the abstract and makes it possible to transform more efficiently expressions in order to optimize their evaluation in the floating-point arithmetic.
Matthias Puech (Univ. de Bologne / PPS) — A logical framework for incremental type-checking2011-05-04 10:30 salle 134
In this talk, I will present an ongoing work on a variant of the LF metalanguage, suitable as the core data structure of an /incremental type-checker/. Such a type-checker would allow eventually to provide in turn different versions of a typing derivation, of which only the differing sub-derivations are to be rechecked. It is the key ingredient for designing an enhanced interaction model with our well-known coding/proving tools: non-linear user interaction, typed version control system, type-directed programming...
Designing such a type-checker involves feeding it with a /repository/ containing the previous version(s) of the derivation, and making it return the updated repository. Following popular VCS systems, we explore a data-oriented approach to versioning and use the LF metalanguage for representing derivations in the repository: the reuse of a piece of sub-derivation is encoded as a cut in LF, and subsequent versions as object-level data structures. For this, we need to modify only slightly the usual syntax and metatheory of LF. I will discuss the overall architecture involved in this design, and focus on the repository and the interaction with it.
Assaé Adjé (LIX) — Caractérisation du plus petit point fixe et itération sur les politiques et applications aux jeux à paiements positifs et à l'interprétation abstraite2011-04-20 10:30 salle 31
Dans le cas des jeux stochastiques classiques, avec taux d'escompte, l'itération sur les politiques retourne l'unique point fixe de l'opérateur de Shapley. Malheureusement quand le point fixe de l'opérateur de Shapley n'est plus unique, l'itération sur les politiques retourne un point fixe qui n'est pas forcément le plus petit point fixe. Dans le cadre des jeux à paiements positifs, le plus petit point fixe de l'opérateur de Shapley détermine la valeur du jeu. Dans le cadre de l'interprétation abstraite, le plus petit point fixe de l'analogue de l'opérateur de Shapley détermine les bornes de l'invariant numérique le plus précis. L'atteinte du plus petit point fixe dans ces deux cadres est donc une question importante. Dans cet exposé, nous commençons par rappeler brièvement ce qu'est l'itération sur les politiques dans le cas des jeux stochastiques puis en interprétation abstraite. Dans un deuxième temps, nous proposons une caractérisation du plus petit point fixe pour les fonctions contractantes grâce à la semidifférentielle et au rayon spectral non linéaire. Enfin, nous illustrons nos résultats sur quelques jeux à paiements positifs ainsi que sur des programmes analysés dans le domaine des intervalles.
Uli Fahrenberg (IRISA Rennes) — Max-plus polyhedra in real-time reachability2011-03-29 14:00 salle 134
Reachability algorithms for real-time models have to work with symbolic representation to ensure termination. For the model of timed automata, the state-of-the-art symbolic representation is given by so-called zones, which computationally are represented by difference-bound matrices (DBM). To overcome some fundamental problems with the zone/DBM representation, we propose using convex max-plus polyhedra instead. We show that the reachability algorithms can be implemented using internal representations of convex max-plus polyhedra.
In the talk we will carefully introduce the timed-automata reachability problem as well as its zone-based solution. Afterwards we will talk a bit about max-plus algebra and convex max-plus polyhedra, and then we will show the different algorithms. We put emphasis on efficiency of the algorithms, as we expect that our current algorithms can be much improved.
Arshia Cont + Jean Louis Giavitto (IRCAM) — Antescofo: Performance Synchronous Language for Realtime Computer Music + 8 1/2 : un langage déclaratif data-parallèle synchrone2011-03-23 10:30 salle 31
Antescofo est un système de suivi de partition modulaire et un langage de programmation synchrone pour la composition musicale. Le module permet la reconnaissance automatique de la position dans la partition et le tempo du musicien en temps réel, permettant ainsi de synchroniser une performance instrumentale avec celle d’une partition virtuelle informatique. Antescofo réunit la description de la partie instrumentale et électronique dans la même partition, et grâce à un langage synchrone conçu pour la pratique de musique mixte, afin d'augmenter l'expressivité lors de l'écriture des processus temps réel et proche au langage commun des artistes pour l'écriture du temps et de l'interaction.
http://repmus.ircam.fr/antescofo
"Otto e Mezzo" est un langage déclaratif à flot de données qui combine une notion d'horloge synchrone permettant une composition plus souple des programmes et des opérations data-parallèles. Nous montrerons comment les flots résultants peuvent se définir par des définitions récursives aussi bien spatiale que temporelle, le typage permettant de s'assurer du caractère effectif de ces définitions. Nous évoquerons aussi quelques éléments d'implémentation sur diverses architectures parallèles.
Marc Pouzet (ENS Ulm) — Divide & Recycle: Types and Compilation for a Hybrid Synchronous Language2011-03-16 10:30 salle 31
Hybrid modelers such as Simulink have become the corner stone of complex embedded systems development. They allow to program in the very same language both the discrete controller and its continuous environment. Nonetheless, this combination raises a number of semantics and typing issues as well as a clear separation of the discrete and continuous part.
In this talk, we present an extension of a synchronous language with a mean to mix ordinary differential equations (ODE) and data-flow equations. We propose to use non standard analysis as a semantic foundation for the language. This semantics clarifies the interaction between the continuous part --- which is exercised by the numerical solver --- from the discrete part and clarifies how zero-crossings interact with each others. We presents the type system and compilation for this language. We show several concrete examples written in the prototype SunLucid and its interaction with the solver SUNDIALS cvode.
The main contribution of this work is to show that a hybrid modeler can be developed on top of an existing synchronous language by reusing most of their compilation techniques.
This is joint work with Albert Benveniste, Tim Bourke and Benoit Caillaud.
Matthias Péron (MathWorks) — Discovering Properties about Arrays Contents in Simple Programs2011-03-02 10:30 salle 31
Array bound checking has been widely studied. However, there are few works about array contents analysis, and all of them date back to the last decade.
In the core of these static analyses there are symbolic partitioning analyses of the arrays. To precisely analyze a loop "for i = 1 to n", in which an array is accessed at index i, slices [1, i - 1], [i, i] and [i + 1, n] of arrays contents must be considered. We defined a semantic partitioning analysis and then an array contents analysis based on its results. Both of these analyses are abstract interpretations. The later analysis binds to each slice S a property P whose variables stand for the arrays contents of the slice. The properties P are interpreted pointwise on the slice. So for S = [1, i - 1] and P = (a = b + 1), it means that for all k in [1, i - 1], a[k] = b[k] + 1.
Experimental results show that our automatic analysis is efficient and precise on simple programs: one-dimensional arrays, indexed by one variable at most (x+c or c), traversed by possibly nested "for" loops, the counters of which follow an arithmetic progression. The analysis is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a "sentinel", the index stays within the bounds.
Finally, I will briefly point out interesting recent work on this subject, that followed ours.
oint work with Nicolas Halbwachs (CNRS/Verimag) and Francesco Logozzo (Microsoft Research)
Arnaud Spiwack (LIX) — Mathematics without Unique Choice2011-02-23 10:30 salle 31
I will present in this talk the principles of choice and unique choice, and how they are usually articulated around constructive mathematics. From this starting point, I will describe why the unique choice, which is traditionally valid, is a hindrance in the project of writing computationally efficient mathematics. Fortunately, the principle of unique choice is not provable in Coq, due to the (weak) irrelevance of the sort of propositions. The separation of the sort Prop from the rest of the logic was motivated by program extraction, which is, of course, related to the problem of efficient mathematics. In a sense, we will seek to give some mathematical substance to the pragmatics behind Prop. I will discuss the mathematical consequences of dropping the unique choice (a lot of things break, some seriously. That's the cost of efficiency).
Jade Alglave (Oxford University Computing Laboratory) — Fences in Weak Memory Models2011-02-16 10:30 salle 134
We present an axiomatic framework, implemented in Coq, to define weak memory models w.r.t. several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as Sequential Consistency from a weaker one. Finally, we provide a tool, diy, that tests a given machine to determine the architecture it exhibits. We detail the results of our experiments on Power and the model we extract from it. This identified an implementation error in Power 5 memory barriers (for which IBM is providing a software workaround); our results also suggest that Power 6 does not suffer from this problem.
Tali Sznajder (LIP6) — Fair Synthesis of Asynchronous Distributed Systems2011-01-26 10:30 salle 8
We study the synthesis problem in an asynchronous distributed setting: a finite set of processes interact locally with an uncontrollable environment and communicate with each other by sending signals -- actions that are immediately received by the target process. The fair synthesis problem is to come up with a local strategy for each process such that the resulting fair behaviours of the system meet a given specification. We consider external specifications over partial orders. External means that specifications only relate input and output actions from and to the environment and not signals exchanged by processes. We also ask for some closure properties of the specification. We present this new setting for studying the fair synthesis problem for distributed systems, and give decidability results: the non-distributed case, and 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.
Pierre-Loïc Garoche (ONERA) — Model-checking LUSTRE using k-induction2011-01-19 14:00 salle 31
In this talk, we will present our approach for verying properties on Lustre-like programs. Lustre is a synchronous language which is widely used to model control systems. As far as we know one of the most efficient method to address verification issues for these programs and ensure their safety is model-checking, based on the k-induction principle and SMT solvers. But one of the major drawback of this approach is the need of external inputs, mainly done by humans nowadays, to reinforce the description of the system to help the analysis to converge. Our proposal is based on a specific collaboration between a k-induction procedure and an abstract interpreter to evaluate safety properties and inject lemmas describing the system during the k-induction process.
This talk will present the Lustre language, the k-induction method tooled with SMT solvers and finally our approach to collaboration between techniques.
This work has been done in collaboration with Pierre Roux and Rémi Delmas, from Onera.