Cette thèse étudie l’intérêt de la mesure de la diffusion cohérente de rayons X dans le cadre de l’imagerie du sein à des fins de diagnostic. Aujourd'hui, la plupart des systèmes d'imagerie médicale par rayons X exploitent le rayonnement transmis à travers les tissus. C’est le cas pour la mammographie, qui est la modalité d’imagerie du sein la plus courante. L'apparition récente de détecteurs résolus en énergie, à base de semi-conducteurs notamment, permet cependant d'envisager l'exploitation en milieu clinique d'un autre phénomène : le rayonnement diffusé cohérent. La mesure de spectres de diffusion peut apporter de nouvelles informations liées à la structure moléculaire des tissus examinés pour mieux les caractériser et ainsi améliorer le diagnostic final. Deux modalités sont envisagées : la détection in vivo de tumeurs du sein, à la suite d’une mammographie présentant un résultat suspect ou l'analyse de biopsie.Le système de mesure de diffusé développé lors de cette thèse exploite les détecteurs résolus en énergie de type CdZnTe, ces derniers présentant des caractéristiques (résolution en énergie, sensibilité, résolution spatiale, compacité) prometteuses pour une utilisation en condition clinique. Il se base par ailleurs sur la pixellisation du détecteur afin de proposer une modalité d’imagerie permettant de caractériser les matériaux ou tissus traversés dans une direction sans translation ni rotation.Cette thèse propose ainsi une étude complète de ce système, articulée autour de trois grandes parties : modélisation puis simulation du système de mesure, développement du traitement des données mesurées par le détecteur afin d’imager et caractériser l’échantillon analysé et enfin, dimensionnement d’un banc expérimental plus complexe intégrant un détecteur complet et un système de collimation multifente. Ces trois parties font par ailleurs l’objet de validations expérimentales associées. / This thesis studies the interest of measuring the coherent scattering of X-rays for breast diagnosis imaging. Nowadays, most of X-ray-based medical imaging techniques use the information of X-rays attenuation through the tissues. It is the case for mammography, the most common breast imaging modality. The recent emergence of energy resolved detectors (based on semiconductors in particular) allows to consider using another phenomenon: the coherent X-ray scattering. Measurement of diffracted spectra can provide new information related to the molecular structure of the examined tissues, in order to improve their characterization and therefore improve the final diagnosis. Two modalities are considered: the breast cancer detection in vivo, following a suspicious mammography result, or biopsy analysis.The coherent scattering measurement system developed during this thesis work uses energy-resolved CdZnTe-based detectors, these detectors combining performances (energy resolution, sensitivity, spatial resolution, and compactness) promising for clinical application. This system is also based on the detector pixelation, which allows to provide an imaging modality capable of characterizing analyzed materials or tissues in one direction without any translation or rotation.A complete study of the measurement system is proposed in this thesis, structured in three main parts: modeling and simulation of the system, development of the processing of the data measured by the detector in order to image and characterize the analyzed sample and finally, designing of a new and more complex experimental setup based on a whole detector and multislit collimation system. An experimental validation is proposed for each of these three parts.

Résumé non communiqué / Résumé non communiqué

Dans cette thèse, on étudie des problèmes liés à la vérification de systèmes (logiciels). On s’intéresseplus particulièrement à la conception sûre de procédures de décision utilisées en vérification. De plus, onconsidère également un problème de modularité pour un langage de modélisation utilisé dans la plateformede vérification Why.De nombreux problèmes de vérification peuvent se réduire à un problème de satisfaisabilité modulodes théories (SMT). Pour construire des procédures de satisfaisabilité, Armando et al. ont proposé en2001 une approche basée sur la réécriture. Cette approche utilise un calcul général pour le raisonnementéquationnel appelé paramodulation. En général, une application équitable et exhaustive des règles ducalcul de paramodulation (PC) conduit à une procédure de semi-décision qui termine sur les entréesinsatisfaisables (la clause vide est alors engendrée), mais qui peut diverger sur les entrées satisfaisables.Mais ce calcul peut aussi terminer pour des théories intéressantes en vérification, et devient ainsi uneprocédure de décision. Pour raisonner sur ce calcul, un calcul de paramodulation schématique (SPC)a été étudié, en particulier pour prouver automatiquement la décidabilité de théories particulières etde leurs combinaisons. L’avantage de ce calcul SPC est que s’il termine sur une seule entrée abstraite,alors PC termine pour toutes les entrées concrètes correspondantes. Plus généralement, SPC est unoutil automatique pour vérifier des propriétés de PC telles que la terminaison, la stable infinité et lacomplétude de déduction.Une contribution majeure de cette thèse est un environnement de prototypage pour la conception etla vérification de procédures de décision. Cet environnement, basé sur des fondements théoriques, estla première implantation du calcul de paramodulation schématique. Il a été complètement implanté surla base solide fournie par le système Maude mettant en oeuvre la logique de réécriture. Nous montronsque ce prototype est très utile pour dériver la décidabilité et la combinabilité de théories intéressantes enpratique pour la vérification.Cet environnement est appliqué à la conception d’un calcul de paramodulation schématique dédié àune arithmétique de comptage. Cette contribution est la première extension de la notion de paramodulationschématique à une théorie prédéfinie. Cette étude a conduit à de nouvelles techniques de preuveautomatique qui sont différentes de celles utilisées manuellement dans la littérature. Les hypothèses permettantd’appliquer nos techniques de preuves sont faciles à satisfaire pour les théories équationnellesavec opérateurs de comptage. Nous illustrons notre contribution théorique sur des théories représentantdes extensions de structures de données classiques comme les listes ou les enregistrements.Nous avons également contribué au problème de la spécification modulaire pour les classes et méthodesJava génériques. Nous proposons des extensions du language de modélisation Krakatoa, faisant partiede la plateforme Why qui permet de prouver qu’un programme C ou Java est correct par rapport à saspécification. Les caractéristiques essentielles de notre apport sont l’introduction de la paramétricité à lafois pour les types et les théories, ainsi qu’une relation d’instantiation entre les théories. Les extensionsproposées sont illustrées sur deux exemples significatifs: tri de tableaux et fonctions de hachage.Les deux problèmes traités dans cette thèse ont pour point commun les solveurs SMT. Les procéduresde décision sont les moteurs des solveurs SMT, et la plateforme Why engendre des conditions devérification dérivées d’un programme source annoté, qu’elle transmet aux solveurs SMT (ou assistants depreuve) pour vérifier la correction du programme.Mots-clés: / In this thesis we address problems related to the verification of software-based systems. We aremostly interested in the (safe) design of decision procedures used in verification. In addition, we alsoconsider a modularity problem for a modeling language used in the Why verification platform.Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In orderto build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting.This approach uses a general calculus for equational reasoning named paramodulation. In general, afair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decisionprocedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge onsatisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thusit becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulationcalculus (SPC) has been studied, notably to automatically prove decidability of single theories and oftheir combinations. The advantage of SPC is that if it halts for one given abstract input, then PC haltsfor all the corresponding concrete inputs. More generally, SPC is an automated tool to check propertiesof PC like termination, stable infiniteness and deduction completeness.A major contribution of this thesis is a prototyping environment for designing and verifying decisionprocedures. This environment, based on the theoretical studies, is the first implementation of theschematic paramodulation calculus. It has been implemented from scratch on the firm basis provided bythe Maude system based on rewriting logic. We show that this prototype is very useful to derive decidabilityand combinability of theories of practical interest in verification. It helps testing new saturationstrategies and experimenting new extensions of the original (schematic) paramodulation calculus.This environment has been applied for the design of a schematic paramodulation calculus dedicated tothe theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulationto a built-in theory. This study has led to new automatic proof techniques that are different fromthose performed manually in the literature. The assumptions to apply our proof techniques are easyto satisfy for equational theories with counting operators. We illustrate our theoretical contribution ontheories representing extensions of classical data structures such as lists and records.We have also addressed the problem of modular specification of generic Java classes and methods.We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for provingthat a Java or C program is a correct implementation of some specification. The key features arethe introduction of parametricity both for types and for theories and an instantiation relation betweentheories. The proposed extensions are illustrated on two significant examples: the specification of thegeneric method for sorting arrays and for generic hash map.Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures areat the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a sourceprogram annotated by specifications, and then transmits them to SMT solvers or proof assistants to checkthe program correctness.

Au cours des six dernières décennies, la culture cellulaire est devenue une pratique courante. Elle est un outil majeur de la recherche biologique pour la compréhension du vivant, l'étude de maladies et la découverte de nouveaux médicaments. Elle représente un outil très répandu dans de nombreuses industries étant impliquées dans la production de produits alimentaires, cosmétiques et pharmaceutiques.Cependant, les cultures cellulaires en recherche et en industrie sont aujourd'hui confrontées à des limites et soulèvent des besoins à satisfaire. Elles sont toutes deux associées à des coûts élevés du fait des ressources nécessaires (cellules, réactifs, opérateurs qualifiés). Plus précisément, la culture en recherche est caractérisée par le faible débit des expériences, une variabilité importante et un risque de contamination due à la répétition d'opérations manuelles. De plus, les expériences de culture sont effectuées dans des conditions statiques et sur des modèles (cultures 2D, animaux...) relativement éloignés de la physiologie humaine. La culture cellulaire industrielle, quant à elle, a besoin de systèmes miniaturisés qui miment les procédés des bioréacteurs à grande échelle et qui offrent des possibilités de criblage plus élevés.Les systèmes de culture microfluidique représentent un outil prometteur pour résoudre ces problèmes et ces besoins. Le changement de comportement de la physique à petite échelle dans ces dispositifs permet de contrôler temporellement et spatialement le microenvironnement des cellules. Ce qui n'est pas possible avec des méthodes de culture classiques. Le degré d'automatisation et d'intégration permet une nette augmentation du nombre d'expériences par système et la réduction conséquente de la consommation de ressources. Ainsi, de nombreuses petites architectures 3D cellulaires cultivées dans des conditions dynamiques et à haut débit ont été réalisées et ont démontré leur capacité à recréer rapidement des environnements plus physiologiques. En ce qui concerne la culture industrielle, des cultures miniaturisées ont déjà montré leur capacité à reproduire les caractéristiques observées dans les macrobioreactors avec des possibilités de criblages élevées.Dans ce contexte, un bioréacteur microfluidique de paillasse, se conformant aux formats standards utilisés dans le laboratoire d'accueil, a été fabriqué avec succès au cours de cette thèse pour effectuer des cultures cellulaires en continu. Des solutions intégrées ont été mises au point pour fournir de façon continue les conditions adéquates pour la prolifération cellulaire (perfusion, régulation de température…). Des études ont également été menées afin d'automatiser la récolte des cellules avec pour but final de cultiver ces cellules sur du long terme dans le bioréacteur.Le système fabriqué garantit ainsi des conditions stériles pour les cultures sur un simple banc de laboratoire. En outre, ces cultures ont été réalisées de façon autonome sans utiliser un incubateur encombrant. Dans ces conditions, le bioréacteur permet de réaliser des cultures en continu de divers types cellulaires sur plusieurs jours: des cellules d'insectes ont été cultivées pendant 5 jours et des cellules de mammifère pendant 3 jours. En ce qui concerne les cultures de cellules de mammifère, une avancée majeure a été effectuée par rapport aux cultures réalisées dans les systèmes microfluidiques en utilisant comme support de culture des microporteurs (diam. : 175 µm).Bien que la culture de cellules sur microporteurs soit réalisée en routine dans l'industrie, aucun système de culture microfluidique autonome n'a encore intégré ce type de culture. Ce genre de miniaturisation est une avancée majeure pour des applications en bioprocédés où il devrait permettre de raccourcir et réduire les coûts associés au développement de bioproduits. / Over the past six decades, cell culture has become a common practice. It is a major tool in biological research for the understanding of life science, such as the study of disease and the discovery of new drugs. It plays an important role in many industries since it is involved in the production of many food, cosmetic, and pharmaceutical products.However, Research and the industry are now facing some limits and are expressing needs to be addressed. They are both associated with high costs due to a large consumption of resources (cells, reagents, qualified operators). More specifically, cell culture in research is characterized by low throughput of experiments, important variability and risk of contamination due to the recurrent manual operations performed by operators. Additionally, experiments are performed in static conditions and on models (2D cultures, animals…) which poorly resemble the human physiology. Industrial cell culture needs miniaturized systems that mimic the large scale bioreactors and offer higher screening possibilities.Microfluidic cell culture systems represent a promising tool to address the aforementioned issues and needs. The change of physical behaviors at the small-scale in microfluidic devices allow controlling temporally and spatially the cell microenvironment, unattainable with conventional cell culture methods. The level of automation and integration allows the substantial increase of the number of experience per system and considerable reduction of resource consumption. Thus, many small cellular 3D architectures grown under dynamic conditions and in high-throughput have been performed and have demonstrated their ability to quickly re-create more physiological environments. Regarding the industrial culture, miniaturized cultures have already shown their ability to reproduce the characteristics of the culture observed in macrobioreactors with higher screening capabilities.In this framework, a benchtop microfluidic bioreactor, complying with the standard microfluidic platform and format used in the host laboratory, has been successfully fabricated to perform continuous cell cultures. Integrated solutions were developed to provide continuously the adequate conditions for cell proliferation (perfusion, thermal regulation…). Integrated cell harvest was also performed with the final goal to achieve long-term cell culture in the bioreactor.The fabricated system proved to guarantee sterile conditions for cell cultures on a regular lab bench. Moreover, these cultures were achieved autonomously without requiring a cumbersome incubator. In these conditions, the bioreactor demonstrated the possibility to perform continuous cell cultures of various cell types during several days: insects cells were cultured during 5 days and mammalian cells during 3 days. Regarding the mammalian cell cultures performed, a breakthrough has been achieved compared to the cultures performed in microfluidic systems since microcarriers (diam.:175 µm) were used as growth support.Although microcarrier cell culture is routinely performed in the industry, no autonomous microfluidic culture system has addressed this type of culture yet. Such a miniaturization is a major step forward for bioprocess applications where the need to develop scale-down bioreactors that mimic large scale operation has been clearly identified to shorten and reduce the costs associated to bioproduct development.