Groupe de Travail
Modélisation, Optimisation
et Analyse Statique

Le groupe de travail aura lieu au CIRM du lundi 7/01/2013 après-midi au vendredi 11/01/2013 fin de matinée. Le petit déjeuner aura lieu de 7h00 à 9h00, le déjeuner à 12h30 et diner à 19h30.

Programme

Lundi 7 janvier

Mardi 8 janvier

Mercredi 9 janvier

Jeudi 10 janvier

Vendredi 11 janvier

Résumés

Manel Abid — MAP estimation of the input of an oversampled filter bank from noisy subbands

Oversampled filter banks perform simultaneously subband decomposition and redundancy introduction. This redundancy has been shown to be useful to combat channel impairments, when the subbands are transmitted over a wireless channel, as well as quantization noise. This talk describes several implementation of the maximum a posteriori estimator of the input signal from the noisy quantized subbands obtained at the output of some transmission channel. In a first approach, the relations between the input samples and the noisy subband samples are described using a factor graph. Belief propagation is then applied to get the posterior marginals of the input samples. In a second approach, the bounded nature of the quantization noise is explicitely taken into account to build a consistent estimator.

Alexandre Chapoutot — Méthodes de Runge-Kutta implicite en mode garanti (slides)

Les systèmes hybrides sont composés de parties évoluant continûment dans le temps et de parties évoluant de manière discrète dans le temps. Une des nombreuses manières de représenter ces systèmes s'appuie sur une extension des systèmes dynamiques qui mélange des équations différentielles et des équations récurrentes. Par exemple, cette représentation est utilisée dans le logiciel Matlab/Simulink qui est utilisé dans l'industrie dans le cadre de la conception dirigée par les modèles. La vérification formelle de ces systèmes repose sur la capacité à résoudre des équations différentielles. Dans des cas particuliers, par exemple les systèmes linéaires, il est possible d'avoir la solution analytique de ces équations. Cependant, dans le cas général cette solution analytique est impossible à avoir et il est nécessaire de recourir à des méthodes numériques pour approcher ou dans le meilleur des cas encadrer la solution exacte de ces équations différentielles. Les méthodes numériques qui encadrent la solution exacte des équations différentielles sont dites garanties et soit elles reposent sur un développement de Taylor soit elles appartiennent à la famille des méthodes de Runge-Kutta explicites. Nous présentons un début de formalisation pour rendre garanti les méthodes de Runge-Kutta implicite. Nous motiverons ce travail en rappelant les caractéristiques et propriétés associées aux schémas numériques d'intégration et nous rappellerons les éléments importants de l'intégration numérique garantie.

Cinzia di Giusto — Disciplined Structured Communications with Consistent Runtime Adaptation

Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing adaptation and evolvability requirements. This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. In previous work, we developed a process calculi framework of adaptable processes, in which concurrent processes can be replaced, suspended, or discarded at runtime. During the seminar, I will propose a session types discipline for a calculus with adaptable processes. Our framework offers an alternative for integrating runtime adaptation mechanisms in the analysis of structured communications. We show that well-typed processes enjoy consistency: communicating behavior is never interrupted by evolvability actions.

Jérôme Feret — Réduction de modèles (slides)

Combinatorial explosion of protein states generated by post-translational modifications and complex formation. Rule-based models provide a powerful alternative to approaches that require an explicit enumeration of all possible molecular species of a system. Such models consist of formal rules stipulating the (partial) contexts for specific protein-protein interactions to occur. These contexts specify molecular patterns that are usually less detailed than molecular species. Yet, the execution of rule-based dynamics requires stochastic simulation, which can be very costly. It thus appears desirable to convert a rule-based model into a reduced system of differential equations by exploiting the lower resolution at which rules specify interactions.In this talk, we present a formal framework for constructing coarse-grained systems. We track the flow of information between different regions of chemical species, so as to detect and abstract away some useless correlations between the state of sites of molecular species.The result of our abstraction is a set of molecular patterns, called fragments, and a system which describes exactly the concentration (or population) evolution of these fragments. The method never requires the execution of the concrete rule-based model and the soundness of the approach is described and proved by abstract interpretation.

Michel Kieffer — Guaranteed characterization of exact non-asymptotic confidence regions

In parameter estimation, it is often desirable to supplement the estimates with an assessment of their quality. Various approaches are available, depending on the hypotheses on the noise corrupting the data and on the nature of the estimator. The approach based on the Cramér-Rao bound and the Fisher information matrix is only valid when the number of data points tends to infinity, unless restrictive conditions are met. When the noise is additive, white, Gaussian, zero mean, and with constant covariance, non-asymptotic posterior distributions of the least-square estimates may be obtained based on differential geometry, as described for instance by Pazman and Pronzato. Sets guaranteed to contain all acceptable values of the parameter vector can be obtained by bounded-error techniques under the hypothesis that bounds are available on the acceptable values of the errors. With this approach, there is no need to assume a specific type of probability distribution for the errors, which may even be deterministic (as when a complex deterministic system is approximated with a simple deterministic model). Moreover the results are guaranteed even if the number of data points is very small. Recently, a new family of methods has been proposed by Campi et al., which makes it possible to obtain exact, non-asymptotic confidence regions for the parameter estimates under relatively mild assumptions on the noise distribution, namely that the noise samples are independently and symmetrically distributed. The numerical characterization of an exact confidence region with this new approach is far from being trivial, however. The aim of this paper is to show how interval analysis, which has been used for a guaranteed characterization of confidence regions for the parameter vector in other contexts, can contribute.

Tristan Legall — Safety Verification of Communicating One-Counter Machines

In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, Fifo channels. This model extends communicating finite-state machines (Cfsm) by infinite-state local processes and an infinite message alphabet. We present a complete characterization of the communication topologies that have a solvable reachability question. As already Cfsm exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization.

Philippe Malbos — Stratégies de normalisation et systèmes de réécriture acycliques (slides)

Cet exposé est un panorama de résultats homologiques et homotopiques en réécriture. Squier a montré que la décidabilité par réécriture du problème du mot dans un monoïde est soumise à des conditions de finitude homotopique et homologique intrinsèques au monoïde. Après avoir rappelé les constructions de Squier, je présenterai des généralisations de la condition homologique utilisée par Squier, ainsi qu'une généralisation de la condition homotopique dans le contexte de la réécriture de dimension supérieure. J'exposerai les raisons pour lesquelles certains résultats homotopiques de convergence en réécriture de mots ne se généralisent pas aux dimensions supérieures de la réécriture. Enfin, j'introduirai la notion de système de réécriture acyclique qui est une notion de modèle cellulaire complet pour les monoïdes, ou les petites catégories, contenant générateurs, relations et dans les dimensions supérieures des syzygies construits par réécriture.

Samuel Mimram — Une modélisation catégorique des systèmes de version de contrôle

When working with distant collaborators on the same files, one often uses a distributed version control system, which is a program tracking the history of files and handles importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations users have performed on files, and it is thus difficult to ensure that all the corner cases have been correctly handled. Here, instead of verifying the implementation of such a system, we adopt a "converse" approach: we introduce a theoretical model, which is defined abstractly by the universal property that it should satisfy, and work out a concrete description of it. We begin by defining a category of files and patches, where the operation of merging the effect of two coinitial patches is defined by pushout. Since the category is not closed under pushouts (two patches can be incompatible), in order to still be able to represent and manipulate files in conflicting states, we investigate the free completion of the category of files under finite colimits, in such a way that existing colimits are preserved, and provide an explicit description of this category. Finally, we introduce a formalization of repositories based on event structures and discuss various generalizations of the model.

Olivier Mullier — General inner-approximation of vector-valued functions (slides)

This presentation addresses the problem of evaluating a subset of the range of a vector-valued function. It is based on a work by Goldsztejn and Jaulin which provides methods based on interval analysis to address this problem when the dimension of the domain and co-domain of the function are equal. This presentation extends this result to vector-valued functions with domain and co-domain of different dimensions. This extension requires the knowledge of the rank of the function Jacobian on the whole domain. This leads to the sub-problem of extracting an interval sub-matrix of maximum rank from a given interval matrix. Approximate solutions are given, based on the Levy-Desplanques theorem, its generalization, and a combinatory method.

Nicolas Ninin — Algèbre des régions cubiques

L'étude de la décomposition de processus concurrent par une interprétation géométrique fait intervenir des régions cubiques et permet de démontrer un théorème de factorisation, théorème obtenu par E. Haucourt et T. Balabonski (Concur 2010). Une axiomatisation des régions cubiques plus générales, élargie à des algèbres de Boole particulières, permet d'élargir naturellement ces résultats à des structures plus riches notamment aux produits de graphes. On utilise pour cela une construction tensorielle dans la catégorie des semi-treillis avec zéros.

Sylvie Putot — Analyse des tests instables dans Fluctuat (slides)

Frank Védrine — Application des traces à l’analyse statique : optimisation, analyse arrière et propriétés compositionnelles (slides)

Cet exposé présente un retour d'expérience sur l'analyse à base de traces implémentée dans l'analyseur de code binaire CFGBuilder. Ce modèle 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. De plus il permet d'effectuer des analyses arrières relativement efficaces ne remontant que sur les dépendances de données intersectées avec les dépendances de contrôle. 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.

Frank Védrine — Représentation graphique des zonotopes - algorithmique d'affichage (slides)

Cet exposé présente des algorithmes de conversion d'équations zonotopiques en un ensemble de points, voire d'arêtes et de faces définissant son enveloppe convexe. Les équations zonotopiques, construites avec n symboles partagés, définissent naturellement 2ⁿ points remarquables correspondant aux instances ε=-1,+1 des symboles partagés. Mais seulement 2n (en dimension 2), au plus n²-n+2 (en dimension 3) d'entre eux font partie de l'enveloppe convexe. Les algorithmes que nous avons implémentés ont une complexité de l'ordre de n×log₂(n) en dimension 2 et de n³×log₂(n) en dimension 3. Si en dimension 2, un algorithme se dégage, en dimension 3, plusieurs alternatives sont pertinentes avec quasiment la même complexité : une première alternative est orientée équation et une seconde est orientée recherche locale des sommets adjacents. Nous soupçonnons que des algorithmes encore plus efficaces (de l'ordre de n²×log(n)) puissent être valides en dimension 3. Bref, cet exposé peut servir de support pour discuter de propriétés et de représentations des zonotopes autres qu'à base d'équations, représentations que nous n'avons finalement que peu l'occasion de manipuler dans nos outils d'analyse statique.

Baptiste Strazulla — Programmation web simplifiée en OCaml

Le sujet de mon exposé est hors-sujet puisqu'il ne concerne ni la modélisation ni l'optimisation ni l'analyse statique. En effet, ayant intégré le LMeASI au CEA récemment, je n'ai pas de travail à présenter dans ces domaines. Du coup, ce que je me propose de présenter est ce sur quoi j'ai travaillé juste avant, pendant mon stage de Master, à savoir Ocsigen, un framework Web écrit en OCaml. Je présenterai donc comment faire de la programmation Web avec un langage fonctionnel comme OCaml ainsi que ce que j'ai produit pendant mon stage.

Participants

1. Manel Abid
2. Assalé Adjé
3. Alexandre Chapoutot
4. Cinzia di Giusto
5. Jérôme Feret
6. Éric Goubault
7. Emmanuel Haucourt
8. Tobias Heindel
9. Michel Kieffer
10. Tristan Legall
11. Philippe Malbos
12. Samuel Mimram
13. Olivier Mullier
14. Nicolas Ninin
15. Sylvie Putot
16. Yassmine Seladji
17. Baptiste Strazzulla
18. Frank Védrine

Éditions précédentes

• En 2010.