La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origine / Software verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification.

Ce travail de thèse porte sur le contrôle de santé intégré par émission acoustique desmatériaux composites stratifiés et sandwichs. Le capteur d’EA est d’une part implanté dans lamasse du matériau et d’autre part collé à la surface de ce dernier. Une première étude estconsacrée à l’étude de l’influence de l’implant piézoélectrique dans le volume du matériau surle comportement et les caractéristiques mécaniques en statiques, en fatigue cyclique et enfluage sous sollicitations en traction et en flexion. Les signaux d’émission acoustique sontcollectés au cours des essais sur les différents matériaux. Les mécanismes d’endommagementde chaque matériau sont identifiés et caractérisés en utilisant une analyse multiparamétrique(k-moyennes) des signaux collectés. La dynamique de chaque mécanisme est suivie jusqu’à larupture permettant de discriminer les mécanismes les plus critiques conduisant à la rupture dumatériau. Une étude comparative des signaux d’EA entre matériau instrumenté en surface etcelui instrumenté en volume avec insertion d’élément piézoélectrique est également menée.Elle a montré que les matériaux avec capteurs intégrés sont plus sensibles à l’émissionacoustique, améliorant ainsi l’identification des mécanismes d’endommagement et le contrôlede santé intégré des matériaux composites étudiés. Enfin, la dernière partie du travail a étéconsacrée à l’étude de l’influence de l’intégration de plusieurs capteurs dans des structures encomposites stratifiés et sandwichs. L’analyse des résultats expérimentaux et l’observation dessignaux d’EA obtenus dans ces structures soumises à différentes sollicitations ont permis dedéfinir les principaux signatures acoustiques des différents modes d’endommagementprépondérants dans chaque type de structure. La localisation des sources d’endommagement amis en évidence que les événements acoustiques sont apparus loin des positions des capteursintégrés. De point de vue comparaison entre matériau instrumenté et matériau noninstrumenté, l’activité acoustique montre clairement l’avantage de l’intégration del’instrumentation au sein du composite. Cet avantage réside dans le fait de la détectionexpérimentale des modes d’endommagement précoces et leur chronologie d’apparition,faisant ainsi révéler les performances du composite instrumenté vis-à-vis à sa réponse enversl’initiation, la propagation et l’accumulation des défauts microscopiques. / The increasing demands to improve the performance of aerospace and other engineering Systems require a new class of structures, such as smart structures. These can be defined as the system that has built-in capability or with intrinsic sensors that perceive and process the operating environments, and take effective action to fulfil the intended mission. The future of smart structure technology is very promising. There has been considerable interest in the use of piezoelectric materials in conjunction with the light-weight and high-strength/modulus polymeric composites as one type of smart structures. This work presents a health monitoring study of composites incorporating an integrated piezoelectric sensor. Firstly, experimental research is focused on examining the effects of the embedded sensors on the structural integrity of composites subjected to tensile and 3-point bending loads. A series of specimen composites (laminated composites and sandwich) with and without embedded piezoelectric sensors were fabricated. The composite specimens with PZT sensors embedded in the mid-plane were tested in static, fatigue and creep loading while continuously monitoring the response by the acoustic emission technique. The acoustic signals were analysed using the classification k-means methoc in order to identify the different damage and to follow the evolution of these various mechanisms for both types of materials (with and without sensor).

Bien que les orthèses lombaires (OL) soient couramment employées depuis de nombreuses années dans le traitement conservateur des lombalgies, leurs effets mécaniques et posturaux restent, à notre connaissance, partiellement inexplorés. Des obstacles d'ordre méthodologique en sont la principale cause avec en premier lieu la difficulté d'évaluer les effets des OL à l'intérieur du tronc sans être invasif et sans nécessiter un équipement coûteux difficilement utilisable lors de la pratique médicale courante. La levée de ces verrous scientifiques a guidé l'ensemble de ce travail doctoral à travers le développement d'une méthodologie spécifique. L'effet mécanique a été étudié à partir d'une nouvelle méthode non-invasive de mesure de la pression intradiscale réalisée à partir d'une modélisation par éléments finis contrôlée par radiographie. Les premiers résultats ont démontré la possibilité de diminuer de 15 à 22% en moyenne la pression intradiscale lors du port d'une OL modifiant la statique rachidienne. Les différents travaux sur l'équilibre postural ont permis de définir une méthodologie d'analyse de la posture en station debout puis assise adaptée à l'évaluation des OL. Les premiers résultats chez des patients lombalgiques subaiguës ont mis en évidence un contrôle postural plus efficient (réduction de la raideur active du tronc) lors du port de l'OL la plus rigide. A terme, cette méthodologie facile à mettre en œuvre permettra d'adapter les caractéristiques du produit (raideur passive / forme) aux caractéristiques des patients (raideur active / courbure lombaire) dans le but d’optimiser l'efficacité clinique / Although lumbar orthoses (LO) are commonly used for many years in the conservative treatment of low back pain, postural and mechanical effects are, to our knowledge, partly unexplored. Methodological difficulties are the main cause with, in the first place, the difficulty to assess the LO effects inside the trunk with a non-invasive and not expensive method adapted for current medical practice. This Ph.D work attempts to address these difficulties through the development of a specific methodology. The mechanical effect was studied by a non-invasive estimation of the intradiscal pressure through a finite element modeling controlled by radiographs. The first results showed the possibility of a mean reduction from 15 to 22% of the intradiscal pressure while wearing an LO which is able to change the spinal posture. The different works on postural balance allowed us to define a methodology for a suitable LO assessment in standing and then sitting postures. The first results in patients with subacute low back pain showed a more efficient postural control (reduction of active stiffness of the trunk) while wearing the most stiffer LO. In the future, this easy-to-implement assessment could be helpful to more accurately target the appropriate LO for a given patient in order to improve his / her clinical status

De nombreux produits encapsulés sont utilisés dans la vie quotidienne. Crèmes cosmétiques, peintures, et pesticides en sont quelques exemples. De nos jours, de plus en plus de technologies innovantes mettent en jeu des substances encapsulées. La microencapsulation a permis à de nouveaux « textiles intelligents » de voir le jour, tels que les textiles sur lesquels sont fixées des microcapsules qui libèrent un principe actif amincissant, odorant, hydratant ou encore répulsif pour les insectes. Les microcapsules sont des produits à fortes valeur ajoutée, dont les propriétés sont nombreuses, et délicates à maîtriser toutes à la fois. Si l'étape de formulation a pour objectif de trouver la recette optimale pour répondre le mieux possible au cahier des charges, le type de procédé de fabrication choisi doit garantir une production homogène dans le temps, sans écarts par rapports aux propriétés attendues. L'objectif de ces travaux est de proposer une alternative continue aux procédés batch traditionnellement mis en œuvre pour l'encapsulation par polycondensation interfaciale, coûteux en termes d'investissement et de frais de fonctionnement. L'encapsulation par polycondensation interfaciale est constituée d'une étape d'émulsification suivie d'une étape réactive. Nous proposons un procédé découplant ces deux étapes grâce à deux technologies adaptées aux contraintes hydrodynamiques respectives de chaque étape. Cette étude est réalisée sur la base d'un système modèle espèce encapsulée / membrane polymérique. L'étape d'émulsification est réalisée en mélangeurs statiques en régime turbulent. Des mesures de pertes de charge en écoulements monophasiques ont permis de mettre en évidence l'apparition de ce régime et d'établir des corrélations représentant ces pertes de charge a travers l'emploi des nombres adimensionnels que sont le nombre de Reynolds et le facteur de friction. Concernant l'émulsification, nous évaluons l'influence de différents paramètres sur les performances de l'opération en termes de tailles de gouttes obtenues en fonction du coût énergétique. Nous comparons également les performances de trois designs de mélangeurs statiques commercialisés par la société Sulzer, et corrélons les résultats obtenus en termes de diamètres moyens de Sauter en fonction des nombres de Reynolds et de Weber. L'étape réactive est tout d'abord mise en œuvre en réacteur agité afin d'étudier la cinétique de la réaction, et d'acquérir des temps de réactions qui permettent par la suite de dimensionner le réacteur continu. Enfin cette étape est réalisée dans deux types de réacteurs continus : le réacteur Deanhex, développé et étudié par Anxionnaz et al. (2009), ainsi qu'un réacteur tubulaire en serpentin. Cette dernière étude consiste d'une part à valider le passage au continu à travers la conservation de la granulométrie des gouttelettes de l'émulsion durant la réaction, et la conservation de la vitesse apparente de la réaction. Enfin, les conditions hydrodynamiques favorables présentées par les réacteurs continus permettent d'apporter de nouvelles voies d'intensification au procédé en augmentant d'une part la concentration en capsules dans le réacteur, et en s'affranchissant de l'emploi du tensioactif utilisé pour stabiliser les gouttes de l'émulsion. Ce procédé, proposé pour la production en continu de microcapsules, offre une amélioration en termes de qualité du produit et de coût par rapport aux procédés traditionnels en batch mis en œuvre dans l'industrie. / The aim of the present work is to propose a continuous alternative to batch processes classically used to carry out encapsulation by interfacial polycondensation that represent high investment and working costs. Encapsulation by interfacial polycondensation consists in an emulsification step followed by a reactive step. We propose here a process decoupling these two steps using technologies well adapted to hydrodynamic issues of each step. This study is realised on the basis of model system. The emulsification step is carried out in static mixers under turbulent flow. Pressure drop measurements in single-phase flow enable to highlight this flow regime and to establish correlations representing these pressure drops in terms of dimensionless numbers: the Reynolds number and the friction factor. About emulsification we evaluate the influence of different parameters on the operation performances in terms of mean droplets size as a function of energy cost. We compare the performances of three different Sulzer static mixers and correlate results obtained in terms of Sauter mean diameter as a function of Reynolds and Weber numbers. The reactive step has been first carried out is stirred tank in order to study the reaction kinetics and to acquire reaction times necessary to design continuous reactors. Finally this step has been realised using two continuous reactors: the Deanhex reactor (Anxionnaz et al., 2009) and a coiled tube reactor. This last study consists first in validating the continuous process through the conservation of the emulsion size distribution during encapsulation and the conservation of the apparent kinetics. Finally the favourable hydrodynamic conditions presented by continuous reactors offer new ways of intensification to the process. In fact it is possible to increase the microcapsule concentration in the reactor and to work without surfactant to stabilize the emulsion. This continuous process for microcapsules production offers improvements in terms of product quality and working costs compared to traditional batch process used in the industry

Dans cette thèse, nous étudions l'analyse statique par interprétation abstraites de programmes manipulant des tableaux, afin d'inférer des propriétés sur les valeurs numériques et les structures de données qui y sont stockées. Les tableaux sont omniprésents dans de nombreux programmes, et les erreurs liées à leur manipulation sont difficile à éviter en pratique. De nombreux travaux de recherche ont été consacrés à la vérification de tels programmes. Les travaux existants s'intéressent plus particulièrement aux propriétés concernant les valeurs numériques stockées dans les tableaux. Toutefois, les programmes bas-niveau (comme les systèmes embarqués ou les systèmes d'exploitation temps réel) utilisent souvent des tableaux afin d'y stocker des structures de données telles que des listes, de manière à éviter d'avoir recours à l'allocation de mémoire dynamique. Dans cette thèse, nous présentons des techniques permettant de vérifier par interprétation abstraite des propriétés concernant à la fois les données numériques ainsi que les structures composites stockées dans des tableaux. Notre première contribution est une abstraction qui permet de décrire des stores à valeurs numériques et avec valeurs optionnelles (i.e., lorsqu'une variable peut soit avoir une valeur numérique, soit ne pas avoir de valeur du tout), ou bien avec valeurs ensemblistes (i.e., lorsqu'une variable est associée à un ensemble de valeurs qui peut être vide ou non). Cette abstraction peut être utilisée pour décrire des stores où certaines variables ont un type option, ou bien un type ensembliste. Elle peut aussi servir à la construction de domaines abstraits pour décrire des propriétés complexes à l'aide de variables symboliques, par exemple, pour résumer le contenu de zones dans des tableaux. Notre seconde contribution est un domaine abstrait pour la description de tableaux, qui utilise des propriétés sémantiques des valeurs contenues afin de partitionner les cellules de tableaux en groupes homogènes. Ainsi, des cellules contenant des valeurs similaires sont décrites par les mêmes prédicats abstraits. De plus, au contraire des analyses de tableaux conventionnelles, les groupes ainsi formés ne sont pas nécessairement contigüs, ce qui contribue à la généralité de l'analyse. Notre analyse peut regrouper des cellules non-congitües, lorsque celles-ci ont des propriétés similaires. Ce domaine abstrait permet de construire des analyses complètement automatiques et capables d'inférer des invariants complexes sur les tableaux. Notre troisième contribution repose sur une combinaison de cette abstraction des tableaux avec différents domaines abstraits issus de l'analyse de forme des structures de données et reposant sur la logique de séparation. Cette combinaison appelée coalescence opère localement, et relie des résumés pour des structures dynamiques à des groupes de cellules du tableau. La coalescence permet de définir de manière locale des algorithmes d'analyse statique dans le domaine combiné. Nous l'utilisons pour relier notre domaine abstrait pour tableaux et une analyse de forme générique, dont la tâche est de décrire des structures chaînées. L'analyse ainsi obtenue peut vérifier à la fois des propriétés de sûreté et des propriétés de correction fonctionnelle. De nombreux programmes bas-niveau stockent des structures dynamiques chaînées dans des tableaux afin de n'utiliser que des zones mémoire allouées statiquement. La vérification de tels programmes est difficile, puisqu'elle nécessite à la fois de raisonner sur les tableaux et sur les structures chaînées. Nous construisons une analyse statique reposant sur ces trois contributions, et permettant d'analyser avec succés de tels programmes. Nous présentons des résultats d'analyse permettant la vérification de composants de systèmes d'exploitation et pilotes de périphériques. / We study the static analysis on both numeric and structural properties of array contents in the framework of abstract interpretation. Since arrays are ubiquitous in most software systems, and software defects related to mis-uses of arrays are hard to avoid in practice, a lot of efforts have been devoted to ensuring the correctness of programs manipulating arrays. Current verification of these programs by static analysis focuses on numeric content properties. However, in some lowlevel programs (like embedded systems or real-time operating systems), arrays often contain structural data (e.g., lists) without using dynamic allocation. In this manuscript, we present a series of techniques to verify both numeric and structural properties of array contents. Our first technique is used to describe properties of numerical stores with optional values (i.e., where some variables may have no value) or sets of values (i.e., where some variables may store a possibly empty set of values). Our approach lifts numerical abstract domains based on common linear inequality into abstract domains describing stores with optional values and sets of values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded memory blocks like in arrays. Our second technique is an abstract domain which utilizes semantic properties to split array cells into groups. Cells with similar properties will be packed into groups and abstracted together. Additionally, groups are not necessarily contiguous. Compared to conventional array partitioning analyses that split arrays into contiguous partitions to infer properties of sets of array cells. Our analysis can group together non-contiguous cells when they have similar properties. Our abstract domain can infer complex array invariants in a fully automatic way. The third technique is used to combine different shape domains. This combination locally ties summaries in both abstract domains and is called a coalesced abstraction. Coalescing allows to define efficient and precise static analysis algorithms in the combined domain. We utilize it to combine our array abstraction (i.e., our second technique) and a shape abstraction which captures linked structures with separation logicbased inductive predicates. The product domain can verify both safety and functional properties of programs manipulating arrays storing dynamically linked structures, such as lists. Storing dynamic structures in arrays is a programming pattern commonly used in low-level systems, so as to avoid relying on dynamic allocation. The verification of such programs is very challenging as it requires reasoning both about the array structure with numeric indexes and about the linked structures stored in the array. Combining the three techniques that we have proposed, we can build an automatic static analysis for the verification of programs manipulating arrays storing linked structures. We report on the successful verification of several operating system kernel components and drivers.

L'utilisation d'architectures hétérogènes, combinant des processeurs multicoeurs avec des accélérateurs tels que les GPU, FPGA et Intel Xeon Phi, a augmenté ces dernières années. Les GPUs peuvent atteindre des performances significatives pour certaines catégories d'applications. Néanmoins, pour atteindre ces performances avec des API de bas niveau comme CUDA et OpenCL, il est nécessaire de réécrire le code séquentiel, de bien connaître l’architecture des GPUs et d’appliquer des optimisations complexes, parfois non portables. D'autre part, les modèles de programmation basés sur des directives (par exemple, OpenACC, OpenMP) offrent une abstraction de haut niveau du matériel sous-jacent, simplifiant ainsi la maintenance du code et améliorant la productivité. Ils permettent aux utilisateurs d’accélérer leurs codes séquentiels sur les GPUs en insérant simplement des directives. Les compilateurs d'OpenACC/OpenMP ont la lourde tâche d'appliquer les optimisations nécessaires à partir des directives fournies par l'utilisateur et de générer des codes exploitant efficacement l'architecture sous-jacente. Bien que les compilateurs d'OpenACC/OpenMP soient matures et puissent appliquer certaines optimisations automatiquement, le code généré peut ne pas atteindre l'accélération prévue, car les compilateurs ne disposent pas d'une vue complète de l'ensemble de l'application. Ainsi, il existe généralement un écart de performance important entre les codes accélérés avec OpenACC/OpenMP et ceux optimisés manuellement avec CUDA/OpenCL. Afin d'aider les programmeurs à accélérer efficacement leurs codes séquentiels sur GPU avec les modèles basés sur des directives et à élargir l'impact d'OpenMP/OpenACC dans le monde universitaire et industrielle, cette thèse aborde plusieurs problématiques de recherche. Nous avons étudié les modèles de programmation OpenACC et OpenMP et proposé une méthodologie efficace de parallélisation d'applications avec les approches de programmation basées sur des directives. Notre expérience de portage d'applications a révélé qu'il était insuffisant d'insérer simplement des directives de déchargement OpenMP/OpenACC pour informer le compilateur qu'une région de code particulière devait être compilée pour être exécutée sur la GPU. Il est essentiel de combiner les directives de déchargement avec celles de parallélisation de boucle. Bien que les compilateurs actuels soient matures et effectuent plusieurs optimisations, l'utilisateur peut leur fournir davantage d'informations par le biais des clauses des directives de parallélisation de boucle afin d'obtenir un code mieux optimisé. Nous avons également révélé le défi consistant à choisir le bon nombre de threads devant exécuter une boucle. Le nombre de threads choisi par défaut par le compilateur peut ne pas produire les meilleures performances. L'utilisateur doit donc essayer manuellement différents nombres de threads pour améliorer les performances. Nous démontrons que les modèles de programmation OpenMP et OpenACC peuvent atteindre de meilleures performances avec un effort de programmation moindre, mais les compilateurs OpenMP/OpenACC atteignent rapidement leur limite lorsque le code de région déchargée a une forte intensité arithmétique, nécessite un nombre très élevé d'accès à la mémoire globale et contient plusieurs boucles imbriquées. Dans de tels cas, des langages de bas niveau doivent être utilisés. Nous discutons également du problème d'alias des pointeurs dans les codes GPU et proposons deux outils d'analyse statiques qui permettent d'insérer automatiquement les qualificateurs de type et le remplacement par scalaire dans le code source. / Recent years have seen an increase of heterogeneous architectures combining multi-core CPUs with accelerators such as GPU, FPGA, and Intel Xeon Phi. GPU can achieve significant performance for certain categories of application. Nevertheless, achieving this performance with low-level APIs (e.g. CUDA, OpenCL) requires to rewrite the sequential code, to have a good knowledge of GPU architecture, and to apply complex optimizations that are sometimes not portable. On the other hand, directive-based programming models (e.g. OpenACC, OpenMP) offer a high-level abstraction of the underlying hardware, thus simplifying the code maintenance and improving productivity. They allow users to accelerate their sequential codes on GPU by simply inserting directives. OpenACC/OpenMP compilers have the daunting task of applying the necessary optimizations from the user-provided directives and generating efficient codes that take advantage of the GPU architecture. Although the OpenACC / OpenMP compilers are mature and able to apply some optimizations automatically, the generated code may not achieve the expected speedup as the compilers do not have a full view of the whole application. Thus, there is generally a significant performance gap between the codes accelerated with OpenACC/OpenMP and those hand-optimized with CUDA/OpenCL. To help programmers for speeding up efficiently their legacy sequential codes on GPU with directive-based models and broaden OpenMP/OpenACC impact in both academia and industry, several research issues are discussed in this dissertation. We investigated OpenACC and OpenMP programming models and proposed an effective application parallelization methodology with directive-based programming approaches. Our application porting experience revealed that it is insufficient to simply insert OpenMP/OpenACC offloading directives to inform the compiler that a particular code region must be compiled for GPU execution. It is highly essential to combine offloading directives with loop parallelization constructs. Although current compilers are mature and perform several optimizations, the user may provide them more information through loop parallelization constructs clauses in order to get an optimized code. We have also revealed the challenge of choosing good loop schedules. The default loop schedule chosen by the compiler may not produce the best performance, so the user has to manually try different loop schedules to improve the performance. We demonstrate that OpenMP and OpenACC programming models can achieve best performance with lesser programming effort, but OpenMP/OpenACC compilers quickly reach their limit when the offloaded region code is computed/memory bound and contain several nested loops. In such cases, low-level languages may be used. We also discuss pointers aliasing problem in GPU codes and propose two static analysis tools that perform automatically at source level type qualifier insertion and scalar promotion to solve aliasing issues.

Le principal objectif de cette thèse est d'expliquer en quoi l’efficience statique (static efficiency), l’efficience de coordination (coordinative efficiency) et l’efficience créative (creative efficiency) jouent un rôle déterminant dans la conception de la gouvernance à l'ère numérique. Il s’agit également d’étudier des mécanismes originaux de gouvernance, au-delà de la traditionnelle dimension marché-hiérarchie, pouvant faciliter les processus de coordination intégrative (integrative coordination) ainsi que de création collective dans les organisations.La thèse comprend trois essais. Le premier est une contribution de nature théorique montrant que l’économie des coûts de transaction (Williamson 1979, 1991, 1996, 2002) ne permet pas de rendre compte de façon satisfaisante de la conception de la gouvernance à l’ère numérique. Le modèle conceptuel normatif proposé contribue à repenser celle-ci dans une perspective pluraliste intégrant complexité et variété. Les choix de gouvernance ne sont ainsi plus limités à la seule dimension marché-hiérarchie comme le laisse penser l’économie des coûts de transaction. Une perspective intégrant la construction sociale des modes d’organisation (Giddens, 1985; Greenwood et al. 2011) permet de définir une variété de formes de gouvernance. Il est possible de représenter, dans un espace à trois dimensions (efficience statique, efficience de coordination et efficience créative), les différentes configurations de gouvernance sous la forme d’un triangle. Cette représentation peut être appliquée afin de rendre compte des choix de gouvernance possibles à différents niveaux organisationnels.Les deux essais suivants sont à dominante empirique. Ils visent à prolonger le premier en étudiant le lien entre des configurations innovantes de gouvernance et la performance des organisations en matière d’efficacité de coordination et d’efficacité créative. Le deuxième essai se concentre sur la coordination d’intégration dans les organisations. Des structures organisationnelles distribuées à plusieurs couches ou layered distributed organizational structures (Simon, 1962), des plans définis ex ante de façon imprécise ou broad-brushed ex ante plans (Edmondson, Bohmer et Pisano, 2001), ainsi que des semi-structures (Brown et Eisenhardt, 1997) s’avèrent utiles au processus de coordination lorsque les interdépendances sont complexes et incertaines. Le troisième essai porte sur la performance des organisations en matière de créativité collective. Il s’intéresse notamment aux dispositifs organisationnels facilitant l’émergence d’une telle créativité tout en préservant stabilité et efficacité. Plusieurs formes de perturbation qualifiées d’ordonnées (ordered disruption), tant au niveau spatial (ordered spatial disruption) que temporel (ordered temporal disruption) et affectif (ordered affective disruption), contribuent à l'émergence de la créativité collective.Le matériel empirique utilisé dans les deuxième et troisième essais provient d’une étude des modes de gouvernance de différents projets de villes intelligentes (smart-cities) nécessitant une collaboration entre plusieurs organisations. / The main objective of this dissertation is to explain why coordinative efficiency, creative efficiency, together with static efficiency are all critical goals of governance design in digital age, and to explore innovative governance arrangements, beyond the one-dimensional line defined by “market” and “hierarchy”, that can facilitate the processes of integrative coordination, and collective creation in organizations.The dissertation is composed of three essays. Essay 1 is a theory paper that provides the overall theoretical arguments about why transaction cost economics (Williamson 1979, 1991, 1996, 2002) is no longer a satisfactory theoretical framework for governance design in the digital age, and offers a normative model which suggest possibilities of much more nuanced, complicated and pluralistic governance choices than suggested by transaction cost economics. It is argued that potential governance choices are not solely situated on a one-dimensional line between hierarchy and market, as transaction cost economics asserts. The rich connotations of socially constructed agency (Giddens, 1985; Greenwood et al. 2011) provide diverse possibilities of governance arrangements, which spread across a triangular plane in a three-dimensional space defined by static efficiency, coordinative efficiency and creative efficiency (see Figure 1). This paper provides both graphic and mathematical presentations of this three-dimensional model for governance design, which can be applied to different levels of organizing.Essay 2 and 3 are two empirical papers that endeavor to extend Essay 1 by finding out the exact relationship between certain innovative governance arrangements with organizations’ performance in coordinative and creative efficiencies. Essay 2 focuses on the realization of integrative coordination in organizations. It found out that layered distributed organizational structure (Simon, 1962), broad-brushed ex ante plan (Edmondson, Bohmer and Pisano, 2001), and semi-structures (Brown and Eisenhardt, 1997) are beneficial in facilitating an ongoing coordination process when interdependencies are complex and uncertain. Essay 3 focuses on organizations’ performance in collective creativity (Shalley et al., 2004; George, 2007), especially on what governance arrangements can best allow collective creativity to emerge without overly sacrificing organizational stability and efficiency. It is discovered that “ordered disruption”, including ordered spatial disruption, ordered temporal disruption and ordered affective disruption, have positive effects on the emergence of collective creativity. Both Essay 2 and Essay 3 use collaborative organizations on smart city projects as the empirical setting. The findings of these two empirical papers are grounded on multiple case studies on those collaborative organizations.

Cette thèse porte sur l'analyse statique de code par typage dans le but de détecter les erreurs dans les programmes avant leur exécution. Plus précisément, nous nous intéressons ici au domaine du sous-typage, dans lequel les propriétés du code sont représentées par des ensemble de contraintes de la forme (t1 <= t2). Nos mécanismes de vérification sont alors basés sur l'agrégation de contraintes de sous-typage et la vérification de leur compatibilité par saturation. Le langage de base sur lequel nous travaillons est un ML étendu, muni de variants et d'un mécanisme de filtrage de motifs. Nous commençons par définir un formalisme nous permettant d'exprimer nos systèmes de types sous forme de règles d'inférences. Ce formalisme présente l'avantage d'être suffisamment souple pour nous permettre de prouver les propriétés de validité et de terminaison de nos systèmes, et suffisamment précis pour nous permettre d'en dériver une implémentation de manière systématique. Après avoir défini un système de types de base pour notre langage, nous en présentons trois extensions originales : * Une amélioration du typage du filtrage de motifs basée en particulier sur l'ajout d'un opérateur de disjonction entre les contraintes de sous-typage. Cet opérateur permet alors d'exprimer, pour chaque cas de filtrage, le lien entre le filtre et les contraintes extraites du typage de l'expression correspondante. Ceci nous permet en particulier de représenter beaucoup plus finement le type de certaines fonctions et ainsi d'accepter plus de programmes valides. * Une alternative au mécanisme classique de généralisation permettant de distinguer les contraintes associées aux différents usages des paramètres des fonctions. Un tel mécanisme rend en particulier la construction de langage "let" de ML obsolète. Mixé avec la première extension, nous obtenons un système permettant d'encoder dans le langage lui même (c'est à dire sans ajouter de construction supplémentaire), un modèle objet intéressant. * Une formalisation des GADT basée sur une implantation originale des variables de type existentielles. En plus d'être compatible avec le sous-typage, cette variante des GADT présente une amélioration notable par rapport aux GADT standards par le fait qu'elle étend les possibilités d'inférence. Les annotations de type, habituellement obligatoires en présence de GADT, deviennent ici presque toutes facultatives. Bien qu'il soit possible de dériver directement une implémentation de ces systèmes, ce qui est principalement utile pour leur compréhension et leur prototypage, les performances des typeurs obtenus de la sorte ne sont pas suffisantes pour analyser des programmes de taille réelle. Ceci est principalement dû aux différentes extensions que nous apportons au langage des contraintes, en particulier les opérateurs de disjonction et de négation. Nous présentons alors les différentes techniques que nous avons mises en place pour l'implémentation de nos systèmes permettant à nos analyses de passer à l'échelle en pratique. / This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1 <= t2). Our verification mechanisms are based on the aggregation of sub-typing constraints and checking of their compatibility by saturation. The base language on which we define our type systems is an ML-like language provided with variants and pattern matching. We starts by defining a formalism to express our type systems thanks to inference rules. This formalism has the advantage to be sufficiently flexible to allow proving validity and termination properties of our systems, and sufficiently precise to allow a systematic derivation of our inference rules into a runnable typer. After the definition of a base type system for our language, we present three novel extensions: * An improvement of type inference for the pattern matching based on the addition of the "or" operator between sub-typing constraints. This operator allow to express a link, in each cases of a match, between the pattern and the constraints generated at typing time of the case expression. This allows us to refine the type of some functions, and then to accept more valid programs. * A new implementation of the generalization mechanism. This allows to distinguish constraints associated to the different occurrences of a function parameter in its body. Thanks to this mechanism, the "let" construction from ML is in particular obsolete. By mixing this extension with the first one, we obtain a type system able to encode "objects" without any additional language construction. * A formalization of GADT based on an novel implementation of existential type variables. In addition to be compatible with the sub-typing context of this thesis, this alternative to GADT has the advantage to improve type inference. As a consequence, most of type annotations, usually required in the presence of GADT, are now optional. Despite the fact that it is possible to directly derive an implementation of our type systems from their rules, that is principally interesting for their comprehension and prototyping, the effectiveness of such typer is insufficient to analyze real world programs. This is principally due to the extensions we provide to the language of constraints, and in particular to the "or" and "not" operators. At then end, we present multiple techniques we used in our implementation to extend the scalability of our analysis.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

La première étape de cette étude vise à évaluer, selon les données de terrain, la validité prédictive des outils les plus utilisés quant à prédire le risque de récidive auprès des délinquants sexuels, soit la Statique-99R et la Stable-2007. Au cours de la première étape de cette étude, la validité prédictive de la Statique-99R et de la Stable-2007 a été évaluée via les données d’expertise d’un échantillon d’un échantillon de 797 délinquants sexuels hommes. Ces données ont été obtenues par la recension des archives du Centre d’Intervention en Délinquance sexuelle (CIDS) au Québec, Canada, de 1998 à 2021 et pairées aux données officielles de récidive obtenues par la Sûreté du Québec pour la même période. Les scores totaux et les niveaux de risques évalués par la Statique-99R prédisaient significativement la récidive générale, sexuelle et violente (non-sexuelle). Bien que cela n’ait pas été le cas pour la Stable-2007, cet outil contribuait à prédire, lorsqu’ajoutée à la Statique-99R, la récidive générale, sexuelle et violente (non-sexuelle) pour ces trois types de récidive. La seconde partie de cette étude s’intéressait aux dimensions latentes de ces instruments. Les analyses factorielles exploratoire ont permis de relever 3 dimensions pour la Statique-99R, soit Jeune/Célibataire, Persistance (sexuelle et non-sexuelle) et Conduite de Prédation détachée, similaires à certain de ceux identifiés par Barbaree et al. (2006). Pour la Stable-2007, deux dimensions ont été identifiées, soit la présence de Caractéristiques antisociales et la Déviance sexuelle. Toutefois, aucune des dimensions extraites pour la Statique-99R et la Stable-2007 ne permettait de prédire significativement la récidive sexuelle. L’interprétation de ces résultats, les limites de cette étude et les implications possibles pour de plus amples recherches sont discutées. / The first phase of this study aimed to evaluate, based on field data, the predictive validity of the most used tools for predicting the risk of recidivism among sexual offenders, the Static-99R and the Stable-2007. Predictive validity of the Static-99R and the Stable-2007 was firstly assessed using legal expertise data from a sample of 797 male sex offenders. These data were obtained by reviewing the archives of the Centre d'Intervention en Délinquance sexuelle (CIDS) in Quebec, Canada, from 1998 to 2021 and matched with official recidivism data obtained by the Sûreté du Québec for the same period. The total scores and risk categories assessed by the Static-99R significantly predicted general, sexual, and violent (non-sexual) recidivism. Although this was not the case for the Stable-2007, scores and risk categories from the Stable-2007, when added to the Static-99R, helped predict general, sexual, and violent (non-sexual) recidivism for all three types of recidivism. The second part of this study focused on the latent dimensions of these instruments. Exploratory factor analyses identified 3 dimensions for the Static-99R, namely Youth/Single, Persistence (sexual and non-sexual), and Detached Predatory Conduct, similar to some of those identified by Barbaree et al. (2006). For the Stable-2007, two dimensions were identified, which were Antisociality and Sexual Deviance. However, none of the dimensions extracted for the Static-99R and the Stable-2007 significantly predicted sexual recidivism. The interpretation of these results, the limitations of this study, and possible implications for further research are discussed.