info:eu-repo/semantics/nonPublished

info:eu-repo/semantics/nonPublished

Les problèmes logiciels sont frustrants et diminuent l’expérience utilisateur. Par exemple, la fuite de données bancaires, la publication de vidéos ou de photos compromettantes peuvent affecter gravement une vie. Comment éviter de telles situations ? Utiliser des tests est une bonne stratégie, mais certains bogues persistent. Une autre solution est d’utiliser des méthodes plus mathématiques, aussi appelées méthodes formelles. Parmi celles-ci se trouve la sémantique dénotationnelle. Elle met la sémantique extraite de vos logiciels préférés en correspondance avec des objets mathématiques. Sur ceux-ci, des propriétés peuvent être vérifiées. Par exemple, il est possible de déterminer, sous certaines conditions, si votre logiciel donnera une réponse. Pour répondre à ce besoin, il est nécessaire de s’intéresser à des théories mathématiques suffisamment riches. Parmi les candidates se trouvent le sujet de ce mémoire : la théorie des domaines. Elle offre des objets permettant de modéliser formellement les données et les instructions à l’aide de relations d’ordre. Cet écrit présente les concepts fondamentaux tout en se voulant simple à lire et didactique. Il offre aussi une base solide pour des lectures plus poussées et contient tout le matériel nécessaire à sa lecture, notamment les preuves des énoncés présentés. / Bugs in programs are definitively annoying and have a negative impact on the user experience. For example, leaks of bank data or leaks of compromising videos or photos have a serious effect on someone’s life. How can we prevent these situations from happening? We can do tests, but many bugs may persist. Another way is to use mathematics, namely formal methods. Among them, there is denotational semantics. It links the semantics of your favorite program to mathematical objects. On the latter, we can verify properties, e.g., absence of bugs. Hence, we need a rich theory in which we can express the denotational semantics of programs. Domain Theory is a good candidate and is the main subject of this master thesis. It provides mathematical objects for data and instructions based on order relations. This thesis presents fundamental concepts in a simple and pedagogical way. It is a solid basis for advanced readings as well as containing all the needed knowledge for its reading, notably proofs for all presented statements.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Dans cette thèse, nous présentons les relations entre le principe de réflexion MRP introduit par Moore, les propriétés d'arbres généralisées ITP et ISP introduites par Weiß, ainsi que les propriétés square introduites par Jensen et développées par Schimmerling. Le résultat principal de cette thèse est que MRP+MA entraine ITP(λ, ω2) pour tout cardinal λ ≥ ω2. Ce résultat implique par conséquent que les méthodes actuelles pour prouver la consistance de MRP+MA nécessitent au moins l'existence d'un cardinal supercompact. Il s'avère que MRP seul ne suffit pas à démontrer ce résultat, et nous donnons la démonstration que MRP n'entraine pas la propriété d'arbre plus faible, à savoir TP(ω2, ω2). De plus MRP+MA n'entraine pas le principe d'arbre plus fort ISP(ω2, ω2). Enfin nous étudions les relations entre MRP et des versions faibles de square. Nous montrons que MRP implique la négation de square(λ, ω) et MRP+MA implique la négation de square(λ, ω1) pour tout λ ≥ ω2.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Dans ces travaux de thèse nous proposons de tirer parti de la théorie des ensembles flous afin d'améliorer les interactions entre les systèmes de bases de données et les utilisateurs. Les mécanismes coopératifs visent à aider les utilisateurs à mieux interagir avec les SGBD. Ces mécanismes doivent faire preuve de robustesse : ils doivent toujours pouvoir proposer des réponses à l'utilisateur. Empty set (0,00 sec) est un exemple typique de réponse qu'il serait désirable d'éradiquer. Le caractère informatif des explications de réponses est parfois plus important que les réponses elles-mêmes : ce peut être le cas avec les réponses vides et pléthoriques par exemple, d'où l'intérêt de mécanismes coopératifs robustes, capables à la fois de contribuer à l'explication ainsi qu'à l'amélioration des résultats. Par ailleurs, l'utilisation de termes de la langue naturelle pour décrire les données permet de garantir l'interprétabilité des explications fournies. Permettre à l'utilisateur d'utiliser des mots de son propre vocabulaire contribue à la personnalisation des explications et améliore l'interprétabilité. Nous proposons de nous intéresser aux explications dans le contexte des réponses coopératives sous trois angles : 1) dans le cas d'un ensemble pléthorique de résultats ; 2) dans le contexte des systèmes de recommandation ; 3) dans le cas d'une recherche à partir d'exemples. Ces axes définissent des approches coopératives où l'intérêt des explications est de permettre à l'utilisateur de comprendre comment sont calculés les résultats proposés dans un effort de transparence. Le caractère informatif des explications apporte une valeur ajoutée aux résultats bruts, et forme une réponse coopérative. / In this thesis, we are interested in how we can leverage fuzzy logic to improve the interactions between relational database systems and humans. Cooperative answering techniques aim to help users harness the potential of DBMSs. These techniques are expected to be robust and always provide answer to users. Empty set (0,00 sec) is a typical example of answer that one may wish to never obtain. The informative nature of explanations is higher than that of actual answers in several cases, e.g. empty answer sets and plethoric answer sets, hence the interest of robust cooperative answering techniques capable of both explaining and improving an answer set. Using terms from natural language to describe data --- with labels from fuzzy vocabularies --- contributes to the interpretability of explanations. Offering to define and refine vocabulary terms increases the personalization experience and improves the interpretability by using the user's own words. We propose to investigate the use of explanations in a cooperative answering setting using three research axes: 1) in the presence of a plethoric set of answers; 2) in the context of recommendations; 3) in the context of a query/answering problem. These axes define cooperative techniques where the interest of explanations is to enable users to understand how results are computed in an effort of transparency. The informativeness of the explanations brings an added value to the direct results, and that in itself represents a cooperative answer.

En sciences économiques, l'une des questions centrales concerne l'allocation des ressources rares et plus particulièrement leur répartition. La décision apparait ainsi au cœur des thématiques économiques, que ce soit en micro-économie ou en macro-économie. Dans un premier temps, nous revenons sur le fait que l’information, élément central de la prise de décision, est imparfaite. En utilisant la théorie des ensembles flous, qui a pour objet de capturer l’imprécision, nous construisons un nombre flou nommé nombre flou C-Shape qui permet de capter la sensibilité du preneur de décision. Nous étudions ensuite la théorie de la décision au travers de deux axes de recherche à savoir (1) la recherche opérationnelle couplée à la théorie des jeux et (2) l’aide à la décision. En premier lieu, Nous faisons une analogie entre la fonction distance et la fonction d’appartenance. Grâce à l’hypothèse de B-convexité et à la fonction C-Shape nous construisons des classes de jeux pour lesquels les joueurs peuvent être optimistes, pessimistes ou neutres, et pour lesquels l’existence d’équilibre de Nash est avérée. Enfin, concernant l’aide à la décision, nous utilisons la fonction C-Shape pour caractériser un nouveau type de critère nommé pseudo critère C-Shape qui permet de considérer les alternatives comme substituables. Ceci permet de prendre en compte, par exemple le contexte institutionnel dans lequel la prise de décision est prise. / Determining the allocation and the distribution of scarce resources is fundamental in economics. Thus, decision theory is the cornerstone of economic theory. In this thesis, we first provide a state of the art insisting on the fact that information, that is a central element of decision-making, is imperfect. Secondly, using fuzzy set theory, which aims to capture imprecision, we construct a fuzzy number, so-called C-Shape that captures the sensitivity of the decision-maker. Thirdly, we study decision theory through two key concepts of operation research: (1) game theory and (2) multi-criteria decision making. We provide an analogy between the gauge functions of convex sets and the membership functions arising in fuzzy set theory. Coupling a suitable notion of -convexity with the C-Shape function, we introduce a class of games for which the players can be optimistic, pessimistic or neutral. In addition the existence of Nash equilibrium is proved for such a class of games. Finally, concerning multi-criteria decision analysis, we use the C-Shape functions to characterize a new type of criteria called C-Shape pseudo-criterion, which makes possible to consider the alternatives as substitutable. This should be of interest to take into account, for example, the institutional context in which decision-making is taken.

Cette thèse vise à utiliser la modélisation mathématique avec les outils du contrôle avancé, afin de guider les thérapies pour assurer la contraction de la tumeur. Les buts de cette thèse sont la contribution au développement des méthodes de la théorie des ensembles pour le contrôle robuste des systèmes non linéaires et le développement d’outils numériques pour l’analyse et le contrôle de la croissance tumorale en présence de chimiothérapie et=ou de traitement anti-angiogénique. Génériquement, dans le contexte de la théorie du contrôle, les techniques qui sont théoriquement basées sur certaines propriétés des sous-ensembles de l’espace d’état du système pourraient être désignées comme des méthodes de la théorie des ensembles. Dans la première partie, nous passons en revue les définitions, concepts et outils de la théorie des ensembles existants dans la littérature pour réponde efficacement à des problématiques de contrôle des systèmes linéaires et non linéaires avec contraintes dures et incertitudes. Dans ce cadre, nous nous intéressons à deux propriétés des ensembles qui sont l’invariance et la contraction. Les problèmes liés à la stabilité des systèmes peuvent être formulés en termes de calcul de leurs domaines d’attraction. Pour des fins de développement, nous rappelons les méthodes de la littérature pour la caractérisation de ces domaines d’attraction pour les systèmes linéaires et non linéaires. Une application importante de ces méthodes est le contrôle de la croissance tumorale en présence de différents traitements. Car dans cette application, plusieurs contraintes peuvent être posées pour éviter l’intoxication des patients pendant les traitements et les méthodes de la théorie des ensembles peuvent les prendre en compte facilement. Pour cette application, nous proposons une méthodologie pour déterminer les domaines d’attraction pour les modèles mathématiques choisis pour simuler la croissance tumorale. Dans la deuxième partie, nous proposons des méthodes de la théorie des ensemble pour la caractérisation des domaines d’attraction pour les systèmes non linéaires incertains. Au début, nous développons des conditions suffisantes pour l’invariance et la contraction d’un ellipsoïde pour des systèmes saturés. Ces conditions permettent de déterminer implicitement une fonction de Lyapunov quadratique locale. Nous montrerons que l’approche proposée est moins conservatrice que celles de la littérature, et donnerons un algorithme pour la caractérisation de l’ellipsoïde invariant et contractif. Pour les systèmes non linéaires incertains, nous développons une condition suffisante pour l’invariance contrôlable robuste pour le cas des incertitudes paramétriques. Une méthode basée sur cette condition est développée pour la caractérisation des domaines d’attraction des systèmes avec ces incertitudes. Ensuite, nous nous concentrons sur l’étude des systèmes non linéaires avec incertitudes additives, et nous donnons également une autre méthode pour la caractérisation de leurs domaines d’attraction. Ces méthodes sont des méthodes facilement traitables en utilisant les outils de l’optimisation convexe. Dans la troisième partie, nous développons des outils numériques pour la caractérisation des domaines d’attraction pour les modèles de la croissance tumorale en présence de traitements, en particulier la chimiothérapie et le traitement anti-angiogénique. Ces domaines contiennent tous les états des patients pour lesquels ils existent des protocoles de traitement efficaces. Dans ce cadre, nous considérons que les modèles sont incertains car les paramètres exactes qui les définissent sont en pratique inconnus. Ces outils sont basés sur les méthodes rappelées et développées dans cette thèse. Plusieurs informations utiles pour une thérapie tumorale efficace peuvent être extraites de ces domaines. / This thesis aims at using the mathematical modeling with advanced control tools to guide therapies for the contraction of the tumor. The aims of this thesis are the contribution to the development of the set-theoretic methods for robust control of nonlinear systems and the development of analytical tools for the analysis and control of tumor growth in presence of chemotherapy and/oranti-angiogenic therapy. Generically, in the context of control theory, techniques that are theoretically based on some properties of subsets of the system state space could be referred as set-theoretic methods.In the first part, we review the definitions, concepts and tools of the existing set-theoretic methods in the literature to respond effectively to the control issues of linear and nonlinear systems with hard constraints and uncertainties. In this context, we are interested in two properties of sets that are invariance and contractiveness. The problems associated with the stability of the systems may be formulated in terms of calculation of their domain of attraction. For development purposes, we recall methods from the literature for characterizing these domains of attraction for linear and nonlinear systems. An important application of these methods is the control of tumor growth in the presence of different treatments. For this application, several constraints can be imposed in order to avoid the patient intoxications during the treatments and the set-theoretic methods can consider easily these constraints. For this latter application, we propose a methodology to estimate the domains of attraction for the mathematical models chosen to simulate the tumor growth.In the second part, we propose set-theoretic methods for the characterization of the domains ofattraction for linear and nonlinear uncertain systems. At the beginning, we develop sufficient conditions for the invariance and contractiveness of an ellipsoid for saturated systems. These conditions allow implicitly determining a local Lyapunov function. We will show that the proposed approach is less conservative than those in the literature, and we give an algorithm for characterizing the invariant ellipsoids. For uncertain nonlinear systems, we develop a sufficient condition for the robust controlled invariance in the case of parametric uncertainties. A method based on this condition is developed for characterizing the domains of attraction for nonlinear systems with these uncertainties. Then we focus on the study of nonlinear systems with additive uncertainties, and we also give a method for the characterization of their domains of attraction. These methods are easily treatable using convex optimization tools.In the third part, we develop numerical tools for characterizing the domains of attraction for themodels of tumor growth in the presence of treatments, particularly chemotherapy and anti-angiogenictreatment. These domains contain all the states of the patients for whom effective treatment protocols exist. In this context, we consider that the models are uncertain and in particular the parameters that are unknown in practice. These tools are based on the methods developed in this thesis. Several useful informations for effective tumor therapy can be extracted from these domains.

Face à l'augmentation significative du taux de mortalité par cancer du sein chez les femmes ainsi que la croissance continue du nombre de mammographies réalisées chaque année, le diagnostic assisté par ordinateur devient de plus en plus impératif pour les experts. Dans notre travail de thèse, une attention particulière est accordée aux masses mammaires vu qu'elles représentent le signe de cancer du sein le plus couramment observé en mammographies. Néanmoins, ces images présentent un très faible contraste, ce qui fait que les frontières entre les tissus sains et les masses sont mal définies. C'est ainsi qu'il est difficile de pouvoir discerner avec précision ces masses et de leur définir un contour unique. En outre, la complexité et la grande variabilité des formes des masses mammaires rendent les tâches de diagnostic et de classification difficiles. Dans ce cadre, nous proposons un système d'aide au diagnostic dont le but est la segmentation de masses dans les régions d'intérêt et par la suite la classification de ces masses en deux catégories : bénignes et malignes. La première étape de segmentation est une étape assez délicate vu que les étapes postérieures à savoir la caractérisation et la classification y sont dépendantes. En effet, une mauvaise segmentation peut entrainer une mauvaise prise de décision. Un tel cas peut survenir en raison de l'incertitude et l'imprécision émanant de l'image mammographique. C'est pour cette raison que nous proposons une définition de contours flous permettant de prendre en compte ces types d'imperfections. Ces contours flous sont introduits dans l'énergie d'un contour actif pour modifier son mouvement et aboutir à une délimitation exacte des masses. Une fois les régions d'intérêt sont segmentées, nous présentons une méthode de classification de masses basée sur la théorie des possibilités qui permet de modéliser les ambigüités inhérentes aux connaissances exprimées par l'expert. En outre, cette méthode utilise essentiellement les descripteurs de forme pour caractériser les masses et décider de leur degré de gravité vu que la forme des masses constitue un bon indicateur de gravité.La validation et l'évaluation de ces deux méthodes sont réalisées en utilisant les régions d'intérêt contenant des masses extraites de la base MIAS. Les résultats obtenus sont très intéressants et les comparaisons effectuées ont mis en évidence leurs performances. / In view of the significant increase in breast cancer mortality rate among women as well as the continuous growth in number of mammograms performed each year, computer-aided diagnosis is becoming more and more imperative for experts. In our thesis work, special attention is given to breast masses as they represent the most common sign of breast cancer in mammograms. Nevertheless, mammographic images have very low contrast and breast masses possess ambiguous margins. Thus, it is difficult to distinguish them from the surrounding parenchymal. Moreover, the complexity and the large variability of breast mass shapes make diagnostic and classification challenging tasks.In this context, we propose a computer-aided diagnosis system which firstly segments masses in regions of interests and then classifies them as benign or malignant. Mass segmentation is a critical step in a computer-aided diagnosis system since it affects the performance of subsequent analysis steps namely feature analysis and classification. Indeed, poor segmentation may lead to poor decision making. Such a case may occur due to two types of imperfection: uncertainty and imprecision. Therefore, we propose to deal with these imperfections using fuzzy contours which are integrated in the energy of an active contour to get a fuzzy-energy based active contour model that is used for final delineation of mass.After mass segmentation, a classification method is proposed. This method is based on possibility theory which allows modeling the ambiguities inherent to the knowledge expressed by the expert. Moreover, since shape and margin characteristics are very important for differentiating between benign and malignant masses, the proposed method is essentially based on shape descriptors.The evaluation of the proposed methods was carried out using the regions of interest containing masses extracted from the MIAS base. The obtained results are very interesting and the comparisons made have demonstrated their performances.