Les fournisseurs de services de cloud computing, les réseaux sociaux et les entreprises de gestion des données ont assisté à une augmentation considérable du volume de données qu'ils reçoivent chaque jour. Toutes ces données créent des nouvelles opportunités pour étendre la connaissance humaine dans des domaines comme la santé, l'urbanisme et le comportement humain et permettent d'améliorer les services offerts comme la recherche, la recommandation, et bien d'autres. Ce n'est pas par accident que plusieurs universitaires mais aussi les médias publics se référent à notre époque comme l'époque "Big Data". Mais ces énormes opportunités ne peuvent être exploitées que grâce à de meilleurs systèmes de gestion de données. D'une part, ces derniers doivent accueillir en toute sécurité ce volume énorme de données et, d'autre part, être capable de les restituer rapidement afin que les applications puissent bénéficier de leur traite- ment. Ce document se concentre sur ces deux défis relatifs aux "Big Data". Dans notre étude, nous nous concentrons sur le stockage de sauvegarde (i) comme un moyen de protéger les données contre un certain nombre de facteurs qui peuvent les rendre indisponibles et (ii) sur le placement des données sur des systèmes de stockage répartis géographiquement, afin que les temps de latence perçue par l'utilisateur soient minimisés tout en utilisant les ressources de stockage et du réseau efficacement. Tout au long de notre étude, les données sont placées au centre de nos choix de conception dont nous essayons de tirer parti des propriétés de contenu à la fois pour le placement et le stockage efficace.

Les mots constituent l'un des fondements des langues naturelles de type indo-européenne. Des corpus rédigés avec ces langues sont alors naturellement décrits avec des mots. Cependant, l'information qu'ils véhiculent seuls est assez réduite d'un point de vue sémantique. Il est en effet primordial de prendre en compte la complexité de ces langues comme par exemple leurs propriétés syntaxiques, lexicales et sémantiques. Nous proposons dans cette thèse de prendre en considération ces propriétés en décrivant un corpus par le biais d'informations syntaxiques permettant de découvrir des connaissances sémantiques. Nous présentons dans un premier temps un modèle de sélection de descripteurs SelDe. Ce dernier se fonde sur les objets issus des relations syntaxiques d'un corpus. Le modèle SelDe a été évalué pour des tâches de classification de données textuelles. Pour cela, nous présentons une approche d'expansion de corpus, nommée ExpLSA, dont l'objectif est de combiner les informations syntaxiques fournies par SelDe et la méthode numérique LSA. Le modèle SelDe, bien que fournissant des descripteurs de bonne qualité, ne peut être appliqué avec tous types de données textuelles. Ainsi, nous décrivons dans cette thèse un ensemble d'approches adaptées aux données textuelles dites complexes. Nous étudions la qualité de ces méthodes avec des données syntaxiquement mal formulées et orthographiées, des données bruitées ou incomplètes et finalement des données dépourvues de syntaxe. Finalement un autre modèle de sélection de descripteurs, nommé SelDeF, est proposé. Ce dernier permet de valider de manière automatique des relations syntaxiques dites “induites”. Notre approche consiste à combiner deux méthodes. Une première approche fondée sur des vecteurs sémantiques utilise les ressources d'un thésaurus. Une seconde s'appuie sur les connaissances du Web et des mesures statistiques afin de valider les relations syntaxiques. Nous avons expérimenté SelDeF pour une tâche de construction et d'enrichissement de classes conceptuelles. Les résultats expérimentaux montrent la qualité des approches de validation et reflètent ainsi la qualité des classes conceptuelles construites.

Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat.

La prise en compte de la complexité croissante des systèmes embarqués temps réel, le besoin de formalisation du processus de développement, les contraintes inhérentes de ces systèmes (ressources limitées et spécifiques, prédictibilité, correction) font qu'il est nécessaire de pouvoir disposer d'un support permettant une maîtrise fine du processus de développement et une gestion sûre des ressources utilisées par le système. L'utilisation des principes de génie logiciel doit permettre de répondre au défi de la maîtrise et de l'amélioration des processus de développement. L'intégration des techniques formelles doit permettre d'assurer la correction des applications produites. Dans les études présentées, nous nous intéressons aux architectures opérationnelles utilisant les services d'un exécutif multitâches. Dans ce cadre, nous avons plus particulièrement exploré deux thèmes. Le premier porte sur l'utilisation des langages SDL et IF et des techniques formelles par modélisation exhaustive pour assurer la correction des systèmes. Le deuxième porte sur l'utilisation du paradigme composant pour la structuration des politiques de gestion de la QdS dans un contexte fortement dynamique. Dans les premiers travaux, un premier niveau, dit de spécification, exprimé en SDL, permet de formaliser les propriétés attendues du système. Ensuite, on décrit, toujours à l'aide de SDL, l'architecture opérationnelle du système par instanciation de boîtes grises, décrivant le comportement des entités du système (tâches, routines). Les modèles IF correspondant fournissent une sémantique d'écoulement du temps. Enfin, les LTS, générés à partir de IF, servent de base à la validation et à la vérification du système. Pour la validation, il faut s'assurer que la mise en place de l'architecture opérationnelle n'aboutit pas à la perte ou à l'activation d'actions non souhaitées. Pour cela nous avons proposé une relation d'équivalence originale qui considère les phénomènes de mémorisation et de décalage temporels inhérent à l'implémentation. Pour la vérification des échéances, l'approche s'appuie sur un modèle réaliste, non abstrait, de l'implémentation (routines d'interruption, sémaphores, boîtes aux lettres, ...) et propose des règles de modélisation et d'abstraction pour contenir le phénomène d'explosion combinatoire (ordre partiel, priorité des tâches, modes de fonctionnement). La vérification, considérant un modèle fin du code, permet par la même occasion de traiter diverses propriétés de sûreté du code (pas de débordement des boîtes aux lettres, ...). Après avoir étudié les langages formels pour décrire et valider des architectures opérationnelles, nous nous intéressons à la structuration à base de composants pour la prise en compte de contraintes de QdS. Dans ce cadre, Fractal et son framework pour l'embarqué Think permettent de construire des systèmes flexibles et adaptables pour les systèmes embarqués. Notre proposition, notée Qinna, permet d'étendre ces modèles pour intégrer des politiques de gestion de la QdS liées à l'utilisation de ressources matérielles. Les expérimentations de Qinna nous ont amené à définir des principes de mise en œuvre, soit des compromis, effectué par le concepteur du système, entre un gaspillage de QdS (discrétisation du niveau de QdS contractualisé) et un nombre important d'opérations d'adaptation à réaliser par l'architecture (suivi de la variabilité des profils de QdS requis et des capacités des ressources matérielles, niveau de QdS contractualisé proche du niveau réel utilisé). Enfin, dans une dernière partie de perspectives, nous donnons des éléments pour étendre les études menées aux architectures applicatives et au plus généralement au problème du déploiement. Dans ce cadre, nous proposons des extensions pour le domaine des systèmes d'acquisition et de communication de données.

In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex. Our Coq implementation is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, we have taken special care with performance in our implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.

Le cadre général de cette thèse est l'indexation sémantique et la recherche d'informations, appliquée à des documents multimédias. Plus précisément, nous nous intéressons à l'indexation sémantique des concepts dans des images et vidéos par les approches d'apprentissage actif, que nous utilisons pour construire des corpus annotés. Tout au long de cette thèse, nous avons montré que les principales difficultés de cette tâche sont souvent liées, en général, à l'fossé sémantique. En outre, elles sont liées au problème de classe-déséquilibre dans les ensembles de données à grande échelle, où les concepts sont pour la plupart rares. Pour l'annotation de corpus, l'objectif principal de l'utilisation de l'apprentissage actif est d'augmenter la performance du système en utilisant que peu d'échantillons annotés que possible, ainsi minimisant les coûts de l'annotations des données (par exemple argent et temps). Dans cette thèse, nous avons contribué à plusieurs niveaux de l'indexation multimédia et nous avons proposé trois approches qui succèdent des systèmes de l'état de l'art: i) l'approche multi-apprenant (ML) qui surmonte le problème de classe-déséquilibre dans les grandes bases de données, ii) une méthode de reclassement qui améliore l'indexation vidéo, iii) nous avons évalué la normalisation en loi de puissance et de l'APC et a montré son efficacité dans l'indexation multimédia. En outre, nous avons proposé l'approche ALML qui combine le multi-apprenant avec l'apprentissage actif, et nous avons également proposé une méthode incrémentale qui accélère l'approche proposé (ALML). En outre, nous avons proposé l'approche de nettoyage actif, qui aborde la qualité des annotations. Les méthodes proposées ont été tous validées par plusieurs expériences, qui ont été menées et évaluées sur des collections à grande échelle de l'indice de benchmark internationale bien connue, appelés TRECVID. Enfin, nous avons présenté notre système d'annotation dans le monde réel basé sur l'apprentissage actif, qui a été utilisé pour mener les annotations de l'ensemble du développement de la campagne TRECVID en 2011, et nous avons présenté notre participation à la tâche d'indexation sémantique de cette campagne, dans laquelle nous nous sommes classés à la 3ème place sur 19 participants.

Since 2006, deep learning algorithms which rely on deep architectures with several layers of increasingly complex representations have been able to outperform state-of-the-art methods in several settings. Deep architectures can be very efficient in terms of the number of parameters required to represent complex operations which makes them very appealing to achieve good generalization with small amounts of data. Although training deep architectures has traditionally been considered a difficult problem, a successful approach has been to employ an unsupervised layer-wise pre-training step to initialize deep supervised models. First, unsupervised learning has many benefits w.r.t. generalization because it only relies on unlabeled data which is easily found. Second, the possibility to learn representations layer by layer instead of all layers at once improves generalization further and reduces computational time. However, deep learning is a very recent approach and still poses a lot of theoretical and practical questions concerning the consistency of layer-wise learning with many layers and difficulties such as evaluating performance, performing model selection and optimizing layers. In this thesis we first discuss the limitations of the current variational justification for layer-wise learning which does not generalize well to many layers. We ask if a layer-wise method can ever be truly consistent, i.e. capable of finding an optimal deep model by training one layer at a time without knowledge of the upper layers. We find that layer-wise learning can in fact be consistent and can lead to optimal deep generative models. To do this, we introduce the Best Latent Marginal (BLM) upper bound, a new criterion which represents the maximum log-likelihood of a deep generative model where the upper layers are unspecified. We prove that maximizing this criterion for each layer leads to an optimal deep architecture, provided the rest of the training goes well. Although this criterion cannot be computed exactly, we show that it can be maximized effectively by auto-encoders when the encoder part of the model is allowed to be as rich as possible. This gives a new justification for stacking models trained to reproduce their input and yields better results than the state-of-the-art variational approach. Additionally, we give a tractable approximation of the BLM upper-bound and show that it can accurately estimate the final log-likelihood of models. Taking advantage of these theoretical advances, we propose a new method for performing layer-wise model selection in deep architectures, and a new criterion to assess whether adding more layers is warranted. As for the difficulty of training layers, we also study the impact of metrics and parametrization on the commonly used gradient descent procedure for log-likelihood maximization. We show that gradient descent is implicitly linked with the metric of the underlying space and that the Euclidean metric may often be an unsuitable choice as it introduces a dependence on parametrization and can lead to a breach of symmetry. To mitigate this problem, we study the benefits of the natural gradient and show that it can restore symmetry, regrettably at a high computational cost. We thus propose that a centered parametrization may alleviate the problem with almost no computational overhead.

The intended goal of this manuscript is to build bridges between two definitions of complexity. One of them, called the algorithmic complexity is well-known to any computer scientist as the difficulty of performing some task such as sorting or optimizing the outcome of some system. The other one, etymologically closer from the word "complexity" is about what happens when many parts of a system are interacting together. Just as cells in a living body, producers and consumers in some non-planned economies or mathematicians exchanging ideas to prove theorems. On the algorithmic side, the main objects that we are going to use are two models of computations, one called communication protocols, and the other one circuits. Communication protocols are found everywhere in our world, they are the basic stone of almost any human collaboration and achievement. The definition we are going to use of communication reflects exactly this idea of collaboration. Our other model, circuits, are basically combinations of logical gates put together with electrical wires carrying binary values, They are ubiquitous in our everyday life, they are how computers compute, how cell phones make calls, yet the most basic questions about them remain widely open, how to build the most efficient circuits computing a given function, How to prove that some function does not have a circuit of a given size, For all but the most basic computations, the question of whether they can be computed by a very small circuit is still open. On the other hand, our main object of study, cellular automata, is a prototype of our second definition of complexity. What "does" a cellular automaton is exactly this definition, making simple agents evolve with interaction with a small neighborhood. The theory of cellular automata is related to other fields of mathematics, such as dynamical systems, symbolic dynamics, and topology. Several uses of cellular automata have been suggested, ranging from the simple application of them as a model of other biological or physical phenomena, to the more general study in the theory of computation.

La thématique de la navigation autonome constitue l'un des principaux axes de recherche dans le domaine des véhicules intelligents et des robots mobiles. Dans ce contexte, on cherche à doter le robot d'algorithmes et de méthodes lui permettant d'évoluer dans un environnement complexe et dynamique, en toute sécurité et en parfaite autonomie. Dans ce contexte, les algorithmes de localisation et de cartographie occupent une place importante. En effet, sans informations suffisantes sur la position du robot (localisation) et sur la nature de son environnement (cartographie), les autres algorithmes (génération de trajectoire, évitement d'obstacles ...) ne peuvent pas fonctionner correctement. Nous avons centré notre travail de thèse sur une problématique précise : développer un algorithme de SLAM simple, rapide, léger et limitant les erreurs de localisation et de cartographie au maximum sans fermeture de boucle. Au cœur de notre approche, on trouve un algorithme d'IML : Incremental Maximum Likelihood. Ce type d'algorithmes se base sur une estimation itérative de la localisation et de la cartographie. Il est ainsi naturellement divergent. Le choix de l'IML est justifié essentiellement par sa simplicité et sa légèreté. La particularité des travaux réalisés durant cette thèse réside dans les différents outils et algorithmes utilisés afin de limiter la divergence de l'IML au maximum, tout en conservant ses avantages.

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.