L'objectif de cette thèse est d'obtenir une démonstration effective d'un résultat de Cohen, Shiga et Wolfart, généralisant aux espaces de Siegel $\mathfrak{H}_{g}$ de degré $g$ quelconque le théorème classique de Schneider sur l'invariant modulaire $j(\tau)$. Un premier pas dans cette direction consiste, étant donnée une variété abélienne $\mathcal{A}$ définie sur $\overline{\mathbb{Q}}$ et paramétrée par un point $\tau$ de l'espace de Siegel, à minorer $|||\tau-\beta|||$ où $\beta$ est un point algébrique de l'espace de Siegel, en fonction des données géométriques du problème. C'est ce qui est réalisé ici, en affinant des outils d'indépendance linéaire de logarithmes de la méthode de Gel'fond-Baker.

La première partie de cette thèse traite de la manipulation des séries de polynômes orthogonaux classiques par le calcul formel. Grâce à l'approche hypergéométrique, nous obtenons de manière synthétique et constructive des opérateurs aux différences qui définissent les opérations élémentaires sur les séries de polynômes orthogonaux classiques telles que le produit par un polynôme, la dérivation ou l'évaluation des séries partielles. Ces opérations élémentaires sont implémentées en Maple sous forme de primitives à partir desquelles des opérations plus complexes sont construites : application d'un opérateur différentiel, produits de séries et surtout la résolution de problèmes différentiels au moyen de tau-méthodes. Dans le cas des séries de Chebyshev, les résultats de la premiére partie permettent de construire une équation récurrente, dite récurrence de Chebyshev, vérifiée par les coefficients de Chebyshev de toute fonction solution d'une équation différentielle holonome donnée. Divers problèmes relatifs à la construction et à la structure de la récurrence de Chebyshev sont traités. Parallèlement, les solutions de la récurrence de Chebyshev conduisent à la notion de série de Chebyshev formelle solution d'une équation différentielle. Un théorème décrit le comportement asympotique des coefficients d'une telle série qui peut être divergente. Dans certains cas, le lien entre une série de Chebyshev divergente et une fonction toutes deux solutions de la même equation differentielle peut être établi soit par des méthodes de resommation soit par une suite d'intégrales dans le champ complexe.

Le but de cette thèse est de fournir des moyens de calcul et de visualisation d'objets mathématiques issus de l'analyse complexe. Dans ce cadre, de nombreux problèmes d'origine mathématique empêchent d'utiliser les nombres complexes aussi naturellement que les nombres réels : indéterminations dans les calculs, nombre élevé de dimensions empêchant les méthodes naïves de visualisation, phénomènes multiformes. Au niveau calcul, quelques méthodes ont été étudiées, menant à la définition d'un modèle de programmation permettant de gérer les indéterminations. Au niveau visualisation, des méthodes adaptées aux objets mathématiques complexes ont été mises au point, en particulier dans le cadre des solutions d'équations différentielles complexes. Toutes ces méthodes (calcul, visualisation) ont été implémentées sous forme de modules dans un environnement commun permettant le prototypage rapide d'expériences, axées notamment sur un couplage entre calcul et visualisation. Les différentes applications présentées dans le document (intégration numérique d'équations différentielles avec des fonctions multiformes, visualisation de solutions d'équations différentielles complexes, visualisation de l'erreur globale estimée pendant une intégration) y ont été intégrées.

A ce jour, les méthodes formelles ont montré qu'elles étaient applicables avec succès au développement de logiciels industriels. Pour maîtriser la complexité croissante de ces applications, la mise en oeuvre des paradigmes d'abstraction et de composition est incontournable. La méthode B permet d'assister le processus de développement des spécifications au code et offre une notion de modularité qui permet de composer à la fois les spécifications et les développements. La compositionnalité des preuves est assurée par des restrictions imposées par le langage, qui limitent les formes d'architectures autorisées. A la suite de nos précédents travaux, le manuscrit présenté ici explicite les principes de composition des spécifications et des développements, énonce les théorèmes sous-jacents à la composition des preuves et complète et valide les restrictions imposées par la méthode B. Bien que dédiés à la méthode B, les résultats présentés sont plus généraux : ils peuvent s'appliquer à d'autres approches formelles basées sur la notion d'état, comme les approches objet

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d'Isabelle/HOL nous avons fourni une intégration vérifiée d'UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d'Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d'Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié.

Cette thèse traite des systèmes paramétrés. Ils modélisent des applications dans divers domaines, comme la robotique ou la calibration. Soit S un système paramétré. Nous cherchons à décrire les ouverts connexes U de l'espace des paramètres tels que S restreint à U admet un nombre constant de solutions réelles. En robotique, nous détectons les positions cuspidales des robots plan 3-RPR. En calibration photographique, nous décrivons le nombre de solutions réalisables du problème Perspective-3- Points. D'un point de vue théorique, nous montrons que sous certaines hypothèses, le calcul de la variété discriminante d'un système paramétré peut se réduire à un calcul de projection. Dans le cas des systèmes quelconques, nous introduisons la décomposition équidimensionnelle régulière. Notre algorithme possède de bonnes performances en pratique et nous permet par ailleurs de déduire un nouvel algorithme pour le calcul du radical d'un idéal.

Ce travail porte sur le test automatique de systèmes interactifs. L'approche proposée est basée sur des techniques de test de systèmes réactifs synchrones. Le comportement de systèmes synchrones, qui est constitué de cycles commençant par la lecture d'une entrée et finissant par l'émission d'une sortie, est sous certaines conditions, similaire à celui de systèmes interactifs. En particulier, nous étudions l'utilisation de Lutess, un environnement de test synchrone, pour valider les systèmes interactifs. <br />Nous montrons l'intérêt d'utiliser les techniques de test proposées par Lutess afin de générer des scénarios intéressants et nous illustrons leur utilisation sur une étude de cas (une application de réalité virtuelle mobile). <br />Nous avons également étudié la génération de données de test à partir d'arbres de tâches, qui peuvent être enrichis d'une spécification de profils opérationnels. <br />L'adaptation des techniques de test synchrone à la validation d'applications interactives multimodales est également étudiée, notamment en prenant en compte certaines propriétés concernant la multimodalité.

La réécriture algébrique dans les systèmes d'équations<br />différentielles polynomiales consiste à transformer<br />un système d'équations polynomiales différentielles<br />ordinaires ou aux dérivées partielles en un système<br />équivalent, uniquement par manipulations symboliques,<br />sans essayer ni de résoudre les équations sous forme close ni<br />de les intégrer numériquement. Plusieurs algorithmes dédiés à<br />ce domaine ont été mis au point ces quinze dernières années<br />dans l'équipe « calcul formel » du LIFL, dont « Rosenfeld-Gröbner »,<br />que j'ai inventé en 1994 lors de ma thèse de troisième cycle et qui<br />constitue le coeur du paquetage MAPLE diffalg.<br /><br />Le mémoire résume l'activité de recherche que j'ai menée depuis dix ans, soit<br />directement soit en collaboration : approfondir la théorie sous-jacente de<br />l'élimination en algèbre différentielle, lui chercher des applications et<br />la diffuser auprès des scientifiques non spécialistes.<br /><br />Le lecteur trouvera dans le mémoire des approfondissements théoriques<br />sur la notion de solution d'un système différentiel polynomial<br />(théorème de François Lemaire) et la notion de « chaîne différentielle<br />régulière » (leur équidimensionnalité en particulier).<br />Plusieurs nouveaux algorithmes sont présentés : « PARDI » (un cas particulier<br />de Rosenfeld-Gröbner mieux adapté à plusieurs applications),<br />un algorithme de changement d'ordre inspiré de FGLM fondé sur les<br />différentielles de Kähler, « reg-characteristic » et « regalise » qui<br />évitent le recours aux bases de Gröbner dans la deuxième partie de<br />« Rosenfeld-Gröbner ». Ce dernier est clarifié et optimisé.<br /><br />L'équipe « calcul formel » fait partie de l'Institut de Recherche<br />Interdisciplinaire. Les deux applications présentées relèvent<br />des Sciences du Vivant. Elles sont toutes deux menées en collaboration.<br />Il s'agit d'estimation de paramètres (projet LÉPISME avec Lilianne Denis-Vidal<br />et Ghislaine Joly-Blanchard (UTC)) et de modélisation du cycle cellulaire<br />de l'algue verte « ostreococcus tauri » (François-Yves Bouget (Banyuls),<br />Marc Lefranc (Phlam)).<br /><br />Diffuser l'élimination différentielle exige de produire des composants<br />logiciels simples d'emploi. Le mémoire évoque rapidement le paquetage<br />diffalg de MAPLE (interactif, 1996). Il insiste sur BLAD (bibliothèques<br />en langage C, destinées à préparer le travail des intégrateurs numériques)<br />qui a demandé un investissement de plusieurs années. Diffuser l'élimination<br />différentielle exige de produire aussi des documents pédagogiques. Le mémoire<br />lui-même constitue une tentative en ce sens.

Ce mémoire aborde plusieurs domaines :<br />- le calcul de Lie et en particulier les séries de Lie et leurs applications en théorie du contrôle (avec F. JEAN), en mécanique hamiltonienne et dans l'étude de relations dans des groupes ; <br />- l'étude des déformations de groupes triangulaires discrets dans l'espace PU(2,1) des automorphismes<br />de la boule unité complexe de dimension 2 (avec E. FALBEL).<br />- ainsi qu'un travail en collaboration avec Serge GALAM sur l'étude d'un modèle particulier du problème<br />d'Ising triangulaire antiferromagnétique.

Je présente dans ce mémoire un bilan de mon activité scientifique effectuée au sein des groupes POC (Parallèlisation et Optimisation Combinatoire) et SID (Systèmes d'Information Distribués) de l'équipe ROI (Recherche Opérationnelle et Informatique) du laboratoire LAMIH à l'UVHC. <br /><br />Mes travaux de recherche se divisent en trois parties:<br /><br /> - l'étude du problème du sac-à-dos non borné, problème classique de l'optimisation combinatoire, dont nous mettons en évidence des propriétés fondamentales et pour lequel nous avons dérivé, implanté et mis à disposition deux algorithmes qui tirent avantage des propriétés découvertes;<br /><br /> - une approche algorithmique parallèle/distribuée pour la<br /> bio-informatique notamment le problème de repliement de protéïnes qui est un problème reconnu comme l'un des plus difficiles posés à la science informatique dans le contexte de la bio-informatique;<br /><br /> - le développement d'une plate-forme ouverte d'expérimentations pour la méthode formelle B, l'étude de la modularité du langage B et d'extensions de B pour générer des composants logiciels ainsi que l'étude de l' adjonction au langage B d'une logique temporelle.<br /> <br /> Nous montrons comment les approches utilisées dans une recherche en optimisation combinatoire d'une part et en spécification formelle d'autre part peuvent s'enrichir et se féconder mutuellement.