De nombreux travaux ont montré l'importance de l'interpolation de Craig pour la structuration et la modularité des spécifications de type axiomatique. En vue d'en donner des conditions suffisantes dans un cadre théorique adapté à l'informatique, nous nous sommes intéressé à une propriété équivalente à l'interpolation de Craig dans le cadre de la théorie standard des modèles : la consistance de Robinson. L'étude de cette dernière propriété nous a amené à généraliser dans une spécialisation des institutions les notions classiques de diagrammes complets et de morphismes élémentaires. Ceci nous a alors permis de généraliser quelques résultats classiques de théorie des modèles tels que les théorèmes de Löwenheim-Skolem ou l'union de chaînes de Tarski. En fin, les constructeurs de formules étant explicites dans notre cadre théorique, nous nous sommes naturellemant intéressés à la combinaison de logiques et à la préservation de l'interpolation de Craig et de la consistance de Robinson.

Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de<br />techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.<br />Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.<br />Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.<br />Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui<br />confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.<br />Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.<br />Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.

Dans cette thèse, on commence par présenter l'étude d'un système dynamique isométrique par morceaux généralisant un exemple connu. On montre qu'il exhibe une infinité de points périodiques hiérarchisés par une structure auto-similaire. L'application de premier retour dans un de ses atomes est une isométrie par morceaux définie sur une partition auto-similaire comportant une infinité d'atomes dont le temps de retour croit exponentiellement. L'auto-similarité observée n'est que partielle, elle ne décrit pas toute la dynamique, mais elle est préservée quand on varie le paramètre principal de manière continue. Cela permet d'identifier les conditions sous lesquelles une auto-similarité est possible. On dégagera ainsi des hypothèses générales qui ont de nombreuses conséquences intéréssantes. En particulier, outre l'existence éventuelle de familles de cellules périodiques descriptibles par un schéma substitutif, on montrera qu'il doit exister un ensemble non vide de points apériodiques. Cet ensemble est fractal, il peut être construit comme un attracteur d'I.F.S graphe-dirigé et sa dimension de Hausdorff peut être calculée. On montrera aussi que la structure géométrique amène tout naturellement à coder la dynamique par une application de Vershik sur un diagramme de Bratteli stationnaire, uni-ergodique sous des conditions naturelles de primitivité. Ce codage particulier peut être "traduit" dans le langage standard de l'application. Cette dynamique symbolique-ci est alors un système substitutif.\\ Le cadre présenté est suffisament général pour englober la plupart des cas particuliers étudiés jusqu'alors. A titre d'application, on l'utilise pour montrer que le système cité ci-dessus possède une mesure invariante dotée d'une infinité de composantes ergodiques.

Cette étude décrit la mise au point de la synthèse de poly( -caprolactone) dans le dioxyde de carbone supercritique (scCO2). Utilisant des isopropanolates d'aluminium, d'yttrium et de lanthane comme amorceurs, la poly( -caprolactone) a été synthétisée dans le scCO2. Les rendements obtenus varient énormément, selon les amorceurs et les conditions de polymérisation. Afin de mieux comprendre le mécanisme mis en jeu, une étude plus complète portant sur l'état thermodynamique du système et les interactions microscopiques a été initiée. Des mesures de point trouble pour des mélanges (monomère / CO2, polymère / CO2, monomère / polymère / CO2) ont été effectuées à l'aide d'une cellule PVT équipée de deux fenêtres en saphirs, conduisant à l'établissement des diagrammes de phase pour ces systèmes. De plus, les mélanges amorceurs/CO2 ont été étudiés par spectroscopie infra-rouge dans le scCO2 et différents types d'interactions entre l'alcoolate de métal et le CO2 ont été mis en évidence.

La géométrie algorithmique a pour but de concevoir et d'analyser des algorithmes pour résoudre des problèmes géométriques. C'est un domaine récent de l'informatique théorique, qui s'est très rapidement développé depuis son apparition dans la thèse de M. I. Shamos en 1978. La randomisation permet d'éviter le recours à des structures compliquées, et s'avère très efficace, tant du point de vue de la complexité théorique, que des résultats pratiques. Nous nous sommes intéressés plus particulièrement à la conception d'algorithmes dynamiques : en pratique, il est fréquent que l'acquisition des données d'un problème soit progressive. Il n'est évidemment pas question de recalculer le résultat à chaque nouvelle donnée, d'où la nécéssité d'utiliser des schémas (semi-)dynamiques. Nous introduisons une structure très générale, le graphe d'influence, qui permet de construire de nombreuses structures géométriques : diagrammes de Voronoï, arrangements de segments... Nous étudions les algorithmes, à la fois du point de vue de la complexité théorique, de leur mise en oeuvre pratique et de l'efficacité des programmes.

En commentant certains résultats des sciences physiques ou mathématiques, plus particulièrement de la seconde moitié du XXe siècle, on cherche à comprendre l'importance philosophique du concept de diagramme, qui est au cœur de la théorie mathématique des catégories, des topoi et des esquisses. Partant du constat que les diagrammes et catégories contraignent à des options ontologiques, on propose pour étudier leur disposition conjointe de suivre quatre concepts fondamentaux qui forment le quadrilatère épistémique (la virtualité, la fonctorialité, l'universalité et la dualité). Le virtuel est nécessaire parce qu'une table n'existe pas de la même manière que le bleu du ciel qui n'a pas de réalité matérielle. La fonctorialité et le lemme de Yoneda imposent de reconsidérer le statut de l'objet. Le théorème de Diaconescu illustre l'idée que la logique immanente d'un lieu est déterminée par le topologique, que la logique n'a pas l'importance qu'on lui accorde parfois. L'universalité et la dualité déplace la notion de vérité qui n'est plus une simple valuation, mais une vérité-foudre, une vérité-événement qui fonctionne par adéquation et résonance de pans entiers de connaissance et non plus par inférence logique. Le diagramme devient le lieu de cette vérité qui passe par le geste. Dès lors, il devient possible de croiser ontologie et topologie en une onto-(po)-logie (ou une ontologie toposique) qui ne soit pas en contraction avec les philosophies de l'immanence. L'univocité de l'Être ne s'oppose pas à l'approche catégorielle. Plus encore : la prégnance des formes duales incite à penser l'hypothèse que l'Un est le dual de l'Être.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

La conversion photovoltaïque présente de nombreux avantages. Actuellement, les technologiesbasées sur l'élaboration de wafers de silicium cristallins dominent le marché, mais sont responsablesde pertes de matières importantes, très néfastes au coût de production des cellules. Le défi à releverest donc la réalisation de matériaux bas coûts en silicium par un procédé de métallurgie des poudres.Cependant, le frittage du silicium est dominé par des mécanismes de grossissement de grains quirendent la densification difficile par frittage naturel. Dans la littérature, l'identification de cesmécanismes est sujette à controverse. En particulier, le rôle de la couche d'oxyde natif (SiO2) à lasurface des particules de silicium reste inexploré. Dans ce manuscrit, l'influence de l'atmosphère surla réduction de cette couche de silice au cours du frittage est étudiée par analysethermogravimétrique. Les cinétiques de réduction sont en accord avec un modèle thermochimiqueprenant en compte, les quantités d'oxygène initialement présentes dans poudre, la pression partielleen espèces oxydantes autour de l'échantillon et l'évolution de la porosité du fritté. Pour la premièrefois, des données expérimentales permettent de montrer que la couche de silice inhibe legrossissement de grain. Des nouveaux procédés, basés sur un contrôle de l'atmosphère enmonoxyde de silicium (SiO(g)) autour de l'échantillon, sont alors proposés afin de maitriser la stabilitéde cette couche. Bien que la couche d'oxyde retarde les cinétiques de diffusion en volume, sonmaintien à des températures de 1300 - 1400 °C permet d'améliorer significativement la densification.Dans ces conditions, le comportement au frittage du silicium peut être séparé en deux étapes,clairement mises en évidences par la présence de deux pics de retrait sur les courbes de dilatométrie.Ce résultat est inhabituel compte tenu de l'aspect monophasé du matériau étudié. Cependant, il peutêtre expliqué à l'aide d'un modèle cinétique de frittage, basé sur des simplifications géométriques enaccord avec l'évolution microstructurale du matériau.

La spectrométrie de masse, en particulier le couplage HPLC/MRM3, est un outil bien adapté au diagnostic in vitro, particulièrement en microbiologie clinique. L'utilisation en routine de cette technologie est cependant tributaire de sa sensibilité et de sa spécificité. Ce travail de thèse a pour objectif d'étudier la possibilité d'éjecter et de détecter simultanément et de façon sélective des ions de ratio masse/charge donnés, ceux-ci étant confinés dans un piège ionique quadrupolaire. Cette approche permet de supprimer les étapes de balayage en masse et d'intégration mathématique du signal en mode MRM3 ce qui permet de gagner à la fois en sensibilité et en spécificité (en diminuant le temps de cycle et en diminuant le rapport signal sur bruit). Cet objectif a été poursuivi premièrement par une étude théorique approfondie des équations du mouvement des ions dans un piège radiofréquence ; deuxièmement par une étude numérique de la stabilité de ces équations et enfin troisièmement par une validation expérimentale de ces résultats théoriques. La présentation de ces trois approches fait l'objet du présent mémoire

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles. / This PhD thesis proposes the theoretical foundations of a new formal tool for symbolic verification of finite models. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs).In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs).First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures.Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round RobinMutex protocols,... ) our tool is not only better than other rewriting tools such as Timbuk, Maude or TOM, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).