L'imagerie photoacoustique (IPA) des tissus biologiques permet de combiner les avantages des imageries optique et ultrasonore. Le principal contraste endogène pour l’IPA provient des vaisseaux sanguins en raison de la forte absorption de l'hémoglobine par rapport aux tissus environnants. De plus, les vaisseaux sanguins sont à peu près cylindriques et la concentration d'hémoglobine peut être supposée uniforme à l'intérieur des veines. Comme première contribution, nous avons développé dans cette thèse un modèle analytique de fluence optique pour plusieurs inhomogénéités cylindriques parallèles incorporées dans un milieu turbide. Les modèles analytiques n’existent que pour les cas simples. Pour traiter des situations plus complexes, comme les tissus biologiques, les méthodes numériques sont nécessaires. La deuxième contribution de cette thèse consiste à développer un solveur multigrilles de l'équation de diffusion optique et donc de proposer une méthode numérique efficace pour résoudre la fluence optique. Enfin, notre troisième contribution concerne la reconstruction de la tomographie quantitative photoacoustique (TQPA). Basée sur les modèles efficaces présentées dans les première et seconde contributions, nous avons proposé une méthode de reconstruction basée sur le modèle direct analytique pour les cas simples et une méthode d'inversion basée sur multigrille pour les cas plus réalistes. Les avantages de la méthode d'inversion basée sur multigrille sont présentés à la fois en terme de temps de calcul et de vitesse de convergence. Une validation expérimentale est présentée dans le dernier chapitre de cette thèse, prouvant la validité et l'analyse des performances des méthodes développées. / Photoacoustic imaging (PAI) of biological tissues tries to combine the advantages of optical and acoustical imaging. The main endogenous contrast for PAI is derived from blood vessels due to the strong absorption of hemoglobin compared to the background tissues. Furthermore, blood vessels are roughly cylindrical and hemoglobin concentration can be assumed to be uniform inside the vessel. Therefore, the blood vessels can be considered as “cylindrical inhomogeneities”. As a first contribution, we have developed in this thesis an analytical model of optical fluence for multiple parallel cylindrical inhomogeneities embedded in an otherwise homogeneous turbid medium. Analytical models only exist for simple cases. To deal with more complex situations like biological tissues, numerical methods are required. The second contribution of this thesis is to develop a multigrid solver of optical diffusion equation and therefore to propose an efficient numerical method to resolve the optical fluence. Finally, our third contribution is concerned with quantitative PA tomography (QPAT) reconstruction. Based on the efficient models presented in the first and second contributions, we have proposed an analytic-based reconstruction method for simple cases and a multigrid-based inversion scheme for more realistic cases. The advantages of multigrid-based inversion scheme are shown in both computation and convergence speed. An experimental validation is presented in the last chapter of this thesis, proving the validity and analyzing the performances of the developed methods.

L'analyse de la microstructure osseuse joue un rôle important pour étudier des maladies de l'os comme l'ostéoporose. Des nouveaux scanners périphériques haute résolution (HR-pQCT) permettent de faire des acquisitions de la micro-architecture osseuse in-vivo sur l'homme. Toutefois la résolution spatiale de ces appareils reste comparable à la taille des travées osseuses, ce qui limite leur analyse quantitative. L'objectif de cette thèse est de proposer de nouvelles approches jointes super-résolution/ segmentation pour une analyse quantitative plus fine des images HR-pQCT in-vivo de la structure osseuse trabéculaire. Dans une première étape nous nous sommes concentrés sur des méthodes 2D de super-résolution avec régularisation par variation totale (TV) puis par variation totale d'ordre plus élevé (Higher Degree TV), avec minimisation par un algorithme ADMM (Alternating Direction Method of Multipliers). Ensuite, nous avons proposé une méthode itérative combinant le principe de Morozov et la méthode de Newton pour estimer le paramètre de régularisation TV. Comparé à la méthode UPRE (Unbiased Predictive Risk Estimator), la méthode proposée est plus rapide et ne requiert pas un balayage exhaustif des valeurs des paramètres. Nous avons développé dans une deuxième étape une méthode de super-résolution/segmentation conjointe avec un a priori basé sur la Variation Totale et une relaxation convexe (Tvbox), qui permet d'améliorer les paramètres quantitatifs de l'os et de la connectivité 3D. La méthode a été validée sur des images expérimentales micro-CT déteriorées artificiellement. Finalement, en vue de l'application à des images réelles HR-pQCT, nous nous sommes intéressés à une approche conjointe semi-aveugle super-résolution/segmentation qui vise à estimer à la fois l'image binaire super-résolue et le noyau de convolution. Des résultats sur des images micro-CT et HR-pQCT sont présentés. En conclusion, notre travail montre que les méthodes d'optimisation basées sur la régularisation TV sont prometteurs pour améliorer la quantification de la micro-architecture osseuse sur des images HR-pQCT. / The investigation of trabecular bone micro-architecture provides relevant information to determine the bone strength, an important parameter in osteoporosis investigation. While the spatial resolution of clinical CT is not sufficient to resolve the trabecular structure, the High Resolution peripheral Quantitative CT (HR-pQCT) has been developed to investigate bone micro-architecture in-vivo at peripheral sites (tibia and radius). Despite this considerable progress, the quantification of 3D trabecular bone micro-architecture in-vivo remains limited due to a lack of spatial resolution compared to the trabeculae size. The objective of this thesis is to propose new joint super-resolution/segmentation approaches for improving the quantitative analysis of in-vivo HR-pQCT images of the trabecular bone structure. To begin with, we have investigated 2D super-resolution methods based on Total Variation (TV) and Higher Degree Total Variation (HDTV) and Alternating Direction Method of Multipliers (ADMM) minimization. Afterwards, an iterative method combining the Morozov principle and the Newton method was proposed in order to estimate the TV regularization parameter. The proposed method provides a very good regularization parameter only in few iterations compared with the UPRE method that requires an extensive scanning of parameter values. Furthermore, we have developed a 3D joint super-resolution/segmentation method based on a TV a prior with a convex relaxation (TVbox). The validation of the proposed methods was made on experimental micro-CT bone images artificially deteriorated. The results showed an improvement of the bone parameters and 3D connectivity with the TVbox method. Moreover, we have investigated a semi-blind joint super-resolution/ segmentation approach aiming to estimate both the binary super-resolved image and the assumed Gaussian blurring kernel that is not known for the real HR-pQCT images. Results on micro-CT and HR-pQCT experimental bone images were presented. In conclusion, our work has shown that TV based regularization methods promise to improve the quantification of bone micro-architecture from HR-pQCT images.

Les travaux de thèse présentés s’intéressent à l’optimisation des activités d’un bloc opératoire. Ces activités concernent les interventions chirurgicales à planifier et les interventions de maintenance préventive sur les équipements dans les salles d’opération. Une solution est la synchronisation de ces activités lors de la construction du planning opératoire au niveau opératoire. Nous dissocions deux stratégies de programmation opératoire : programmation ouverte et programmation avec allocation préalable des plages horaires aux chirurgiens. Pour chacune des stratégies, nous considérons deux cas : le cas où l’heure de début d’une intervention de maintenance dans la salle est fixée, ladite intervention précédant l’affection des interventions chirurgicales dans les salles. Le second cas étant celui où l’heure de début de maintenance varie dans un intervalle entre une heure de début minimum et une heure de début maximum, avec l’intervention de maintenance placée a posteriori.Nous faisons plusieurs propositions de méthodes (exactes et approchées), y compris une méthode hybride, qui repose sur le couplage entre une métaheuristique et une heuristique. Les résultats obtenus sur des instances générées en concertation avec le monde hospitalier sont intéressants. / The presented dissertation is about the optimization of hospital systems, more precisely the optimization of the activities of an operation theatre. These activities showcase the surgical procedures to be planned and the preventive maintenance interventions on the equipment in the operating rooms. One solution is the synchronization of these activities during the construction of the operational planning at the operational level.We dissociate two operating programming strategies: Open Scheduling or Open programming and Block Scheduling or Programming with prior allocation of times to surgeons. For each strategy two cases are considered: the first case is where the time of beginning of a maintenance intervention in the room is fixed - this intervention preceding the affection of the surgical interventions in the rooms. The second case is where the maintenance start time varies in the interval between a minimum start time and a maximum start time, with the maintenance intervention placed beforehand. We make several proposition’s methods (exact and approximate), including a hybrid method, which is based on the coupling between a metaheuristic and a heuristic. The results obtained on bodies generated in consultation with the hospital’s world are interesting.

Cette thèse se situe dans le cadre de l'analyse théorique et numérique de quelques généralisations de l'équation de Cahn-Hilliard. On étudie l'existence, l'unicité et la régularité de la solution de ces modèles ainsi que son comportement asymptotique en terme d'existence d'un attracteur global de dimension fractale finie. La première partie de la thèse concerne des modèles appliqués à la retouche d'images. D'abord, on étudie la dynamique de l'équation de Bertozzi-Esedoglu-Gillette-Cahn-Hilliard avec des conditions de type Neumann sur le bord et une nonlinéarité régulière de type polynomial et on propose un schéma numérique avec une méthode de seuil efficace pour le problème de la retouche et très rapide en terme de temps de convergence. Ensuite, on étudie ce modèle avec des conditions de type Neumann sur le bord et une nonlinéarité singulière de type logarithmique et on donne des simulations numériques avec seuil qui confirment que les résultats obtenus avec une nonlinéarité de type logarithmique sont meilleurs que ceux obtenus avec une nonlinéarité de type polynomial. Finalement, on propose un modèle basé sur le système de Cahn-Hilliard pour la retouche d'images colorées. La deuxième partie de la thèse est consacrée à des applications en biologie et en chimie. On étudie la convergence de la solution d'une généralisation de l'équation de Cahn-Hilliard avec un terme de prolifération, associée à des conditions aux limites de type Neumann et une nonlinéarité régulière. Dans ce cas, on démontre que soit la solution explose en temps fini soit elle existe globalement en temps. Par ailleurs, on donne des simulations numériques qui confirment les résultats théoriques obtenus. On termine par l'étude de l'équation de Cahn-Hilliard avec un terme source et une nonlinéarité régulière. Dans cette étude, on considère le modèle à la fois avec des conditions aux limites de type Neumann et de type Dirichlet. / This thesis is situated in the context of the theoretical and numerical analysis of some generalizations of the Cahn-Hilliard equation. We study the well-possedness of these models, as well as the asymptotic behavior in terms of the existence of finite-dimenstional (in the sense of the fractal dimension) attractors. The first part of this thesis is devoted to some models which, in particular, have applications in image inpainting. We start by the study of the dynamics of the Bertozzi-Esedoglu-Gillette-Cahn-Hilliard equation with Neumann boundary conditions and a regular nonlinearity. We give numerical simulations with a fast numerical scheme with threshold which is sufficient to obtain good inpainting results. Furthermore, we study this model with Neumann boundary conditions and a logarithmic nonlinearity and we also give numerical simulations which confirm that the results obtained with a logarithmic nonlinearity are better than the ones obtained with a polynomial nonlinearity. Finally, we propose a model based on the Cahn-Hilliard system which has applications in color image inpainting. The second part of this thesis is devoted to some models which, in particular, have applications in biology and chemistry. We study the convergence of the solution of a Cahn-Hilliard equation with a proliferation term and associated with Neumann boundary conditions and a regular nonlinearity. In that case, we prove that the solutions blow up in finite time or exist globally in time. Furthermore, we give numericial simulations which confirm the theoritical results. We end with the study of the Cahn-Hilliard equation with a mass source and a regular nonlinearity. In this study, we consider both Neumann and Dirichlet boundary conditions.

Cette thèse se situe dans le cadre de l'analyse théorique et numérique de modèles en séparation de phase qui tiennent compte d'effets d'anisotropie. Ceci est pertinent, par exemple, pour l'évolution de cristaux dans leur matrice liquide pour lesquels ces effets d'anisotropie sont très forts. On étudie l'existence, l'unicité et la régularité de la solution des équations de Cahn-Hilliard et d'Allen-Cahn ainsi que son comportement asymptotique en terme d'existence d'un attracteur global de dimension fractale finie. La première partie de la thèse concerne certains modèles de séparation de phase qui, en particulier, décrivent la formation de motifs dendritiques. D'abord, on étudie les équations de Cahn-Hilliard et d'Allen-Cahn qui prennent en compte les effets d'anisotropie forts en dimension un avec des conditions de type Neumann sur le bord et une non linéarité régulière de type polynomial. En particulier, ces modèles contiennent un terme supplémentaire appelé régularisation de Willmore. Ensuite, on étudie ces modèles avec des conditions de type périodique (respectivement, Dirichlet) sur le bord pour l'équation de Cahn-Hilliard (respectivement, d'Allen-Cahn) mais en dimension spatiales plus élevées. Finalement, on étudie la dynamique des équations de Cahn-Hilliard et d'Allen-Cahn visqueux avec des conditions de type Neumann et Dirichlet respectivement sur le bord et une non linéarité régulière et en plus, la présence de simulations numériques qui montrent les effets du terme de viscosité sur l'anisotropie et l'isotropie dans l'équation de Cahn-Hilliard. Dans le dernier chapitre, on étudie le comportement en temps long en termes d'attracteurs de dimension finie, d'une classe d'équations doublement non linéaires de type Allen-Cahn avec des conditions de type Dirichlet sur le bord et une non linéarité singulière. / This thesis is situated in the context of the theoretical and numerical analysis of models in phase separation which take into account the anisotropic effects. This is relevant, for example, for the development of crystals in their liquid matrix for which the effects of anisotropy are very strong. We study the existence, uniqueness and the regularity of the solution of Cahn-Hilliard and Alen-Cahn equations and the asymptotic behavior in terms of the existence of a global attractor with finite fractal dimension. The first part of the thesis concerns some models in phase separation which, in particular, describe the formation of dendritic patterns. We start by study- ing the anisotropic Cahn-Hilliard and Allen-Cahn equations in one space dimension both associated with Neumann boundary conditions and a regular nonlinearity. In particular, these two models contain an additional term called Willmore regularization. Furthermore, we study these two models with Periodic (respectively, Dirichlet) boundary conditions for the Cahn-Hilliard (respectively, Allen-Cahn) equation but in higher space dimensions. Finally, we study the dynamics of the viscous Cahn-Hilliard and Allen-Cahn equations with Neumann and Dirichlet boundary conditions respectively and a regular nonlinearity in the presence of the Willmore regularization term and we also give some numerical simulations which show the effects of the viscosity term on the anisotropic and isotropic Cahn-Hilliard equations. In the last chapter, we study the long time behavior, in terms of finite dimensional attractors, of a class of doubly nonlinear Allen-Cahn equations with Dirichlet boundary conditions and singular potentials.

Cette thèse est consacrée à l'analyse mathématique et numérique pour les problèmes de transport partiel optimal et d'appariement avec contrainte (constrained matching problem). Ces deux problèmes présentent de nouvelles quantités inconnues, appelées parties actives. Pour le transport partiel optimal avec des coûts qui sont donnés par la distance finslerienne, nous présentons des formulations équivalentes caractérisant les parties actives, le potentiel de Kantorovich et le flot optimal. En particulier, l'EDP de condition d'optimalité permet de montrer l'unicité des parties actives. Ensuite, nous étudions en détail des approximations numériques pour lesquelles la convergence de la discrétisation et des simulations numériques sont fournies. Pour les coûts lagrangiens, nous justifions rigoureusement des caractérisations de solution ainsi que des formulations équivalentes. Des exemples numériques sont également donnés. Le reste de la thèse est consacré à l'étude du problème d'appariement optimal avec des contraintes pour le coût de la distance euclidienne. Ce problème a un comportement différent du transport partiel optimal. L'unicité de solution et des formulations équivalentes sont étudiées sous une condition géométrique. La convergence de la discrétisation et des exemples numériques sont aussi établis. Les principaux outils que nous utilisons dans la thèse sont des combinaisons des techniques d'EDP, de la théorie du transport optimal et de la théorie de dualité de Fenchel--Rockafellar. Pour le calcul numérique, nous utilisons des méthodes du lagrangien augmenté. / The manuscript deals with the mathematical and numerical analysis of the optimal partial transport and optimal constrained matching problems. These two problems bring out new unknown quantities, called active submeasures. For the optimal partial transport with Finsler distance costs, we introduce equivalent formulations characterizing active submeasures, Kantorovich potential and optimal flow. In particular, the PDE of optimality condition allows to show the uniqueness of active submeasures. We then study in detail numerical approximations for which the convergence of discretization and numerical simulations are provided. For Lagrangian costs, we derive and justify rigorously characterizations of solution as well as equivalent formulations. Numerical examples are also given. The rest of the thesis presents the study of the optimal constrained matching with the Euclidean distance cost. This problem has a different behaviour compared to the partial transport. The uniqueness of solution and equivalent formulations are studied under geometric condition. The convergence of discretization and numerical examples are also indicated. The main tools which we use in the thesis are some combinations of PDE techniques, optimal transport theory and Fenchel--Rockafellar dual theory. For numerical computation, we make use of augmented Lagrangian methods.

Les systèmes d’imagerie microonde suscitent un grand intérêt actuellement dans le domaine de la recherche, notamment pour des applications de sécurité (scanners corporels, vision à travers les murs, etc). Plusieurs techniques d’acquisition déjà existantes permettent d’optimiser l’ouverture rayonnante afin de garantir une bonne résolution sur l’image finale. Cependant, le verrou actuel des systèmes d’imagerie est de pouvoir atteindre un temps de rafraîchissement temps réel et d’adresser un grand nombre d’antennes. La majorité des systèmes actuels peinent à concilier la rapidité et la résolution, tout en garantissant une bonne sensibilité. Les travaux réalisés dans ce manuscrit visent à proposer une alternative aux systèmes existants en se basant sur des techniques de codage analogique des signaux d’antennes. Globalement, l’objectif est de minimiser le nombre de récepteurs sans affecter les performances. Les architectures proposées sont essentiellement basées sur le concept du Radar MIMO (pour les systèmes actifs) et du radiomètre à synthèse d’ouverture interférométrique ou SAIR (pour les systèmes passifs). Ces deux systèmes permettent de réduire considérablement le nombre d’antennes sans affecter la résolution de l’image, ce qui permet une première levée de contraintes. En sus, des composants compressifs entièrement passifs sont utilisés pour réduire le nombre de récepteurs des systèmes Radar MIMO et SAIR. Ces composants à diversité spatiale et fréquentielle présentent des fonctions de transfert orthogonales. Utilisés en émission, ils permettent un adressage simultané et indépendant des antennes du réseau. En réception, ils permettent de coder les signaux reçus par les antennes vers un nombre de voies RF considérablement réduit. En appliquant des techniques de décodage appropriées, les signaux reçus par chacune des antennes peuvent être estimées afin d’appliquer les algorithmes dédiés à la reconstruction de l’image. Ces composants offrent l’avantage de réduire fortement le nombre de voies RF tout en conservant la même ouverture rayonnante et en autorisant une acquisition simultanée des signaux. Des démonstrateurs laboratoires ont été réalisés en bande S afin de montrer une preuve de faisabilité des alternatives proposées. Enfin, les résultats obtenus ont fait l'objet d'une demande de brevet et un prototype d'imageur radiométrique à ondes millimétriques est en cours de prototypage dans le cadre du projet ANR-PIXEL. / Microwave imaging systems are currently attracting great attention in the field of research, especially for security applications (body scanners, vision through walls, etc.). Several acquisition techniques already exist to optimize the antenna aperture in order to guarantee a good resolution on the final image. However, the current lock of imaging systems is to be able to achieve a real-time acquisition and address numerous antennas. Most of the current systems struggle to reconcile fast imaging and resolution while ensuring good sensitivity. The work carried out in this manuscript aims at proposing an alternative to the existing systems based on analog coding techniques of the antenna signals. Overall, the goal is to minimize the number of receivers without affecting performances. The proposed architectures are based essentially on the concept of the MIMO radar (for active systems) and the Synthetic Aperture Interferometric Radiometer or SAIR (for passive systems). These two systems allow a significant reduction of the number of antennas without affecting the resolution of the image, thus enabling a first lifting of constraints. In addition, passive compressive components are used to reduce the number of receivers in the MIMO Radar and the SAIR systems. These components with spatial and frequency diversity exhibit orthogonal transfer functions. Used in transmission, they allow simultaneous and independent addressing of each element of the antenna array. In reception, they allow the signals received by the antennas to be coded into a considerably reduced number of aggregate waveforms. By applying suitable decoding techniques, the signals received by each antenna can be estimated in order to apply imaging algorithms. These components offer the advantage of greatly reducing the number of RF channels while keeping the same number of antennas and allowing simultaneous acquisition of the signals. Laboratory demonstrators were carried out in S-band to demonstrate the feasibility of the proposed alternatives. Finally, the results obtained were the subject of a patent application and a prototype of a millimeter-wave radiometric imager is being developed in the framework of the ANR-PIXEL project.

Le développement massif des énergies renouvelables intermittentes dans les systèmes de puissance affecte le fonctionnement des systèmes électriques. En raison des techniques limitées et des investissements nécessaires pour maintenir le niveau de sécurité électrique actuel, les questions liées à l'envoi, à la stabilité statique et dynamique pourraient arrêter le développement de ces sources. Le sujet de la thèse est de développer un outil pour mesurer l'incertitude sur la disponibilité de la puissance produite par les générateurs photovoltaïques dans un réseau urbain. Premièrement, l'incertitude est modélisée par l'étude de la nature incertaine de la PV énergie production et de la charge. Avec les méthodes stochastiques, on calcule la réserve de puissance (OR) un jour d'avance en tenant compte d'un indice de risque de fiabilité associé. Ensuite, l'OR est distribué en différents générateurs (générateurs photovoltaïques actifs et micro-turbines à gaz). Afin de minimiser le coût opérationnel total et/ou les émissions équivalentes de CO2, une planification optimale et une répartition quotidienne de l'OR dans différents générateurs d'énergie sont mises en œuvre. Enfin, un logiciel libre «Un système de gestion de l'énergie convivial et un superviseur de la planification opérationnelle» est développé à partir de l'interface utilisateur graphique de Matlab pour conceptualiser le fonctionnement global du système. / The massive development of intermittent renewable energy technologies in power systems affects the operation of electrical systems. Due to technical limitations and investments needed to maintain the current electrical security level, issues related to dispatching, static and dynamic stability could stop the development of these distributed renewable energy sources (RES). The subject of the PhD is to develop a tool to study the uncertainties of PV power and load forecasting in an urban network. Firstly, the uncertainties are modeled by studying the uncertainty nature of PV power and load. With stochastic methods, the day-ahead operating reserve (OR) is quantified by taking into account an associated reliability risk index. Then the OR is dispatched into different power generators (active PV generators and micro gas turbines). To minimize the microgrid total operational cost and/or equivalent CO2 emissions, day-ahead optimal operational planning and dispatching of the OR into different power generators is implemented. Finally, a freeware “A User-friendly Energy Management System and Operational Planning Supervisor” is developed based on the Matlab GUI to conceptualize the overall system operation

Cette thèse est consacrée à l'étude de plusieurs problèmes d'équations aux dérivées partielles non-linéaires.<p><p>La première partie (chapitres 1-2-3) traite d'un problème trouvant son origine en biologie mathématique, à savoir l'étude de la survie à long terme d'une population dont l'évolution est gouvernée par une équation parabolique non-linéaire. Dans le modèle considéré, le mécanisme de diffusion est contrôlé par le p-Laplacien, la non-linéarité est de type logistique et fait intervenir un poids m pouvant changer de signe, et les conditions aux limites sont de flux nul. Le poids m correspond à une répartition des ressources devant permettre la survie de la population. Dans le chapitre 1, nous déterminons entre autres un critère de survie à long terme faisant intervenir la valeur propre principale du p-Laplacien avec poids m. Cette valeur propre apparait, plus précisément, comme la valeur limite d'un paramètre en-dessous de laquelle toute solution positive de l'équation converge vers zéro lorsque t tend vers l'infini. Ceci nous conduit naturellement au problème de minimiser la valeur propre en question lorsque m varie dans une classe adéquate de poids. Dans le chapitre 2, nous prouvons l'existence de minimiseurs et montrons que ces derniers satisfont une propriété de type “bang-bang”. Plusieurs propriétés de montonie sont aussi étudiées dans des situations géométriques particulières, et une caractérisation complète est donnée en dimension 1. Le chapitre 3 est consacré à l'élaboration de simulations numériques, où l'algorithme utilisé combine un méthode de plus grande pente avec une représentation de certains ensembles comme ensembles de niveaux.<p><p>La deuxième sujet de cette thèse (chapitre 4) est un problème elliptique faisant intervenir l'opérateur de courbure moyenne. Nous nous intéressons à l'existence et à la multiplicité de solutions nodales de ce problème. Nous montrons que, si un certain paramètre de l'équation est suffisamment grand, il existe une solution nodale qui change de signe exactement deux fois. Nous établissons également l'existence d'un nombre arbitrairement grand de solutions nodales. Enfin, dans le cas particulier où le domaine est une boule, un résultat de brisure de symétrie est obtenu, résultat qui induit l'existence d'au moins deux solutions à deux domaines nodaux. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct.<p>One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'étude de nouveaux algorithmes et structures de données dont l'usage est destiné à la vérification de programmes. Les ordinateurs sont de plus en plus présents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confiés des tâches de nature critique pour la sécurité. Ces systèmes sont caractérisés par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement désastreux, que ce soit en pertes humaines, dégâts environnementaux, ou économiques. Pour ces systèmes critiques, les concepteurs de systèmes industriels prônent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction.<p><p>Une des techniques de vérification de programmes les plus utilisées est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a états finis. Après cette phase d'abstraction, des propriétés (typiquement sous la forme d'une formule de logique temporelle) peuvent êtres vérifiées sur l'abstraction à espace d'états fini, à l'aide d'outils de vérification automatisés. Les automates alternants jouent un rôle important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent êtres traduites efficacement vers ces automates. Cette caractéristique des automates alternants permet de réduire le model checking des logiques temporelles à des questions sur les automates, ce qui est appelé l'approche par automates du model checking. Dans ce travail, nous étudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premièrement, nous appliquons l'approche par antichaînes (utilisée précédemment avec succès pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problèmes de satisfaisabilité et du model checking de la logique temporelle linéaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaînes avec l'usage des ROBDD, dans le but de gérer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates générés à partir de LTL. Deuxièmement, nous développons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaînes et de l'interprétation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous définissons une nouvelle structure de données, appelée LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implémentations et ont été validés expérimentalement. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished