La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

Dans cette thèse, nous discutons d’aspects algorithmiques de trois différents problèmes, en lien avec la cryptographie. La première partie est consacrée à l’algèbre linéaire creuse. Nous y présentons un nouvel algorithme de pivot de Gauss pour matrices creuses à coefficients exacts, ainsi qu’une nouvelle heuristique de sélection de pivots, qui rend l’entière procédure particulièrement efficace dans certains cas. La deuxième partie porte sur une variante du problème des anniversaires, avec trois listes. Ce problème, que nous appelons problème 3XOR, consiste intuitivement à trouver trois chaînes de caractères uniformément aléatoires de longueur fixée, telles que leur XOR soit la chaîne nulle. Nous discutons des considérations pratiques qui émanent de ce problème et proposons un nouvel algorithme plus rapide à la fois en théorie et en pratique que les précédents. La troisième partie est en lien avec le problème learning with errors (LWE). Ce problème est connu pour être l’un des principaux problèmes difficiles sur lesquels repose la cryptographie à base de réseaux euclidiens. Nous introduisons d’abord un générateur pseudo-aléatoire, basé sur la variante dé-randomisée learning with rounding de LWE, dont le temps d’évaluation est comparable avec celui d’AES. Dans un second temps, nous présentons une variante de LWE sur l’anneau des entiers. Nous montrerons que dans ce cas le problème est facile à résoudre et nous proposons une application intéressante en re-visitant une attaque par canaux auxiliaires contre le schéma de signature BLISS. / In this thesis, we discuss algorithmic aspects of three different problems, related to cryptography. The first part is devoted to sparse linear algebra. We present a new Gaussian elimination algorithm for sparse matrices whose coefficients are exact, along with a new pivots selection heuristic, which make the whole procedure particularly efficient in some cases. The second part treats with a variant of the Birthday Problem with three lists. This problem, which we call 3XOR problem, intuitively consists in finding three uniformly random bit-strings of fixed length, such that their XOR is the zero string. We discuss practical considerations arising from this problem, and propose a new algorithm which is faster in theory as well as in practice than previous ones. The third part is related to the learning with errors (LWE) problem. This problem is known for being one of the main hard problems on which lattice-based cryptography relies. We first introduce a pseudorandom generator, based on the de-randomised learning with rounding variant of LWE, whose running time is competitive with AES. Second, we present a variant of LWE over the ring of integers. We show that in this case the problem is easier to solve, and we propose an interesting application, revisiting a side-channel attack against the BLISS signature scheme.

Dans cette thèse, nous proposons et évaluons des algorithmes pour résoudre des problèmes d’ordonnancement en ligne. Pendant des décennies, les études en ordonnancement considèrent des modèles déterministes où toutes les informations nécessaires pour la définition du problème sont supposées connues à l’avance. Cette hypothèse n'est généralement pas réaliste. Ceci a motivé les études sur l’ordonnancement en ligne. Dans un problème d’ordonnancement en ligne, un algorithme doit prendre des décisions sans connaissance du futur. L’analyse compétitive est généralement la méthode utilisée pour évaluer les performances de tels algorithmes. Dans cette analyse, la performance d'un algorithme en ligne est mesurée par le ratio compétitif qui est le ratio dans le pire cas entre la performance de la solution obtenue et celle d’une solution optimale hors ligne. Nous considérons principalement deux paradigmes en ligne: celui où les tâches se présentent dans la liste et celui où les tâches arrivent au fur et à mesure. Sur la base de ces deux paradigmes, nous considérons différents modèles : une seule machine, deux machines identiques parallèles, deux machines uniformes parallèles, batch machines et open shop. Pour chacun des problèmes, nous démontrons une borne inférieure de ratios compétitifs et proposons des algorithmes en ligne. Ensuite, nous évaluons la performance de ces algorithmes à l’aide de l’analyse compétitive. Pour certains problèmes, nous montrons que les algorithmes proposés sont optimaux dans le sens où le ratio compétitif est égal à la borne inférieure. / This thesis proposes and evaluates some online algorithms for machine scheduling problems. Deterministic scheduling models have been extensively studied in the literature. One of the basic assumptions of these models is that all the information is known in advance. However, this assumption is usually not realistic. This observation promotes the emergence of online scheduling. In online scheduling problems, an online algorithm has to make decisions without future information. Competitive analysis is a method invented for analyzing online algorithms, in which the performance of an online algorithm (which must satisfy an unpredictable sequence of requests, completing each request without being able to see the future) is compared with the performance of an a posteriori optimal solution where the sequence of requests is known. In the framework of competitive analysis, the performance of an online algorithm is measured by its competitive ratio. We mainly deal with two online paradigms: the one where jobs arrive over list and the one where jobs arrive over time. Based on these two paradigms, we consider different models: single machine, two identical parallel machines, two uniform parallel machines, batch processing machine and open shop. For each of the problems, we prove a lower bound of competitive ratios and propose online algorithms. Then we further measure the worst case performance of these algorithms. For some problems, we can show that the algorithms we proposed are optimal in the sense that their competitive ratios match the lower bounds.

L’objectif de cette thèse est de proposer des méthodes de localisation de mobiles en environnement urbain pour des applications de sécurité civile. Le système de localisation doit alors être basé sur un réseau de récepteurs indépendant de celui des stations de base et autres mobiles. L’objectif visé est de pouvoir localiser avec précision un mobile dans une zone limitée. Pour répondre à ce besoin de localisation ponctuel et immédiat, on considère qu’au plus deux récepteurs (RS) peuvent être déployés. Ces RS sont équipés de réseaux d’antennes permettant l’extraction, par un algorithme de haute résolution (HRA), des caractéristiques géométriques du canal utilisées pour la localisation. L’algorithme de localisation proposé, basé sur une technique d’identification d’empreintes, emploie un modèle de canal déterministe de lancer de rayons. Une caractérisation multidimensionnelle du canal de propagation a d’abord été effectuée pour confronter le modèle avec les canaux expérimentaux. L’algorithme de localisation est testé dans des environnements de synthèse afin de prédire les erreurs de localisation engendrées par l'HRA. Il est ensuite validé expérimentalement sur des configurations de propagation volontairement défavorables. Une approche originale basée sur la diversité de polarisation permet d'améliorer la précision de localisation. Si pour des raisons stratégiques ou financières, il n'est pas envisageable d'utiliser deux RS, un second algorithme de localisation est proposé afin de réduire la zone à explorer en n’utilisant qu’un RS mobile. Il se base sur une technique de tracé de rayons inverse et intègre une phase d’identification des rayons diffractés du canal. / The objective of this thesis is to propose mobile localization methods in urban environments for civil safety/security applications. The localization system must be based on a dedicated network of receivers, independent of the provider base stations and mobiles. The purpose is to accurately locate a mobile in a limited area. To meet this punctual and immediate need of localization, it was considered that at most two receivers (RS) equipped with antenna arrays can be deployed. This allows the extraction of the geometrical characteristics of the channel used for localization by a high resolution algorithm (HRA). The proposed localization algorithm is based on a fingerprinting technique and uses a deterministic ray tracing channel model. First, an experimental multidimensional characterization of the propagation channel was performed to compare with experimental channels. The localization algorithm is tested for synthetic environments in order to predict the localization errors caused by the HRA. Then, it was experimentally validated with deliberately unfavorable propagation configurations, encountered with typical scenarios. An original approach based on polarization diversity allows improving the localization accuracy. If for strategic or financial reasons, it is not possible to use two RS, a second localization algorithm is proposed to reduce the area to be explored, using only one mobile RS. It is based on a reverse ray tracing approach and includes a phase of identification of the diffracted rays of the channel.

L'informatique moderne n'est plus uniquement composée de machines personnelles et de super calculateurs. De nombreux supports de calcul sont maintenant disponibles et chacun pose des contraintes particulières amenant à de nombreux objectifs. Ainsi, la notion de performance d'une application est devenue multi-dimensionnelle. Par exemple, ordonnancer optimalement (en temps) une application sur une grille de calcul est inutile si elle ne fournit pas de résultat parce qu'une machine tombe en panne. Fournir une solution à ces problèmes est un défi algorithmique actuel. Dans ce manuscrit, nous étudions l'ordonnancement multi-objectif à l'aide des outils de la théorie de l'approximation. Nous traitons ainsi quatre problèmes. Les deux premiers sont inspirés des systèmes embarqués, tandis que les deux derniers sont inspirés des problématiques que l'on retrouve sur les grilles et les \textit{clusters}. Le premier problème étudié est l'optimisation des performances d'une application sur une machine disposant de peu de mémoire de stockage. Nous montrons que l'utilisation de l'optimisation multi-objectif permet de fournir une solution et des informations sur le problème que la théorie mono-objectif de l'approximation ne pouvait pas obtenir. Les deux problèmes suivants concernent l'optimisation des performances d'une application lorsque les machines ne sont pas entièrement fiables. Les différents modèles de défaillances amènent à des problèmes d'optimisation radicalement différents. C'est pourquoi le deuxième problème traite de la sûreté de fonctionnement des systèmes embarqués alors que le troisième considère la fiabilité des grilles et \textit{clusters}. Le dernier problème concerne l'utilisation simultanée d'une plate-forme de calcul parallèle par de nombreux utilisateurs. Nous montrons comment l'utilisation de l'optimisation multi-objectif peut permettre de prendre en compte les besoins utilisateurs au sein du processus d'optimisation.

Nous presentons une methode generale de planification : L'algorithme Fil d'Ariane. Cette methode est appliquee au probleme de la planification automatique de trajectoires. L'originalite de la methode reside dans son adaptation automatique a la complexite du probleme pose. La planification automatique de trajectoires est transformee en un probleme d'optimisation d'une fonctionnelle de<br />l'espace des plans dans $R^+$. Cette optimisation permet d'explorer<br />les positions accessibles a partir d'une configuration initiale. La<br />methode ne construit pas l'espace des configurations; par contre, a<br />mesure que le temps passe, une approximation de plus en plus fine de<br />l'espace accessible est construite. Cette approximation est faite par<br />un premier algorithme appele l'algorithme $EXPLORE$ qui garantit la<br />completude pour une resolution donnee de la methode. D'autre part,<br />un deuxieme algorithme, l'algorithme $SEARCH$, permet d'accelerer<br />la recherche d'un chemin et d'atteindre la configuration finale. En<br />resume, la methode proposee permet de construire un planificateur<br />complet pour une resolution donnee qui exploite d'une maniere<br />efficace l'espace des plans pour explorer l'espace des configurations.<br />Nous avons implante deux planificateurs bases sur l'algorithme Fil<br />d'Ariane : le premier est un planificateur de trajectoires pour un<br />robot mobile holonome, et le deuxieme, notre experimentation<br />principale, un planificateur de trajectoires pour un bras manipulateur<br />a six degres de liberte. Pour ce dernier, nous avons realise une<br />implantation de notre algorithme sur une machine massivement<br />parallele et planifie les mouvements d'un bras a 6 degres de<br />liberte.<br />Pour optimiser les fonctions des algorithmes EXPLORE et SEARCH nous<br />avons utilise les algorithmes genetiques. Ces algorithmes<br />sont des methodes d'optimisation stochastiques facilement<br />parallelisables.

Chacun d'entre nous s'est déjà essayé à un jeu combinatoire, tel que les dames ou les échecs. Les jeux les plus connus présentent le double avantage de mêler plaisir ludique et réflexion. L'intérêt que les mathématiciens leur porte réside souvent autour de la recherche d'une stratégie gagnante pour l'un des deux joueurs. Du jeu de Nim jusqu'aux échecs, la complexité de cette recherche est très variable. Dans cette thèse, nous donnons tout d'abord un aperçu des principales étapes du développement de ce domaine, qui a commencé au début des années 1900, et soulignons son étroite corrélation avec des domaines connexes tels que la théorie des nombres, des codes correcteurs d'erreur ou des graphes. Nous nous intéressons ensuite à des variantes de jeux bien connus : le Wythoff's game et le Dots and Boxes. Nous présentons et expliquons les stratégies et positions de jeu favorables au premier et au second joueur. Enfin, nous regardons une version solitaire d'un jeu récent à deux joueurs : le Clobber. Il s'agit d'un casse-tête qui se joue en posant des pierres sur les sommets d'un graphe, et dont le but est de détruire le plus de pierres possibles. Nous donnons des résultats structurels et algorithmiques sur les grilles, les arbres, ou encore les hypercubes.

Les systèmes de reconnaissance automatique de la parole sont de plus en plus répandus et utilisés dans des conditions acoustiques très variées, par des locuteurs très différents. De ce fait, ces systèmes, généralement conçus en laboratoire, doivent être robustes afin de garder des performances optimales en situation réelle. Les travaux que nous avons effectués sont partis de l'idée que si les systèmes de reconnaissance étaient capables de s'auto-modifier dans le temps, afin de s'adapter aux changements de leurs environnements acoustiques, ils pourraient être beaucoup plus robustes. En effet, les organismes vivants ont montré à la fois des capacités à sélectionner les informations utiles et à modifier leur traitement en vue de survivre dans leur environnement. Dans un premier temps, nous avons cherché à adapter le système de reconnaissance lui-même aux différents environnements. Nous avons étudié les capacités du système à s'adapter aux changements de conditions acoustiques, à l'aide d'une approche locale (par rétro-propagation du gradient) et d'une approche globale (par algorithmes évolutionnaires), en vue de trouver un système optimal. Dans un second temps, nous nous sommes placée dans le cadre du traitement des données en entrée du système. Partant d'une base de projection issue d'une analyse en composantes principales, nous avons cherché à trouver à l'aide des algorithmes évolutionnaires une base de projection adaptée à chaque environnement rencontré et permettant de retrouver les conditions acoustiques connues du système. Nous avons mis en place une plate-forme de simulation permettant de faire évoluer des populations de systèmes de reconnaissance. Les résultats obtenus montrent qu'en moyenne l'hybridation des algorithmes évolutionnaires et des techniques de reconnaissance classiques améliore sensiblement, et de manière stable, les performances du système de reconnaissance, et ceci dans les deux types d'hybridation que nous avons testés.

La caractérisation de phase est la pierre angulaire de l'analyse de front d'onde. Devenant un secteur d'activité de plus en plus large, il nécessite de nouveaux moyens de contrôle plus efficaces, plus performants et meilleur marché. Les performances des techniques les plus utilisées dans ce domaine reposent en grande partie sur un équipement optique sophistiqué, alors que l'utilisation de la diffraction par propagation libre permet de simplifier au maximum le matériel et de reporter la charge aux algorithmes intelligents de traitement de données. L'objectif de ce travail est de mettre en valeur une technique d'analyse de front d'onde multivue ainsi que de construire une installation-prototype capable de caractériser les diverses cartes de phase. L'entité de l'étude réalisée consiste à proposer une méthode d'accès à la forme de la phase d'une onde inconnue à partir d'une séquence de ses figures de diffraction créées avec un modulateur spatial de lumière selon le principe des multiples ondes illuminantes. Pour contribuer au problème, un algorithme itératif de type IFTA (Iterative Fourier/Fresnel Transform Algorithm) dit la ``multi-illumination'' a été mis en oeuvre en deux versions qui sous-entendent soit les conditions de l'imagerie cohérente combinée avec une propagation libre, soit une double propagation de Fresnel/Fourier. Le fonctionnement de l'algorithme a été vérifié aussi bien en simulation numérique qu'au sein d'un montage optique experimental gouverné par un logiciel artisanal de pilotage. Les résultats obtenus démontrent sa convergence sûre et particulièrement rapide. Mots-clefs: analyse de front d'onde, reconstruction de phase, modulateur spatial de lumière, multivue, algorithmes iteratifs par transformée de Fourier/Fresnel discrète.

L'objectif de la présente thèse est d'étudier, de définir et de mettre en place un système de vision artificielle permettant de discriminer la nature et la variété de semences à partir de leurs images numériques. Une première étude a porté sur l'étude d'un dispositif mono-caméra destiné au contrôle de la qualité de lots de semences dans l'optique de leur certification. Il est apparu qu'un système mono-caméra ne permettait pas d'identifier les semences dont les faces présentent une disparité de couleur. Ainsi, les semences endommagées ne peuvent pas être correctement détectées avec un tel dispositif. Une deuxième étude a porté sur l'étude et la réalisation d'un nouveau système d'acquisition, muni de trois caméras, et capable de prendre plusieurs images de plusieurs faces d'un même objet. Un prototype a été construit, reposant sur une nouvelle architecture optique et électronique. A l'aide de ce prototype, une collection d'images de semences et de contaminants a été acquise. Sur cette collection, des algorithmes de traitement d'images et de discrimination ont été testés. Les semences composant cette collection ont été caractérisées par plusieurs centaines de variables quantitatives, portant sur leur morphologie, leur couleur et leur texture. Plusieurs méthodes de discrimination ont été étudiées : l'analyse discriminante linéaire (ADL), l'analyse factorielle discriminante, l'analyse discriminante PLS et une méthode de réseau de neurones probabilistes à ajustement adaptatif de poids. Dans tous les cas, les variables ont été sélectionnées préalablement par ADL avec introduction successive des variables les plus discriminantes. L'existence de trois images numériques pour chaque objet étudié offre des possibilités nouvelles en ce qui concerne la prise de décision. Plusieurs heuristiques ont été testées. Nous avons comparé les résultats obtenus en concaténant les tableaux de caractéristiques acquises à l'aide des trois caméras ou en mettant en jeu une stratégie de vote, majoritaire ou unanime. Quelle que soit la stratégie de décision, le réseau de neurones probabilistes donne les résultats les meilleurs, légèrement supérieurs à ceux obtenus par l'ADL. Nous avons conclu que, en considérant la simplicité de l'analyse discriminante linéaire, cette méthode était la plus appropriée pour la réalisation d'un automate fonctionnant en temps réel et capable de répondre aux contraintes de la certification des lots de semences.