Parallelization of SAT on Reconfigurable Hardware

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle.

Routage adaptatif et stabilité dans les réseaux maillés sans fil

Grâce à leur flexibilité et à leur facilité d’installation, les réseaux maillés sans fil (WMNs) permettent un déploiement d’une infrastructure à faible coût. Ces réseaux étendent la couverture des réseaux filaires permettant, ainsi, une connexion n’importe quand et n’importe où. Toutefois, leur performance est dégradée par les interférences et la congestion. Ces derniers causent des pertes de paquets et une augmentation du délai de transmission d’une façon drastique. Dans cette thèse, nous nous intéressons au routage adaptatif et à la stabilité dans ce type de réseaux. Dans une première partie de la thèse, nous nous intéressons à la conception d’une métrique de routage et à la sélection des passerelles permettant d’améliorer la performance des WMNs. Dans ce contexte nous proposons un protocole de routage à la source basé sur une nouvelle métrique. Cette métrique permet non seulement de capturer certaines caractéristiques des liens tels que les interférences inter-flux et intra-flux, le taux de perte des paquets mais également la surcharge des passerelles. Les résultats numériques montrent que la performance de cette métrique est meilleure que celle des solutions proposées dans la littérature. Dans une deuxième partie de la thèse, nous nous intéressons à certaines zones critiques dans les WMNs. Ces zones se trouvent autour des passerelles qui connaissent une concentration plus élevé du trafic ; elles risquent de provoquer des interférences et des congestions. À cet égard, nous proposons un protocole de routage proactif et adaptatif basé sur l’apprentissage par renforcement et qui pénalise les liens de mauvaise qualité lorsqu’on s’approche des passerelles. Un chemin dont la qualité des liens autour d’une passerelle est meilleure sera plus favorisé que les autres chemins de moindre qualité. Nous utilisons l’algorithme de Q-learning pour mettre à jour dynamiquement les coûts des chemins, sélectionner les prochains nœuds pour faire suivre les paquets vers les passerelles choisies et explorer d’autres nœuds voisins. Les résultats numériques montrent que notre protocole distribué, présente de meilleurs résultats comparativement aux protocoles présentés dans la littérature. Dans une troisième partie de cette thèse, nous nous intéressons aux problèmes d’instabilité des réseaux maillés sans fil. En effet, l’instabilité se produit à cause des changements fréquents des routes qui sont causés par les variations instantanées des qualités des liens dues à la présence des interférences et de la congestion. Ainsi, après une analyse de l’instabilité, nous proposons d’utiliser le nombre de variations des chemins dans une table de routage comme indicateur de perturbation des réseaux et nous utilisons la fonction d’entropie, connue dans les mesures de l’incertitude et du désordre des systèmes, pour sélectionner les routes stables. Les résultats numériques montrent de meilleures performances de notre protocole en comparaison avec d’autres protocoles dans la littérature en termes de débit, délai, taux de perte des paquets et l’indice de Gini.

Calcul en n-dimensions sur GPU

Le code source de la libraire développée accompagne ce dépôt dans l'état où il était à ce moment. Il est possible de trouver une version plus à jour sur github (http://github.com/abergeron).

Les assises idéologiques du projet conservateur de Stephen Harper

Plusieurs indices permettent de croire que le premier ministre Harper a pour projet de faire du Parti conservateur le parti politique dominant au Canada. À cette fin, il doit transformer l’organisation sociale et politique du pays de façon à le rendre plus conservateur. L’objectif du présent mémoire est de préciser les fondements idéologiques du projet de réforme de l’État canadien du premier ministre en m’appuyant sur les écrits des membres de l’École de Calgary. Je fais l’hypothèse que les politiques publiques mises en place par Harper sont inspirées des convictions des membres de cette école de pensée, dont il est un proche. Dans le premier chapitre, je détermine la signification du concept d’idéologie et établis la pertinence de l’analyse des idéologies pour expliquer les décisions politiques. Je définis ensuite les principaux types de conservatisme, afin de déterminer lequel inspire les membres de l’École de Calgary et le Parti conservateur. Dans le second chapitre, je dresse un portrait de la pensée de l’École de Calgary relativement à quatre thèmes, soit ceux du développement économique et social, du pouvoir judiciaire, de la politique étrangère et de l’identité nationale. Enfin, dans le troisième chapitre, je recense les décisions prises par le gouvernement Harper en relation avec ces quatre mêmes thèmes et vérifie leur concordance avec les idées portées par l’École de Calgary.

Structural aspects of the ribosome evolution and function

Les résultats ont été obtenus avec le logiciel "Insight-2" de Accelris (San Diego, CA)

Rétro ingénierie des modèles d’objets dynamiques pour JavaScript

La compréhension des objets dans les programmes orientés objet est une tâche impor- tante à la compréhension du code. JavaScript (JS) est un langage orienté-objet dyna- mique, et son dynamisme rend la compréhension du code source très difficile. Dans ce mémoire, nous nous intéressons à l’analyse des objets pour les programmes JS. Notre approche construit de façon automatique un graphe d’objets inspiré du diagramme de classes d’UML à partir d’une exécution concrète d’un programme JS. Le graphe résul- tant montre la structure des objets ainsi que les interactions entre eux. Notre approche utilise une transformation du code source afin de produire cette in- formation au cours de l’exécution. Cette transformation permet de recueillir de l’infor- mation complète au sujet des objets crées ainsi que d’intercepter toutes les modifications de ces objets. À partir de cette information, nous appliquons plusieurs abstractions qui visent à produire une représentation des objets plus compacte et intuitive. Cette approche est implémentée dans l’outil JSTI. Afin d’évaluer l’utilité de l’approche, nous avons mesuré sa performance ainsi que le degré de réduction dû aux abstractions. Nous avons utilisé les dix programmes de réfé- rence de V8 pour cette comparaison. Les résultats montrent que JSTI est assez efficace pour être utilisé en pratique, avec un ralentissement moyen de 14x. De plus, pour 9 des 10 programmes, les graphes sont suffisamment compacts pour être visualisés. Nous avons aussi validé l’approche de façon qualitative en inspectant manuellement les graphes gé- nérés. Ces graphes correspondent généralement très bien au résultat attendu. Mots clés: Analyse de programmes, analyse dynamique, JavaScript, profilage.

La résolution du contrat de vente en droit OHADA : d’une réforme à l’autre

La présente étude examine une des difficultés que soulève la résolution du contrat de vente en droit africain des affaires. L'Organisation pour l'Harmonisation en Afrique du Droit des Affaires (OHADA) créée par le Traité du 17 octobre 1993 organise les règles communautaires relatives à la résolution du contrat de vente. Le Livre VIII de l’Acte uniforme OHADA portant sur le Droit commercial Général a été adopté le 15 décembre 2010 et a abrogé l’Acte du 17 avril 1997. Selon l’article 281 de l’Acte uniforme, la résolution du contrat de vente ne survient que lors de l’inexécution totale ou partielle de l’obligation du cocontractant. Notre étude visera à évaluer les conséquences dans le droit de la vente OHADA de la substitution du critère de privation substantielle par celui de la gravité du comportement du débiteur justifiant une résolution unilatérale du contrat. Cette nouvelle position du droit de la vente OHADA se démarque dans une certaine mesure du droit matériel uniforme et rejoint un courant adapté aux impératifs socioéconomiques du commerce tant régional qu’international. En outre la partie lésée devra déterminer la gravité du comportement du débiteur au risque de voir sa demande sanctionnée pour défaut de droit et donner lieu à des dommages intérêts à l’autre partie. En effet, avec pour optique la nécessité de sauvegarder le contrat au nom du principe favor contractus, comment le juge détermine a posteriori si la gravité du comportement du cocontractant est suffisante pour anéantir le contrat? Ce nouveau critère de la gravité du comportement du cocontractant en droit de la vente OHADA vient supplanter le critère de la privation substantielle et fait cohabiter la traditionnelle résolution judiciaire avec celle de la résolution unilatérale dont les contours demeurent incertains. Les cas d’ouvertures liés à la résolution du contrat de vente OHADA pour inexécution des obligations fondamentales ou accessoires seront passés au crible de même que leurs effets sur les parties. Dans une approche comparatiste avec la Convention de Vienne et les règles de codifications privés telles que les Principes UNIDROIT ou du Droit Européen des Contrats il y a lieu de s’interroger sur la mise en œuvre et les conséquences de la résolution du contrat de vente OHADA par l’inexécution de l’obligation d’une des parties due à un manquement essentiel d’une part et à la gravité du comportement du débiteur d’autre part.

Études de réseaux d’expression génique : utilité pour l’élucidation des déterminants génétiques des traits complexes

Les traits quantitatifs complexes sont des caractéristiques mesurables d’organismes vivants qui résultent de l’interaction entre plusieurs gènes et facteurs environnementaux. Les locus génétiques liés à un caractère complexe sont appelés «locus de traits quantitatifs » (QTL). Récemment, en considérant les niveaux d’expression tissulaire de milliers de gènes comme des traits quantitatifs, il est devenu possible de détecter des «QTLs d’expression» (eQTL). Alors que ces derniers ont été considérés comme des phénotypes intermédiaires permettant de mieux comprendre l’architecture biologique des traits complexes, la majorité des études visent encore à identifier une mutation causale dans un seul gène. Cette approche ne peut remporter du succès que dans les situations où le gène incriminé a un effet majeur sur le trait complexe, et ne permet donc pas d’élucider les situations où les traits complexes résultent d’interactions entre divers gènes. Cette thèse propose une approche plus globale pour : 1) tenir compte des multiples interactions possibles entre gènes pour la détection de eQTLs et 2) considérer comment des polymorphismes affectant l’expression de plusieurs gènes au sein de groupes de co-expression pourraient contribuer à des caractères quantitatifs complexes. Nos contributions sont les suivantes : Nous avons développé un outil informatique utilisant des méthodes d’analyse multivariées pour détecter des eQTLs et avons montré que cet outil augmente la sensibilité de détection d’une classe particulière de eQTLs. Sur la base d’analyses de données d’expression de gènes dans des tissus de souris recombinantes consanguines, nous avons montré que certains polymorphismes peuvent affecter l’expression de plusieurs gènes au sein de domaines géniques de co-expression. En combinant des études de détection de eQTLs avec des techniques d’analyse de réseaux de co-expression de gènes dans des souches de souris recombinantes consanguines, nous avons montré qu’un locus génétique pouvait être lié à la fois à l’expression de plusieurs gènes au niveau d’un domaine génique de co-expression et à un trait complexe particulier (c.-à-d. la masse du ventricule cardiaque gauche). Au total, nos études nous ont permis de détecter plusieurs mécanismes par lesquels des polymorphismes génétiques peuvent être liés à l’expression de plusieurs gènes, ces derniers pouvant eux-mêmes être liés à des traits quantitatifs complexes.

A layered JavaScript virtual machine supporting dynamic instrumentation

L’observation de l’exécution d’applications JavaScript est habituellement réalisée en instrumentant une machine virtuelle (MV) industrielle ou en effectuant une traduction source-à-source ad hoc et complexe. Ce mémoire présente une alternative basée sur la superposition de machines virtuelles. Notre approche consiste à faire une traduction source-à-source d’un programme pendant son exécution pour exposer ses opérations de bas niveau au travers d’un modèle objet flexible. Ces opérations de bas niveau peuvent ensuite être redéfinies pendant l’exécution pour pouvoir en faire l’observation. Pour limiter la pénalité en performance introduite, notre approche exploite les opérations rapides originales de la MV sous-jacente, lorsque cela est possible, et applique les techniques de compilation à-la-volée dans la MV superposée. Notre implémentation, Photon, est en moyenne 19% plus rapide qu’un interprète moderne, et entre 19× et 56× plus lente en moyenne que les compilateurs à-la-volée utilisés dans les navigateurs web populaires. Ce mémoire montre donc que la superposition de machines virtuelles est une technique alternative compétitive à la modification d’un interprète moderne pour JavaScript lorsqu’appliqué à l’observation à l’exécution des opérations sur les objets et des appels de fonction.

Un outil d’évaluation neurocognitive des interactions humain-machine

De plus en plus de recherches sur les Interactions Humain-Machine (IHM) tentent d’effectuer des analyses fines de l’interaction afin de faire ressortir ce qui influence les comportements des utilisateurs. Tant au niveau de l’évaluation de la performance que de l’expérience des utilisateurs, on note qu’une attention particulière est maintenant portée aux réactions émotionnelles et cognitives lors de l’interaction. Les approches qualitatives standards sont limitées, car elles se fondent sur l’observation et des entrevues après l’interaction, limitant ainsi la précision du diagnostic. L’expérience utilisateur et les réactions émotionnelles étant de nature hautement dynamique et contextualisée, les approches d’évaluation doivent l’être de même afin de permettre un diagnostic précis de l’interaction. Cette thèse présente une approche d’évaluation quantitative et dynamique qui permet de contextualiser les réactions des utilisateurs afin d’en identifier les antécédents dans l’interaction avec un système. Pour ce faire, ce travail s’articule autour de trois axes. 1) La reconnaissance automatique des buts et de la structure de tâches de l’utilisateur, à l’aide de mesures oculométriques et d’activité dans l’environnement par apprentissage machine. 2) L’inférence de construits psychologiques (activation, valence émotionnelle et charge cognitive) via l’analyse des signaux physiologiques. 3) Le diagnostic de l‘interaction reposant sur le couplage dynamique des deux précédentes opérations. Les idées et le développement de notre approche sont illustrés par leur application dans deux contextes expérimentaux : le commerce électronique et l’apprentissage par simulation. Nous présentons aussi l’outil informatique complet qui a été implémenté afin de permettre à des professionnels en évaluation (ex. : ergonomes, concepteurs de jeux, formateurs) d’utiliser l’approche proposée pour l’évaluation d’IHM. Celui-ci est conçu de manière à faciliter la triangulation des appareils de mesure impliqués dans ce travail et à s’intégrer aux méthodes classiques d’évaluation de l’interaction (ex. : questionnaires et codage des observations).

Comparison of epicardial mapping and noncontact endocardial mapping in dog experiments and computer simulations

La fibrillation auriculaire, l'arythmie la plus fréquente en clinique, affecte 2.3 millions de patients en Amérique du Nord. Pour en étudier les mécanismes et les thérapies potentielles, des modèles animaux de fibrillation auriculaire ont été développés. La cartographie électrique épicardique à haute densité est une technique expérimentale bien établie pour suivre in vivo l'activité des oreillettes en réponse à une stimulation électrique, à du remodelage, à des arythmies ou à une modulation du système nerveux autonome. Dans les régions qui ne sont pas accessibles par cartographie épicardique, la cartographie endocardique sans contact réalisée à l'aide d'un cathéter en forme de ballon pourrait apporter une description plus complète de l'activité auriculaire. Dans cette étude, une expérience chez le chien a été conçue et analysée. Une reconstruction électro-anatomique, une cartographie épicardique (103 électrodes), une cartographie endocardique sans contact (2048 électrodes virtuelles calculées à partir un cathéter en forme de ballon avec 64 canaux) et des enregistrements endocardiques avec contact direct ont été réalisés simultanément. Les systèmes d'enregistrement ont été également simulés dans un modèle mathématique d'une oreillette droite de chien. Dans les simulations et les expériences (après la suppression du nœud atrio-ventriculaire), des cartes d'activation ont été calculées pendant le rythme sinusal. La repolarisation a été évaluée en mesurant l'aire sous l'onde T auriculaire (ATa) qui est un marqueur de gradient de repolarisation. Les résultats montrent un coefficient de corrélation épicardique-endocardique de 0.8 (expérience) and 0.96 (simulation) entre les cartes d'activation, et un coefficient de corrélation de 0.57 (expérience) and 0.92 (simulation) entre les valeurs de ATa. La cartographie endocardique sans contact apparait comme un instrument expérimental utile pour extraire de l'information en dehors des régions couvertes par les plaques d'enregistrement épicardique.

Urban Detection From Hyperspectral Images Using Dimension-Reduction Model and Fusion of Multiple Segmentations Based on Stuctural and Textural Features

Ce mémoire de maîtrise présente une nouvelle approche non supervisée pour détecter et segmenter les régions urbaines dans les images hyperspectrales. La méthode proposée n ́ecessite trois étapes. Tout d’abord, afin de réduire le coût calculatoire de notre algorithme, une image couleur du contenu spectral est estimée. A cette fin, une étape de réduction de dimensionalité non-linéaire, basée sur deux critères complémentaires mais contradictoires de bonne visualisation; à savoir la précision et le contraste, est réalisée pour l’affichage couleur de chaque image hyperspectrale. Ensuite, pour discriminer les régions urbaines des régions non urbaines, la seconde étape consiste à extraire quelques caractéristiques discriminantes (et complémentaires) sur cette image hyperspectrale couleur. A cette fin, nous avons extrait une série de paramètres discriminants pour décrire les caractéristiques d’une zone urbaine, principalement composée d’objets manufacturés de formes simples g ́eométriques et régulières. Nous avons utilisé des caractéristiques texturales basées sur les niveaux de gris, la magnitude du gradient ou des paramètres issus de la matrice de co-occurrence combinés avec des caractéristiques structurelles basées sur l’orientation locale du gradient de l’image et la détection locale de segments de droites. Afin de réduire encore la complexité de calcul de notre approche et éviter le problème de la ”malédiction de la dimensionnalité” quand on décide de regrouper des données de dimensions élevées, nous avons décidé de classifier individuellement, dans la dernière étape, chaque caractéristique texturale ou structurelle avec une simple procédure de K-moyennes et ensuite de combiner ces segmentations grossières, obtenues à faible coût, avec un modèle efficace de fusion de cartes de segmentations. Les expérimentations données dans ce rapport montrent que cette stratégie est efficace visuellement et se compare favorablement aux autres méthodes de détection et segmentation de zones urbaines à partir d’images hyperspectrales.

Structural rules for the formation of backbone-backbone interactions between closely packed RNA double helices

Les interactions entre les squelettes sucre-phosphate de nucléotides jouent un rôle important dans la stabilisation des structures tertiaires de larges molécules d’ARN. Elles sont régies par des règles particulières qui gouverne leur formation mais qui jusque là demeure quasiment inconnues. Un élément structural d’ARN pour lequel les interactions sucre-phosphate sont importantes est le motif d’empaquetage de deux doubles hélices d’ARN le long du sillon mineur. Ce motif se trouve à divers endroits dans la structure du ribosome. Il consiste en deux doubles hélices interagissant de manière à ce que le squelette sucre-phosphate de l’une se niche dans le sillon mineur de l’autre et vice versa. La surface de contact entre les deux hélices est majoritairement formée par les riboses et implique au total douze nucléotides. La présente thèse a pour but d’analyser la structure interne de ce motif et sa dépendance de stabilité résultant de l’association optimale ou non des hélices, selon leurs séquences nucléotidiques. Il est démontré dans cette thèse qu’un positionnement approprié des riboses leur permet de former des contacts inter-hélices, par l’entremise d’un choix particulier de l’identité des pairs de bases impliquées. Pour différentes pairs de bases participant à ce contact inter-hélices, l’identité optimale peut être du type Watson-Crick, GC/CG, or certaines pairs de bases non Watson-Crick. Le choix adéquat de paires de bases fournit une interaction inter-hélice stable. Dans quelques cas du motif, l’identité de certaines paires de bases ne correspond pas à la structure la plus stable, ce qui pourrait refléter le fait que ces motifs devraient avoir une liberté de formation et de déformation lors du fonctionnement du ribosome.

De l’or et des putes : vie et mort d’un village de 'squatters' abitibien

Cette étude s’intéresse au village de squatters de Roc-d’Or, surnommé Putainville, qui apparaît en 1936 avant d’être détruit par le gouvernement provincial au milieu des années 1940. Notre but est de comprendre pourquoi cette agglomération, qui est érigée illégalement sur les terrains gouvernementaux et qui est réputée pour être un important foyer de déviance, est relativement tolérée pendant une décennie avant que les résidences soient détruites ou déménagées à Malartic. D’abord, nous expliquons pourquoi cette agglomération, sans reconnaissance légale et dans laquelle les résidents ne sont pas propriétaires des terrains sur lesquels leurs bâtiments sont érigés, apparaît en Abitibi-Témiscamingue au début des années 1930. Ensuite, nous nous intéressons à l’aspect physique et à la population de Roc-d’Or. Le taux de masculinité, la mobilité, la diversité d’emploi et l’origine ethnique des résidents sont analysés. De plus, nous nous penchons sur la mauvaise réputation de Putainville : autant le contrôle judiciaire que la présence du monde interlope sont étudiés. Finalement, comme les mœurs légères des résidents et l’influence du curé de Malartic sont souvent considérées comme étant à l’origine de la décision d’éliminer ce village, nous évaluons la pertinence de cette croyance et nous déterminons si d’autres motifs, notamment monétaire ou politique, sont aussi entrés en ligne de compte.

Dynamique de recombinaison radiative dans les nanofils InGaN/GaN : étude détaillée de la photoluminescence

Mesures effectuées dans le laboratoire de caractérisation optique des semi-conducteurs du Prof. Richard Leonelli du département de physique de l'université de Montréal. Les nanofils d'InGaN/GaN ont été fournis par le groupe du Prof. Zetian Mi du département de génie électrique et informatique de l'université McGill.