Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L'approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l'industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d'étude, qui s'inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d'une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d'écrire des programmes structurés en composants. L'introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d'alias, on risque de ne plus pouvoir garantir la validité de l'invariant de données d'une structure. Nous interdisons, alors l'aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s'inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d'obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d'obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s'apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu'aucun invariant de données n'est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l'affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d'un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires.

La visualisation interactive est un outil essentiel pour l'exploration, la compréhension et l'analyse de données. L'exploration interactive efficace de jeux de données grands ou complexes présente cependant deux difficultés fondamentales. La première est visuelle et concerne les limitations de la perception et cognition humaine, ainsi que celles des écrans. La seconde est computationnelle et concerne les limitations de capacité mémoire ou de traitement des machines standards. Dans cette thèse, nous nous intéressons aux techniques de passage à l'échelle relativement à ces deux difficultés, pour plusieurs contextes d'application.Pour le passage à l'échelle visuelle, nous présentons une approche versatile de mise en évidence de sous-ensembles d'éléments par déformation spatiale appliquée aux vues multiples et une représentation abstraite et multi-/échelle de coordonnées parallèles. Sur les vues multiples, la déformation spatiale vise à remédier à la diminution de l'efficacité de la surbrillance lorsque les éléments graphiques sont de taille réduite. Sur les coordonnées parallèles, l'abstraction multi-échelle consiste à simplifier la représentation tout en permettant d'accéder interactivement au détail des données, en les pré-agrégeant à plusieurs niveaux de détail.Pour le passage à l'échelle computationnelle, nous étudions des approches de pré-calcul et de calcul à la volée sur des infrastructures distribuées permettant l'exploration de jeux de données de plus d'un milliard d'éléments en temps interactif. Nous présentons un système pour l'exploration de données multi-dimensionnelles dont les interactions et l'abstraction respectent un budget en nombre d'éléments graphiques qui, en retour, fournit une borne théorique sur les latences d'interactions dues au transfert réseau entre client et serveur. Avec le même objectif, nous comparons des stratégies de réduction de données géométrique pour la reconstruction de cartes de densité d'ensembles de points. / Interactive visualization is helpful for exploring, understanding, and analyzing data. However, increasingly large and complex data challenges the efficiency of visualization systems, both visually and computationally. The visual challenge stems from human perceptual and cognitive limitations as well as screen space limitations while the computational challenge stems from the processing and memory limitations of standard computers.In this thesis, we present techniques addressing the two scalability issues for several interactive visualization applications.To address visual scalability requirements, we present a versatile spatial-distortion approach for linked emphasis on multiple views and an abstract and multi-scale representation based on parallel coordinates. Spatial distortion aims at alleviating the weakened emphasis effect of highlighting when applied to small-sized visual elements. Multiscale abstraction simplifies the representation while providing detail on demand by pre-aggregating data at several levels of detail.To address computational scalability requirements and scale data processing to billions of items in interactive times, we use pre-computation and real-time computation on a remote distributed infrastructure. We present a system for multi-/dimensional data exploration in which the interactions and abstract representation comply with a visual item budget and in return provides a guarantee on network-related interaction latencies. With the same goal, we compared several geometric reduction strategies for the reconstruction of density maps of large-scale point sets.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L’approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l’industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d’étude, qui s’inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d’une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d’écrire des programmes structurés en composants. L’introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d’alias, on risque de ne plus pouvoir garantir la validité de l’invariant de données d’une structure. Nous interdisons, alors l’aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s’inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d’obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d’obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s’apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu’aucun invariant de données n’est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l’affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d’un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires. / The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise between the complexe methods that exist in the literature and what is used in industry, reconciling lightness annotations and restrictions on the alias. We define, firstly, a language study, based on the C language, in which the only type of mutable data allowed is the type of structures, which can be accessed only through pointers. In order to structure our programs, we bring our language with a module notion and concepts issue from a refinement theory such as abstract variables that we formalize by model fields and gluing invariants. This allows us to write programs structured by components. Introducing invariants in our language raises issues related to aliasing. Indeed, in presence of alias, we might not be able to guarantee the validity of the invariant data structure. We forbid then the aliasing in our language. To control memory access, we define a type system based on the concept of regions. This contribution is based on the theory and refinement. It aims to make programs as modular as possible and proofs as automatic as possible. We define on this language, a mechanism for generation of proof obligations by proposing a weakest precondition calculus incorporating refinement. Next we prove the correction of this proof obligations generation mechnaism by an original method based on the concept of blocking semantic, which is similar to a proof of type soundness, and consists therefore, to proove the preservation and the progress of the defined calculus. Secondly, we extend our language by, partially, lifting the restrictions related to aliasing. We allow, in particular, sharing when no invariant is associated to the referenced data structure. In addition, we introduce the type of arrays, global variables, and assignment that are not part of the core language. For each of the extensions mentioned above, we extend the definition and correctness proof of the weakest precondition calculus accordingly. Finally, we propose an implementation of this approach as a Frama-C plugin(http ://frama-c.com/). We experimente our implantation on examples of modules implementing complex data structures, especially the challenges from the challenge VACID0 (http ://vacid. Codeplex.com /), namely sparse srrays and binary heaps.