Nous nous intéressons dans cette thèse à l'estimation, dans un cadre non paramétrique, d'une fonction de régression présentant des discontinuités et, plus précisément aux pro\-blè\-mes de détection de ruptures, d'estimation des paramètres de rupture (nombre, localisations, amplitudes) et de segmentation de la fonction de régression (reconstitution de la fonction). La méthode utilisée est basée sur les propriétés du processsus de saut estimé, $\hat(\gamma)(t)$, défini en tout $t$ comme la différence entre un estimateur à droite et un estimateur à gauche, ces estimateurs étant obtenus régression linéaire locale.\par Dans un premier temps, nous considérons la situation d'une seule discontinuité et étudions les propriétés de l'estimateur de l'amplitude de la discontinuité lorsque la localisation est connue. Nous donnons l'expression de l'erreur quadratique moyenne asymptotique et montrons la convergence et la normalité asymptotique de l'estimateur. Lorsque la localisation $\tau$ n'est pas connue, nous construisons un estimateur de $\tau$ à l'aide du processus de déviation locale associé à $\hat(\gamma)(t)$ et montrons que cet estimateur converge avec une vitesse en $n^(-1)$ ou arbitrairement proche de $n^(-1)$ selon le noyau utilisé. Nous proposons ensuite trois tests d'existence d'une rupture : un test strictement local, un test local et un test global, tous trois définis en terme d'une statistique construite à l'aide du processus de saut estimé. Concernant le problème d'estimation du nombre de ruptures nous élaborons une procédure permettant à la fois d'estimer le nombre $p$ de ruptures et les localisations $\tau_1,\dots,\tau_p$. Nous montrons la convergence presque sûre de ces estimateurs et donnons aussi des résultats sur les vitesses de convergence. Enfin nous proposons une méthode de reconstitution d'une fonction de régression présentant des discontinuités basée sur la segmentation des observations. Nous montrons qu'en utilisant la procédure d'estimation du nombre de ruptures et des localisations développée auparavant, nous obtenons un estimateur de la fonction de régression qui a la même vitesse de convergence qu'en l'absence de ruptures. Des expérimentations numériques sont fournies pour chacun des problèmes étudiés de manière à mettre en évidence les propriétés des procédures étudiées et leur sensibilité aux divers paramètres.

Ce travail porte sur l'étude théorique et numérique des splines de Chebyshev. Ces fonctions généralisent les splines polynomiales tout en préservant l'essentiel de leurs propriétés. Elles offrent de plus un intérêt particulier pour le design géométrique grâce aux paramètres de forme qu'elles fournissent. Dans un premier temps, nous étudions les splines basées sur un espace de Chebyshev invariant par translations, et les propriétés de la B-spline correspondante. Dans un deuxième temps, nous montrons, sous certaines hypothèses, que la base des B-splines de Chebyshev est orthonormale dans un espace de Sobolev pondéré par une suite unique de nombres positifs. La meilleure approximation dans l'espace de splines de Chebyshev au sens de la norme associé au produit scalaire précédent est alors un projecteur local. Enfin, pour l'implémentation numérique des résultats précédents, nous utilisons une méthode de quadratures adaptées. Quelques exemples illustrant les effets de forme obtenus sont présentés. Ces résultats généralisent un résultat prouvé récemment par Ulrich Reif dans le cas particulier des splines polynomiales.

L'utilisation des méthodes formelles pour la conception de protocoles de télécommunication est désormais reconnue comme la seule approche en mesure de garantir leur bon fonctionnement avant la mise en service. Cependant, la complexité toujours croissante ainsi que les contraintes de fiabilité et de sûreté de plus en plus sévères nécessitent l'extension des formalismes de description et l'amélioration continue des méthodes et des techniques de validation. Cette thèse définit une représentation intermédiaire nommé IF pour la description de protocoles. IF est construit à base d'automates temporisés communicants à échéances. Les échéances permettent la modélisation explicite de l'urgence des actions et sont un moyen très fin pour décrire l'évolution temporelle d'un système. Les automates communiquent soit de manière asynchrone, par files d'attente, soit de manière synchrone par rendez-vous. La sémantique opérationnelle de IF est formellement définie et des techniques de simulation efficaces sont proposées. De plus, ayant une structure statique, IF permet l'application intensive des techniques d'analyse statique, comme par exemple celles issues du domaine de l'optimisation de code. Certains informations calculées de cette manière peuvent améliorer considérablement les performances de la validation automatique. Une plate-forme ouverte de validation a été mise en place autour de IF. Elle intègre un grand nombre d'outils autant académiques que industriels et couvre la plupart des techniques actuellement employées pour la vérification et le test des protocoles. Cette plate-forme a été utilisée avec beaucoup de succès sur des protocoles de communication réels, comme par exemple SSCOP ou STARI.

Un automate temporisé est un automate augmenté avec plusieurs horloges qui mesurent le passage de temps et peuvent conditionner la modification de l'état du système. Les automates temporisés ont été introduits en tant que modèle formel pour les systèmes temps-réel, en espérant que leur rôle dans la vérification de tels systèmes sera similaire au rôle des automates finis dans la recherche systématique des erreurs de conception de systèmes non-temporisés. Dans notre thèse nous étudions plusieurs questions théoriques liés aux automates temporisés et aux langages temporisés. Dans une première partie nous étudions une sous-classe simple d'automates temporisés à une seule horloge qui est remise à zéro pendant chaque transition. Nous montrons que cette sous-classe supporte des résultats similaires à la théorie classique des automates finis: des théorèmes de Kleene, de Myhill-Nerode et de fermeture par complémentation. La deuxième et principale partie de la thèse est motivée par les expressions régulières temporisés de Asarin, Caspi et Maler. Depuis leur introduction, on sait qu'il faut employer l'intersection dans les expressions régulières pour que leur expressivité soit égale aux automates temporisés. Nous poursuivons alors une approche alternative en utilisant des parenthèses colorées pour définir les contraintes temporelles sur une séquence d'événements. Cette idée aboutit à une représentation alternative des langage des automates temporisés, basée sur une nouvelle classe de langages formels que nous appelons . Nous développons alors la théorie des expressions régulières sur les regminos et nous montrons que le problème de sémantique vide est indécidable en cas général, et décidable pour une sous-classe large de langages. L'application de ces résultats nous amène à des nouvelles structures de données et à des algorithmes pour le problème du langage vide dans les automates temporisés et les expressions régulières.

Le but principal de ce manuscrit est de montrer que certaines familles de graphes sont des graphes plongeables dans l'hypercube. Un problème d'une autre nature sera traité, il concerne la partition de l'hypercube en des cycles sommet-disjoints de longueur paires. Nous prouvons que l'hypercube de dimension n peut être partitionné en k cycles sommet-disjoints si k

Ce travail présente l'apport de l'ordonnancement pour la programmation parallèle performante d'applications numériques en mécanique et chimie quantique. Nous prenons deux exemples types de résolution de l'équation de Schrödinger --- Boîte Quantique (BQ) et Méthode des Perturbations d'ordre 2 (MP2) --- qui nécessitent de grosses ressources en calcul et mémoire. La programmation traditionnelle (échange de messages et/ou multithreading) des machines parallèles (distribuées ou SMP) est illustrée par les performances obtenues avec le benchmark Linpack sur la grappe I-cluster (INRIA). Le manque de portabilité du code hautement performant obtenu montre l'importance d'un environnement de programmation parallèle permettant de découpler le codage de l'algorithme de son ordonnancement sur la machine cible. Nous introduisons alors Athapascan, qui repose sur l'analyse du flot de données, pour calculer dynamiquement des ordonnancements prouvés efficaces. Un premier critère d'efficacité est le temps de calcul. Sur certains modèles de machines, la théorie et l'expérience montrent que Athapascan permet des ordonnancements qui garantissent des exécutions efficaces pour certains algorithmes adaptés à BQ, de type itératif (méthode de Lanczos). Un deuxième critère fondamental est l'espace mémoire requis pour les exécutions parallèles en calcul numérique ; c'est particulièrement critique pour MP2. Nous proposons d'annoter le Graphe de Flot de Données (GFD) manipulé par Athapascan pour prendre en compte la mémoire et permettre des ordonnancements dynamiques efficaces en mémoire. Pour MP2, dont le GFD est connu statiquement, un ordonnancement efficace en temps et en mémoire est donné.

Les arrangements de droites du plan sont étudiés en géométrie algorithmique pour leur simplicité géométrique couplée à leur grande richesse combinatoire, ou topologique. Notre contribution porte en partie sur la recherche de structures de données couplées à des algorithmes, efficaces à la fois pour la construction des arrangements et l'exploitation de l'information minimale les définissant. Mais l'apport principal de notre travail est l'étude de la représentation géo-métrique des arrangements, notamment par la définition d'une équivalence géométrique entre deux ensembles de droites du plan euclidien par isotopie, qui justifie théoriquement l'algorithme d'optimisation géométrique que nous proposons. Cet algorithme se base sur des critères de ``lisibilité'' de la représentation d'un arrangement, que nous proposons et justifions. Nous donnons également des résultats d'optimisation analytique pour les très petits nombres de droites.

Améliorer la connaissance des circulations dans les océans est d'une importance majeure pour la prévision à court et moyen terme de l'évolution du système climatique, ainsi que pour le développement de l'océanographie cotière et de l'océanographie opérationnelle. Les sources d'information disponibles pour accéder à cette connaissance sont, comme en météorologie, les modèles physiques et numériques et les observations. Dans ce contexte, ce mémoire résume l'essentiel de mes travaux de recherche de ces dernieres années, consacrés à la modélisation numérique et l'assimilation de données pour l'océanographie. J'y présente tout d'abord quelques aspects concernant les schémas utilisés dans les modèles numériques. On s'intéresse ensuite au raffinement, éventuellement adaptatif de maillage dans ces modèles, et à son extension naturelle vers le couplage de modèles. Enfin, la dernière partie est consacrée aux méthodes d'assimilation de données, qui visent à fournir un compromis optimal entre observations et prévisions du modèle, et plus particulièrement au développement de méthodes de rang réduit.

Non disponible

Dans les deux dernières décennies, le logiciel libre a pris un essor considérable. Des distributions qui au début comptaient une centaine de paquets, en ont maintenant des dizaines de milliers, tous de provenance très différente. Ceci engendre des problèmes pour la gestion de qualité. Les outils et procédures ne sont plus adaptés à la taille et la complexité des distributions d'aujourd'hui. Dans cette thèse, nous commençons par présenter une modélisation mathématique des points communs entre les différents types de distribution (Debian et RPM); notamment le concept des paquets et des relations qui existent entre eux: les dépendances et les conflits. Cette modélisation est en partie formalisé avec l'assistant de preuves Coq. Cette modélisation sera ensuite utilisée pour proposer des relations 'sémantiques', qui sont plus adaptés que les relations existantes pour repérer et corriger des erreurs dans les distributions. Nous présentons aussi des algorithmes pour calculer ces relations d'une façon efficace, et nous utiliserons Coq pour prouver formellement les théorèmes les plus importantes utilisées par ces algorithmes. Finalement, nous avons validé les algorithmes sur des distributions existantes. Nous présenterons une analyse de la structure des distributions qui est le résultat de cette validation, ainsi qu'une discussion de la phénomène du "petit monde" en rapport avec les distributions.