Les jeux stochastiques constituent un modèle naturel pour la synthèse de contrôleurs en milieu ouvert, lorsque certaines actions peuvent être considérées comme aléatoires. Deux questions majeures se posent : - Peut-on garantir une propriété quasi-surement ? - Si non, avec quelle probabilité peut on la garantir ? Le second problème est nettement plus complexe que le premier. En particulier, pour le cas de base des jeux d'accessibilité, le problème quasi-sûr est polynomial, tandis que le problème optimal est dans NP \cap co-NP. Dans cet exposé, je présenterai les deux attaques classiques de ce problème : par valeurs et par amélioration de stratégies. Je présenterai ensuite un angle d'attaque original, manipulant des ordres sur les états aléatoire du graphe, ainsi que différents algorithmes qui en dérivent. En particulier, je montrerai comment nos résultats peuvent s'adapter à toutes les conditions de victoire préfixes-indépendantes, à travers un méta-algorithme liant directement la complexité du calcul des valeurs à celle des problèmes quasi-surs et à un seul joueur.

Les jeux stochastiques constituent un modèle naturel pour la synthèse de contrôleurs en milieux ouvert, lorsque certaines actions peuvent être considérées comme aléatoires. Les jeux $\omega$-réguliers, dont les parties sont de longueur infinie, peuvent ainsi représenter des systèmes réactifs qui doivent réagir correctement à un flux continuel d'évènements. Une ressource critique pour ce genre d'applications est la mémoire utilisée lors de l'implémentation effective du contrôleur. Pour chaque condition de Muller, on peut déduire de l'"arbre de Zielonka" la quantité de mémoire nécessaire et suffisante pour définir des stratégies gagnantes. Dans cet exposé, je montrerai comment l'utilisation de stratégies randomisées permet de gagner "presque sûrement" à moindre coût dans chaque arène. Dans ce contexte également, c'est à partir de l'étude de l'"arbre de Zielonka" que l'on définit une meilleure borne supérieure. De plus, pour chaque condition, il existe certaines arènes (de taille exponentielle) pour lesquelles des stratégies utilisant moins de mémoire sont presque sûrement perdantes.

There are several approaches developed by the Implicit Computational Complexity (ICC) community which try to analyze and control program resources. We focus our study on the resource control with the help of semantics interpretations. After introducing the notion of quasi-interpretation together with its distinct properties and characterizations, we show the results obtained in the study of such a tool: We study the synthesis problem which consists in finding a quasi-interpretation for a given program and we tackle the issue of quasi-interpretation modularity. Modularity allows to decrease the complexity of the synthesis procedure and to capture more algorithms. Afterwards, we introduce the notion of sup-interpretation. This notion strictly generalizes the one of quasi-interpretation and is used in distinct criteria in order to control the resources of more algorithms, including algorithms over infinite data and algorithms using a divide and conquer strategy. We combine sup-interpretations with distinct termination criteria, such as RPO orderings, dependency pairs or size-change principle, and we compare them to the notion of quasi-interpretation. Using the notion of sup-interpretation, we characterize small parallel complexity classes. We provide some heuristics for the sup-interpretation synthesis: we manage to synthesize sup-interpretations without the subterm property, that is, sup-interpretations which are not quasi-interpretations. Finally, we extend sup-interpretations to object-oriented programs, thus obtaining distinct criteria for resource control of object-oriented programs and their methods.

Résumé à venir

Résumé: Sequential game and Nash equilibrium are basic key concepts in game theory. In 1953, Kuhn showed that every sequential game has a Nash equilibrium. Traditionally, sequential games involve real-valued payoff functions. I replace them with abstract atomic objects and generalise Kuhn's result to such an extent that I get an equivalence property. I provide two proofs very different from a proof theoretic viewpoint. I have fully formalised the first proof using Coq. In the end of the talk, I may describe the Coq formalism representing the core concepts of this development.

Stephane Leroux sera ensuite disponible pour vous présenter le reste de son travail de thèse, résumé ci-dessous, et discuter avec vous: Les jeux strategiques sont une classe de jeux de la theorie des jeux. La notion d'equilibre de Nash leur est associee. On aimerait bien que chaque jeu ait un equilibre de Nash, mais ce n'est pas le cas, et il n'existe pas de caracterisation simple des jeux qui en ont un. Les deux approches classiques a ce probleme sont celle de Kuhn (et ses predecesseurs) et celle de Nash (et ses predecesseurs). Kuhn definit une sous classe de jeux, les jeux sequentiels, dont il prouve qu'ils ont tous un equilibre de Nash. A l'oppose, Nash affaiblit la notion d'equilibre de Nash en introduisant les probabilites et prouve que tout jeu strategique a un equilibre de Nash probabiliste. Tout ces travaux ont ete effectues dans un contexte de gain a valeur dans R (nombres reels). Je supprime cette restriction, je definis des jeux abstraits, et je regarde comment les techniques de Kuhn et Nash se generalisent. Dans le cas de Nash, les probabilites ne fonctionnent plus et je propose un non-determinisme discret a la place.

We consider Boolean combinations of data tree patterns as a specification and query language for XML documents. Data tree patterns are tree patterns plus variable equalities which express joins between attribute values. Data tree patterns are a simple and natural formalism for expressing properties of XML documents. We consider first the query evaluation problem. We show that it is DP-complete in general and already NP-complete when the query has only one pattern. We then consider the satisfiability problem in the presence of DTD. We show that it is in general undecidable and we identify various decidable fragments.

Common work with Manuel Clavel, Universidad Complutense de Madrid Résumé : We present an approach based on inductive theorem proving for verifying invariance properties of systems specified in Rewriting Logic, an executable specification language implemented (among others) in the Maude tool. Since theorem proving is not directly available for rewriting logic, we define an encoding of rewriting logic into its membership equational (sub)logic. Then, inductive theorem provers for membership equational logic, such as the itp tool, can be used for verifying the resulting membership equational logic specification, and, implicitly, for verifying invariance properties of the original rewriting logic specification. The approach is illustrated first on a 2-process Bakery algorithm and then on a parameterised, n-process version of the algorithm.

Résumé : We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a complete verification method which only partially exploits symmetry, and an approximate verification method which fully exploits symmetry. We describe how symmetry markers can be efficiently computed and integrated into the SPIN tool, and provide an empirical evaluation of our technique using the TopSPIN symmetry reduction package, which shows very good performance results and a high degree of precision for the approximate method (i.e. very few non-symmetric states receive the same marker). We also identify a class of models for which the approximate technique is precise. Contact à l'IRISA : T. Jéron (Vertecs)

UML Use Case Diagrams are a first step towards the definition of system requirements, however, they do not provide enough information for many purposes. UML Activity Diagrams (AD) and Use Case Maps (UCM) provide such information in a quite comprehensive manner. We have developed a "Core Scenario Model" (CSM) that captures the common semantics of AD and UCM, as well as performance-related information. It is closely related to Petri nets and the BPEL notation for Web Services. We show how this notation can also be used for describing the order of execution of collaborations where each collaboration involves two or more system components in the context of distributed services. In the second part of my talk, I will discuss how one can derive an application protocol from the system requirements as described above. The protocol should define the behavior of all the system components in such a manner as to ensure the given requirements. We will discuss under which conditions such a protocol can be derived in a straightforward manner from the service requirements, and we will also discuss what kind of coordination messages may be introduced in more complex situations. Certain situations are difficult to handle in a distributed context, such as alternative choices that involve several components. We will discuss approaches that can be used to deal with such problems which are quite common in distributed applications.

Résumé : Les structures d'événements constituent un modèle standard des processus concurrents non déterministes. Elles combinent des aspects de la théorie des ordres avec des aspects de la théorie des graphes, présentant ainsi un grand nombre problèmes combinatoires à résoudre. Quand on veut montrer que ces modèles sont équivalents à d'autres (tels que les automates, les réseaux de Petri, etc.) il se pose le problème d'étiqueter les arêtes du diagramme de Hasse du domaine associé. Nous présenterons en détailles ce problème, qui en effet revient à un problème de coloriage de graphes. Nous présenterons aussi les peu nombreux résultats connus. Contact à l'IRISA : L. Hélouët (Distribcom)

This presentation considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors. The proposed method consists in computing a sequence of automata representing approximations of the convex hull and using extrapolation techniques to compute the limit of this sequence. The convex hull can then be directly computed from this limit in the form of an automaton-based representation of the corresponding set of real vectors. The technique is quite general and has been successfully implemented. Our result also fits in a wider scheme whose objective is to improve the techniques for converting automata-based representation of constraints to formulas.

Work with François Cantin and Pierre Wolper Contact à l'IRISA : S. Pinchinat (S4)

The emerging technology of interacting systems calls for new formalisms to ensure their reliability. Concurrent games are paradigmatic abstract models for which several logics have been studied. However, the existing formalisms show certain limitations in face of the range of strategy properties required to address intuitive situations. We propose a generic solution to specify expressive constraints on strategies in concurrent games. Our formalism naturally extends alternating-time logics while being highly flexible to combine constraints. Our approach is constructive and can synthesize many types of complex strategies, via automata-theoretic techniques.

Résumé: We present the mathematical foundations of the contract-based model developed in the framework of the SPEEDS project. SPEEDS aims at developing methods and tools to support ``speculative design'', a design methodology in which distributed designers develop different aspects of the overall system, in a concurrent but controlled way. Our generic mathematical model of contract supports this style of development. This is achieved by focusing on behaviors, by supporting the notion of ``rich component'' where diverse (functional and non-functional) aspects of the system can be considered and combined, by representing rich components via their set of associated contracts, and by formalizing the whole process of component composition.

Résumé: Frameworks that incorporate communication into decentralized supervisory control theory address the following problem: find locations in the evolution of the plant behavior where some supervisors send information so that a supervisor that was unable to make the correct control decision prior to receiving external information, is now capable of making the correct control decision. Proposed solutions to this problem identify an earliest and a latest placement where such communication results in the synthesis of a correct control solution. In addition to a first and last communication opportunity, there may be a selection of intermediate possibilities where communication would produce the correct control solution. In this talk I will present a computable procedure to identify a broader range of suitable communication locations. This is joint work with Benoit Caillaud.

Résumé: Les propriétés des langages de scénarios (Message Sequence Charts, Live Sequence Charts, ou diagrammes de séquences d'UML) ont été largement étudiées ces dix dernières années. Les langages de scénarios ayant la puissance d'expression des traces de Mazurkiewicz, de nombreux problèmes pratiques, comme le model-checking, sont indécidables pour ces langages. Cependant, malgré leur puissance d'expression élevée, la plupart des langages de scénarios ne permet de générer que des comportements finiment engendrés, qui ne peuvent être exprimés que comme des concaténations séquentielles de comportements choisis dans un ensemble fini de motifs. Cependant, on rencontre couramment des comportements non-finiment engendrés lorsque l'on cherche à modéliser des systèmes distribués et asynchrones, ce qui est le cas du mécanisme de fenêtres glissantes du protocole TCP. Plusieurs extensions des Message Sequence Charts ont été proposées pour remédier à ce problème, mais ces variantes donnent aux scénarios la puissance d'expression des automates communicants à canaux de communication non-bornés (et par conséquent des Machines de Turing), rendant l'analyse de ces langages encore plus difficile. Dans cet exposé, nous proposons une extension des Message Sequence Charts qui permet de définir des comportements non finiment engendrés sans pour autant donner aux scénarios la puissance des automates communicants, et présentons ses propriétés.

Résumé: Cet exposé présente un cadre formel pour le test de systèmes réactifs à partir de spécifications logiques. Nous étendons le cadre de test fonctionnel défini initialement pour des spécifications algébriques. Dans ce cadre, une méthode de sélection de tests à été définie, appelée dépliage des axiomes. Cette méthode s'appuie sur la définition de critères de sélection dérivés des axiomes de la spécification. Nous proposons alors d'étendre et d'adapter ce cadre pour tester des systèmes dynamiques et réactifs spécifiés à l'aide de logiques modales. L'objectif est d'aborder le test de ce type de systèmes de façon nouvelle, l'approche habituelle étant celle du test de conformité. Nous montrerons alors que ces deux approches sont complémentaires. Contact à l'IRISA : V. Rusu, équipe Vertecs

Résumé: When giving away data, the data provider usually looses control of this data: among many other things, the receiver can re-distribute or archive it. Distributed usage control is concerned with requirements that include "must be deleted after 30 days", "no re-distribution", "at most three copies", "data subject must be notified upon every access", and "use for statistical purposes only". It turns out that the field is equally relevant in the domains of data protection and the management of intellectual property (including DRM) as well as secrets in general. The talk kicks off with an overview of the problem domain. We will then present a policy language together with formal analysis tools, and discuss applications in the areas of composition and interoperability of enforcement mechanisms, negotiation of policies, and rights delegation. The characteristics of usage control as enabling technology will be demonstrated on the grounds of implementations for mobile phones, the Windows Rights Management System, and service-oriented architectures. Contact à l'IRISA : B. Baudry équipe Triskell

Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognized the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released, and when information can be released. We apply this classification in order to evaluate the security of a case study realized in a security-typed language -- an implementation of a non-trivial cryptographic protocol that allows playing online poker without a trusted third party. In addition, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful "sanity checks" for emerging models.

The talk is based on joint work, in part, with David Sands, and, in part, with Aslan Askarov. Contact à l'IRISA : Thomas Genet, équipe Lande

Résumé: Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this presentation, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication. We extends investigation to acceleration in convex data-flow analysis of systems with real-valued variables where guards are convex polyhedra and assignments are translations. In particular, we present a simple and algorithmically efficient characterization of MFP-acceleration for cycles with a unique initial location. We also show that the MFP-solution is a computable algebraic polyhedron for systems with two variables. Contact à l'IRISA : L. Hélouët, équipe Distribcom

Résumé: We study the relationship between various concepts in model-based design, and use the results to derive a general solution to the synthesis of a local specification given a context (residuation). We use an algebraic framework to introduce the concepts of compatibility and conformance (refinement) independently of the particular model of computation employed, and then establish their relationship through a particular notion of complement (mirror). The synthesis problem is set up as the solution to an algebraic equation, and solved using the properties required by the framework. We outline an application in protocol conversion. Contact à l'IRISA : B. Caillaud, équipe S4

Résumé : For distributed systems, logging is an integral part of many middleware aspects, especially, transactions and monitoring. In the event of a failure, the log allows us to deduce the cause of failure (diagnosis), recover by compensating the logged actions (atomicity), etc. However, for heterogeneous systems, logging all the actions is often impracticable due to privacy/security constraints. Also, logging is expensive in terms of both time and space. Thus, we are interested in determining a minimal set of actions that needs to be logged, to know with certainty the actual sequence of executed actions from any given partial log. This problem happens to be NP-Complete. We then propose a decomposition framework in order to use a divide and conquer algorithm. This method also leads to an efficient algorithm for hierarchical systems where components may be reused many times.

Résumé : M'intéressant à l'étude morphologique des ensembles ordonnés finis au travers des sous-structures orthogonales que sont les chaînes et les antichaînes, je vais être amené à introduire la classe des ordres chaîne dominés. Ces ordres sont des ordres admettant une famille partitive de ses éléments en deux ensembles. L'un de ces ensembles induit un chemin dans son digraphe de couverture et l'autre induit un sous-digraphe sans arc. Après avoir rappelé les définitions de base nécessaires à l'exposé, je montrerai que cette classe d'ordre est l'intersection de deux classes connues que sont les ordres d'intervalles et les treillis tronqués. Puis, en utilisant la notion de couplage maximum dans les graphes, je montrerai que le calcul du nombre de sauts des ordres chaîne dominés est alors polynomial. Enfin, je montrerai que tout ordre d'intervalles peut se plonger dans un ordre de cette classe et que leurs dimensions ne diffèrent pas de plus deux.

Programme : On June 14th afternoon, some of the members of Eric Fabre's habilitation jury will participate to a mini-workshop:

14:30 On the composition of processes

by Glynn Winskel (Prof. of CS, Univ. of Cambridge, UK)

Abstract: Pullbacks of Petri nets play a key role in Eric Fabre's habilitation thesis, where they capture the composition of two systems via a common interface. Being an example of a categorical limit, pullbacks in the category of Petri nets are automatically preserved by the operation of unfolding a net to a net of its occurrences (because this operation is a right adjoint) --- a fact which Fabre exploits in the analysis of net behaviour. Pullbacks, again representing a composition of processes, appear in a variety of other contexts. In this talk I will broaden the picture and explain the sense in which uses of pullbacks can fruitfully be seen as examples of the composition of generalized relations, relations which stand for computations between types.

15:30 Chronicle-based monitoring: chronicle learning, and distributed recognition, by Christophe Dousson (France Telecom R & D)

16:30 Decentralized/distributed approaches to diagnosis by Stephane Lafortune (Prof. of EECS, Univ. of Michigan)

Résumé : à venir

Résumé : Middleware has emerged as an important architectural component in modern distributed systems. The role of middleware is to offer a high-level, platform-independent programming model to users (e.g. object-oriented or component-based) and to mask out problems of distribution. Traditionally, such platforms have been deployed (with considerable success) in application domains such as banking and finance as a means of tackling problems of heterogeneity, and also supporting the integration of legacy systems. More recently, middleware technologies have been applied in a wider range of areas including safety critical systems, embedded systems, and real-time systems. In addition, middleware is required to respond to emerging technical challenges as offered for example by mobile and ubiquitous computing, the Grid or P2P computing. It is now becoming apparent that established middleware technologies (such as the ones listed) are not able to respond to such diversity or to such technical challenges. The main reason for this is the /black-box philosophy/ of existing platforms. In particular, existing middleware platforms offer a fixed service to their users, and it is not possible to view or alter the implementation of this service. Inevitably, the architecture of this platform then represents a compromise design featuring, for example, general-purpose protocols and associated management strategies. It is then not possible to specialise platforms to meet the needs of more specific target domains. At Lancaster, we believe that next generation middleware platforms should have the following properties: 1. They should be /configurable/ to meet the needs of a given application domain (e.g. to provide a minimal configuration for embedded systems) 2. They should be /dynamically reconfigurable/ to enable the platforms to respond to changes in their environment (e.g. to respond to dramatic fluctuations in network quality of service as experienced in mobile computing) 3. they should support the /evolution /of the design of the platform as requirements change over time (e.g. to respond to the need to support continuous media interactions). In particular, we have developed an approach which applies principles of reflection to the design of middleware platforms to meet the above properties. This seminar will provide an overview of our research into this emerging field of /reflective middleware/ approach and also examine one project in detail, i.e. GridKit, where we have developed an experimental reflective middleware platform to meet the advanced needs of Grid applications. The seminar will also lead into a discussion of reflection and how it relates to model-driven software development, in particular how concepts such as architectural reflection relate to having models that persist at run-time (Models@run.time).

Résumé : In this talk we introduce the ITP tool, a rewriting-based theorem prover that can be used to prove inductive properties of membership equational specifications. We also discuss membership equational logic as a formal language particularly adequate for specifying and verifying semantic data structures, such as ordered lists, search binary trees, priority queues, and powerlists. The ITP tool is a Maude program that makes extensive use of the reflective capabilities of this system. In fact, rewriting-based proof simplification steps are directly executed by the underlying Maude rewriting engine. Using also the reflective capabilities of Maude, the ITP tool implements a decision procedure for linear arithmetic with uninterpreted function symbols which is integrated into its simplification procedure. The ITP tool is currently available as a web-based application that includes a module editor, a formula editor, and a command editor. These editors allow users to create and modify their specifications, to formalize properties about them, and to guide their proofs by filling and submitting web forms.

Résumé : Les assistants de preuves comme Coq sont capables de vérifier des preuves. Par contre, leur assistance quant à la production de preuve laisse à désirer. À son corps défendant, l'utilisateur est trop souvent contraint à descendre à un niveau de détail de preuve qui frise le ridicule. En effet, rien de plus frustrant que d'avoir à prouver manuellement une propriété qui tombe dans un fragment manifestement décidable. Dans cet exposé, je vous montrerai comment la preuve par réflexion (ou preuve calculatoire) permet d'augmenter l'automatisation d'un assistant de preuve comme Coq à moindre coût. Dans la première partie de l'exposé, je développerai de A à Y un exemple simpliste de preuve par réflexion. Dans la seconde partie de l'exposé, je présenterai la mise en oeuvre de micromega une tactique Coq réflexive pour résoudre des buts arithmétiques sur Z de la forme: for all x1...xn, ¬(^ e_i(x1,...,xn) ? 0) avec e ::= e + e | - e | e * e | c | x Pour résoudre de tels buts, micromega appelle des procédures de décision externes (et existantes) qui produisent intrinsèquement des certificats de non-satisfiabilité qui sont (efficacement) vérifiés par Coq.

Résumé: Le produit sur les mots est associatif. Cette propriété permet d'écrire un mot de nombreuses façons, c'est à dire de le factoriser. La technique de factorisation consiste à rendre une propriété aisée à vérifier sur un mot quand une bonne factorisation en est choisie. Par exemple, il est plus facile de vérifier qu'il y a un nombre pair de lettres dans le mot factorisé (aa)(aa)(aa)(aa)(aa)(aa) que dans aaaaaaaaaaaa. Cet exposé sera l'occasion de montrer combien ce principe élémentaire peut être utile en théorie des automates. Nous commencerons par l'utilisation du théorème de Ramsey par Büchi sur les mots de longueur oméga. Puis nous nous nous intéresserons au théorème des forêts de factorisation de Simon, et son utilisation sur les automates de distance. Nous verrons enfin comment prolonger et unifier ces approches. On retombera alors sur le théorème de déterminisation de McNaughton, la complémentation des automates sur les mots dispersés dénombrables, la complémentation d'automates à compteurs ou encore des résultats d'équivalences entre logiques.

On considère des systèmes distribués, modélisés par des graphes, dans lesquels les processus communiquent par échange de messages en mode asynchrone dans lesquels les processus n'ont pas nécessairement d'identifiants uniques.

Le problème de la détection de la terminaison est le suivant. On considère un algorithme distribué qui permet de réaliser une tâche quelconque sur une famille de graphes et on cherche à déterminer sous quelles conditions il est possible de modifier cet algorithme de telle sorte que lorsque l'exécution est terminée (chaque processus a calculé sa valeur finale), alors au moins un processus puisse détecter que l'exécution est globalement terminée.

On présente une condition nécessaire et suffisante permettant une telle transformation. En fait, il s'avère que cette condition ne dépend que de la famille de graphes considérés et non de l'algorithme initial. Les résultats connus deviennent alors des corollaires de cette caractérisation. On obtient aussi de nouveaux critères simples permettant d'assurer l'existence d'un algorithme détectant la terminaison.

Résultats obtenus en collaboration avec Yves Métivier, Emmanuel Godard et Gerard Tel.

The modular construction of finite and complete prefixes applied to distributed systems, which are modelled by Petri nets in form of synchronous products of automata, is presented. A distributed system is described as a collection of components interacting through interfaces. They exhibit factorisation properties, viz. the unfolding of a distributed system factorises as the product of unfoldings of its components. This gives a compact representation and makes it possible to analise the system by parts.

The construction of modular prefixes is based on deriving 'summaries' of components w.r.t. their interfaces whilst passing them on the interaction structure of system via interfaces. Prefixes of components are then derived locally by taking into account the summaries received on their interfaces.

Le problème de la synthèse a été posé par Church au début des années 60. Un algorithme de synthèse prend en entrée une spécification reliant des entrées et des sorties, et doit produire une machine réagissant instantanément aux entrées en produisant des sorties (comme un transducteur) réalisant cette spécification, si c'est possible.

Le problème peut être paramétré par le langage de spécification et le type de machines sur lesquelles les spécifications sont réalisées.

Dans cet exposé, on présentera le cas de systèmes distribués où les processus communiquent de façon synchrone, et de spécifications allant de LTL, cadre introduit par Pnueli et Rosner, au mu-calcul, en essayant de dégager la limite entre décidabilité et indécidabilité.

Le séminaire de cette semaine s'inscrit dans le cadre du séminaire CRYPTO de l'IRMAR, et se déroulera donc dans le batiment 22 (a.k.a la Tour de Maths).

Tous les programmeurs s'attendent à ce que les compilateurs et autres outils de génération de code produisent du code exécutable qui se comporte exactement comme prescrit par le programme source. Ce n'est malheureusement pas toujours le cas : des bugs dans le compilateur peuvent conduire à la production de code machine incorrect à partir d'un source correct. Ce cas de figure est particulièrement préoccupant dans le cas de code critique qui a été vérifié (au niveau source) à l'aide de méthodes formelles (analyse statique, model checking, preuve de programme) : tout bug dans le compilateur peut potentiellement invalider les garanties obtenues à grand-peine grâce aux méthodes formelles.

Après une introduction aux méthodes formelles et aux différentes manières de renforcer la confiance que l'on peut avoir dans un compilateur, l'exposé détaillera l'une de ces manières : la preuve de programme appliquée directement au compilateur lui-même, avec pour but de prouver que le comportement du programme source est préservé par toutes les passes du compilateur. Je présenterai les premiers résultats du projet Compcert : une expérience de développement et de preuve de correction, utilisant l'assistant de preuves Coq, d'un compilateur modérément optimisant pour un sous-ensemble du langage C. Ces premiers résultats sont encourageants et suggèrent, à plus long terme, que la vérification formelle d'outils intervenant dans la production et la certification de codes critiques est faisable.

Reasoning about programs is (even!) harder when they are distributed (for instance over a wide area network). I will begin this talk by presenting a process calculus in which processes are explicitly located and may use an explicit migration construct to move between locations: the Dpi-calculus.

I will show then a type system suited for this calculus in which types correspond to access rights granted to processes. This type system allows a location to control the processes trying to enter. I will talk of the difficulties arising in this type system and describe an observational equivalence that respect those constraints over migations. Finally I will sketch a complete proof technique that enlighten some subtle difficulties in this setting.

An abstract context-free grammar can be viewed as a system of polynomial functors. The initial algebra of this functor coincides with its least fixed-point; and this fixed-point can be computed by a method of substitution using Bekic theorem. By doing so the system of polynomial functors is transformed into a related system of regular functors. We introduce a splitting operation on algebras producing an algebra for the resulting system of regular functors from an algebra of the original system of polynomial functors. This transformation preserves the interpretation function (catamorphism). The end result is a class of (extended) abstract context-free grammars, associated with regular functors. This class seems to be well-adapted to the modular design of domain-specific embedded languages.

Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow type systems. Much of previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions, and method calls, and/or do not prove formally the soundness of the type system. We define an information flow type system for a sequential JVM-like language that includes classes, objects, arrays, exceptions and method calls, and prove that it guarantees non-interference. For increased confidence, we have formalized the proof in the proof assistant Coq; an additional benefit of the formalization is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to our best knowledge, the first sound and implemented information flow type system for such an expressive fragment of the JVM.

Note:
This work will be presented at the 16th European Symposium on Programming (ESOP'07) Follow this link.

Cet expose presente un etat de l'art de resultats recents concernant deux types d'approximation qui peuvent etre utiles dans le contexte de la verification pour reduire la complexite en temps et en espace. Dans le premier cas, on introduit une notion d'approximation sur les donnees, c'est-a-dire sur le modele a verifier, definie a l'aide d'une distance. Il est alors possible de concevoir des algorithmes probabilistes permettant de decider, en temps independant de la taille du modele, si la propriete consideree est satisfaite ou si elle est loin, a epsilon pres au sens de la distance, de l'etre. Dans le second cas, on definit une methode d'approximation pour la verification de proprietes quantitatives sur des systemes probabilistes. Les algorithmes probabilistes d'approximation ainsi obtenus permettent de reduire de maniere exponentielle la complexite en espace. Ces algorithmes ont ete implementes de maniere distribuee dans un model checker probabiliste qui s'est revele tres efficace.

Les slides Verification probabiliste et Approximation

La page du projet Vera et le lien sur un papier dont il a parlé.