This thesis deals with general polygon boolean operation algorithms. Boolean operations are e.g. intersection, union or difference. A general polygon can be e.g. a selfinterecting polygon with inner hole. Clipping of polygons against a rectangular window is probably the most familiar boolean operation on polygons. At first, basic definitions are listed. Then the principles of a selected set of boolean operation algorithms are reviewed. Finally, a complex comparison of the algorithms is undertaken. Performance as well as the ability to handle degenerate cases are tested. The output of this thesis is an overall evaluation of algorithm properties and a dynamic library that contains the implementation of all of the tested algorithms.

Whitebox cryptography aims at protecting standard cryptographic algorithmsthat execute in attacker-controlled environments. In these, the attacker is ableto read a secret key directly from memory. Common implementations mask alldata at runtime and operate on masked data by using many small precomputedtables. Practical whiteboxes involve trade-offs between security and executionspeed, to limit their footprints and enable applications such as real-time videostreaming.To improve this compromise, we study the use of bitslicing (or bitparallelism)to implement whiteboxes. Bitslicing is commonly used to writefast constant-time implementations of cryptographic algorithms and relies onthe synthesis of boolean circuits implementing the corresponding algorithms.The synthesis of optimal circuits for lookup tables is resource intensive andgenerally only performed once. In a whitebox context however, many randomlookup tables are generated at compile-time. We therefore require the booleancircuit generation to be time efficient.In this master thesis, we review the existing circuit-synthesis algorithms,and analyse their usability in the whitebox context. In particular, we studythe technique of Binary Decision Diagrams to generate efficient circuits ina cheap and adaptable manner. We implemented a flexible version of thisalgorithm as a C++ library. Eventually, we go through different techniques toevaluate the generated circuits and analyse the performances of our algorithm,and recommand the best parameters for the whitebox context. / Vit-låda kryptografi syftar till att skydda kryptografiska standardalgoritmersom körs i miljöer som kontrolleras av angripare, där angriparen kan läsa enhemlig nyckel direkt från minnet. Vanliga tillämpningar maskerar alla data vidkörning och bearbetar maskerade data med hjälp av många små förberäknadetabeller. Praktiska vit-låda innebär att man måste göra avvägningar mellansäkerhet och exekveringshastighet, för att begränsa deras fotavtryck och möjliggöratillämpningar som till exempel videoströmning i realtid.För att förbättra denna kompromiss studerar vi användningen av bitslicing(eller bit-parallelism) för att genomföra vit-låda. Bitslicing används vanligenför att skriva snabba konstanttidsimplementationer av kryptografiska algoritmeroch kräver syntes av boolska kretsar som implementerar motsvarande funktioner.Syntesen av optimala kretsar för uppslagstabeller är resurskrävande och utförsi allmänhet bara en gång. I ett vit-låda-sammanhang genereras dock mångaslumpmässiga uppslagstabeller vid kompilering, och därför kräver vi attgenereringen av boolska kretsar är tidseffektiv.I denna masteruppsats går vi igenom de befintliga algoritmerna för kretssyntesoch analyserar deras användbarhet i vit-låda-sammanhang. Vi studerar särskilttekniken med binära beslutsdiagram för att generera effektiva kretsar på ettbilligt och anpassningsbart sätt. Vi har implementerat en flexibel version avdenna algoritm som ett C++-bibliotek. Slutligen går vi igenom olika teknikerför att utvärdera de genererade kretsarna och analysera vår algoritms prestandaoch rekommenderar de bästa parametrarna för whitebox-kontexten. / La cryptographie en boîte blanche est connue comme protection pour desalgorithmes cryptographiques s’exécutant dans des environnements contrôléspar l’attaquant. L’approche classique consiste à remplacer les opérations pardes accès à des tables précalculées, ce qui a un coût en performance. Il estdifficile d’obtenir un bon compromis entre sécurité et vitesse d’exécution pourdes applications lourdes telles que la diffusion de contenus vidéos en tempsréel.Le parallélisme au bit ou bitslicing est utilisé en cryptographie traditionnellepour accélérer les implémentations, mais aussi en boîte blanche. Cettetechnique d’implémentation demande la synthèse d’un circuit booléen pourchaque table, recherche qui peut être très coûteuse en temps. En pratique, ilest commun de regénérer régulièrement toutes les tables utilisées dans uneboîte blanche pour renouveler sa défense, ce qui complique l’application dubit-parallélisme.Nous présentons dans cette thèse de master notre effort pour une synthèseefficace de circuits booléens à l’usage de la compilation de boîtes blanchesparallèles au bit. Nous publierons avec cet article une bibliothèque C++ etun module de compilation LLVM pour l’écriture d’implémentation bitslicée,avec un objectif de performance et de lisibilité.

The growing interest in the Internet of Things (IoT) has led to predictions claiming that by 2020 we can expect to be surrounded by 50 billion Internet connected devices. With more entry points to a network, adversaries can potentially use IoT devices as a stepping stone for attacking other devices connected to the network or the network itself. Information security relies on cryptographic primitives that, in turn, depend on secret keys. Furthermore, the issue of Intellectual property (IP) theft in the field of Integrated circuit (IC) design can be tackled with the help of unique device identifiers. Physical unclonable functions (PUFs) provide a tamper-resilient solution for secure key storage and fingerprinting hardware. PUFs use intrinsic manufacturing differences of ICs to assign unique identities to hardware. Arbiter PUFs utilise the differences in delays of identically designed paths, giving rise to an unpredictable response unique to a given IC. This thesis explores the statistical properties of Boolean functions induced by arbiter PUFs. In particular, this empirical study looks into the distribution of induced functions. The data gathered shows that only 3% of all possible 4-variable functions can be induced by a single 4 stage arbiter PUF. Furthermore, some individual functions are more than 5 times more likely than others. Hence, the distribution is non-uniform. We also evaluate alternate PUF designs, improving the coverage vastly, resulting in one particular implementation inducing all 65,536 4-variable functions. We hypothesise the need for n XORed PUFs to induce all 22n possible n-variable Boolean functions.

La Tesis investiga técnicas ágiles dentro del paradigma declarativo para dar solución a dos problemas: el análisis de programas y la inferencia de especificaciones a partir de programas escritos en lenguajes multiparadigma y en lenguajes imperativos con tipos, objetos, estructuras y punteros. Respecto al estado actual de la tesis, la parte de análisis de programas ya está consolidada, mientras que la parte de inferencia de especificaciones sigue en fase de desarrollo activo. La primera parte da soluciones para la ejecución de análisis de punteros especificados en Datalog. En esta parte se han desarrollado dos técnicas de ejecución de especificaciones en dicho lenguaje Datalog: una de ellas utiliza resolutores de sistemas de ecuaciones booleanas, y la otra utiliza la lógica de reescritura implementada eficientemente en el lenguaje Maude. La segunda parte desarrolla técnicas de inferencia de especificaciones a partir de programas. En esta parte se han desarrollado dos métodos de inferencia de especificaciones. El primer método se desarrolló para el lenguaje lógico-funcional Curry y permite inferir especificaciones ecuacionales mediante interpretación abstracta de los programas. El segundo método está siendo desarrollado para lenguajes imperativos realistas, y se ha aplicado a un subconjunto del lenguaje de programación C. Este método permite inferir especificaciones en forma de reglas que representan las distintas relaciones entre las propiedades que el estado de un programa satisface antes y después de su ejecución. Además, estas propiedades son expresables en términos de las abstracciones funcionales del propio programa, resultando en una especificación de muy alto nivel y, por lo tanto, de más fácil comprensión. / Feliú Gabaldón, MA. (2013). Logic-based techniques for program analysis and specification synthesis [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/33747

The area of systems biology evolved in an attempt to introduce mathematical systems theory principles in biology. Although we believe that all biological processes are essentially chemical reactions, describing those using precise mathematical rules is not easy, primarily due to the complexity and enormity of biological systems. Here we introduce a formal approach for modeling biological dynamical relationships and diseases such as cancer. The immediate motivation behind this research is the urgency to find a practicable cure of cancer, the emperor of all maladies. Unlike other deadly endemic diseases such as plague, dengue and AIDS, cancer is characteristically heterogenic and hence requires a closer look into the genesis of the disease. The actual cause of cancer lies within our physiology. The process of cell division holds the clue to unravel the mysteries surrounding this disease. In normal scenario, all control mechanisms work in tandem and cell divides only when the division is required, for instance, to heal a wound platelet derived growth factor triggers cell division. The control mechanism is tightly regulated by several biochemical interactions commonly known as signal transduction pathways. However, from mathematical point of view, these pathways are marginal in nature and unable to cope with the multi-variability of a heterogenic disease like cancer. The present research is possibly one first attempt towards unraveling the mysteries surrounding the dynamics of a proliferating cell. A novel yet simple methodology is developed to bring all the marginal knowledge of the signaling pathways together to form the simplest mathematical abstract known as the Boolean Network. The malfunctioning in the cell by genetic mutations is formally modeled as stuck-at faults in the underlying Network. Finally a mathematical methodology is discovered to optimally find out the possible best combination drug therapy which can drive the cell from an undesirable condition of proliferation to a desirable condition of quiescence or apoptosis. Although, the complete biological validation was beyond the scope of the current research, the process of in-vitro validation has been already initiated by our collaborators. Once validated, this research will lead to a bright future in the field on personalized cancer therapy.

Das Ziel dieser Arbeit ist es die mathematische Theorie der Begriffsalgebren zu entwickeln. Wir betrachten dabei hauptsaechlich das Repraesentationsproblem dieser vor Kurzem eingefuehrten Strukturen. Motiviert durch die Suche nach einer geeigneten Negation sind die Begriffsalgebren entstanden. Sie sind nicht nur fuer die Philosophie oder die Wissensrepraesentation von Interesse, sondern auch fuer andere Felder, wie zum Beispiel Logik oder Linguistik. Das Problem Negationen geeignet einzufuehren, ist sicher eines der aeltesten der wissenschaftlichen oder philosophischen Gemeinschaft und erregt auch zur Zeit die Aufmerksamkeit vieler Wissenschaftler. Verschiedene Typen von Logik (die sich sehr stark durch die eigefuehrte Negation unterscheiden) unterstreichen die Wichtigkeit dieser Untersuchungen. In dieser Arbeit beschaeftigen wir uns hauptsaechlich mit der kontextuellen Logik, eine Herangehensweise der Formalen Begriffsanalyse, basierend auf der Idee, den Begriff als Einheit des Denkens aufzufassen. / The aim of this investigation is to develop a mathematical theory of concept algebras. We mainly consider the representation problem for this recently introduced class of structures. Motivated by the search of a "negation" on formal concepts, "concept algebras" are of considerable interest not only in Philosophy or Knowledge Representation, but also in other fields as Logic or Linguistics. The problem of negation is surely one of the oldest problems of the scientific and philosophic community, and still attracts the attention of many researchers. Various types of Logic (defined according to the behaviour of the corresponding negation) can attest this affirmation. In this thesis we focus on "Contextual Logic", a Formal Concept Analysis approach, based on concepts as units of thought.

Das Ziel dieser Arbeit ist es die mathematische Theorie der Begriffsalgebren zu entwickeln. Wir betrachten dabei hauptsaechlich das Repraesentationsproblem dieser vor Kurzem eingefuehrten Strukturen. Motiviert durch die Suche nach einer geeigneten Negation sind die Begriffsalgebren entstanden. Sie sind nicht nur fuer die Philosophie oder die Wissensrepraesentation von Interesse, sondern auch fuer andere Felder, wie zum Beispiel Logik oder Linguistik. Das Problem Negationen geeignet einzufuehren, ist sicher eines der aeltesten der wissenschaftlichen oder philosophischen Gemeinschaft und erregt auch zur Zeit die Aufmerksamkeit vieler Wissenschaftler. Verschiedene Typen von Logik (die sich sehr stark durch die eigefuehrte Negation unterscheiden) unterstreichen die Wichtigkeit dieser Untersuchungen. In dieser Arbeit beschaeftigen wir uns hauptsaechlich mit der kontextuellen Logik, eine Herangehensweise der Formalen Begriffsanalyse, basierend auf der Idee, den Begriff als Einheit des Denkens aufzufassen. / The aim of this investigation is to develop a mathematical theory of concept algebras. We mainly consider the representation problem for this recently introduced class of structures. Motivated by the search of a "negation" on formal concepts, "concept algebras" are of considerable interest not only in Philosophy or Knowledge Representation, but also in other fields as Logic or Linguistics. The problem of negation is surely one of the oldest problems of the scientific and philosophic community, and still attracts the attention of many researchers. Various types of Logic (defined according to the behaviour of the corresponding negation) can attest this affirmation. In this thesis we focus on "Contextual Logic", a Formal Concept Analysis approach, based on concepts as units of thought.

Le réalisme des images en infographie exige de créer des objets (ou des scènes) de plus en plus complexes, ce qui entraîne des coûts considérables. La modélisation procédurale peut aider à automatiser le processus de création, à simplifier le processus de modification ou à générer de multiples variantes d'une instance d'objet. Cependant même si plusieurs méthodes procédurales existent, aucune méthode unique permet de créer tous les types d'objets complexes, dont en particulier un édifice complet. Les travaux réalisés dans le cadre de cette thèse proposent deux solutions au problème de la modélisation procédurale: une solution au niveau de la géométrie de base, et l’autre sous forme d'un système général adapté à la modélisation des objets complexes. Premièrement, nous présentons le bloc, une nouvelle primitive de modélisation simple et générale, basée sur une forme cubique généralisée. Les blocs sont disposés et connectés entre eux pour constituer la forme de base des objets, à partir de laquelle est extrait un maillage de contrôle pouvant produire des arêtes lisses et vives. La nature volumétrique des blocs permet une spécification simple de la topologie, ainsi que le support des opérations de CSG entre les blocs. La paramétrisation de la surface, héritée des faces des blocs, fournit un soutien pour les textures et les fonctions de déplacements afin d'appliquer des détails de surface. Une variété d'exemples illustrent la généralité des blocs dans des contextes de modélisation à la fois interactive et procédurale. Deuxièmement, nous présentons un nouveau système de modélisation procédurale qui unifie diverses techniques dans un cadre commun. Notre système repose sur le concept de composants pour définir spatialement et sémantiquement divers éléments. À travers une série de déclarations successives exécutées sur un sous-ensemble de composants obtenus à l'aide de requêtes, nous créons un arbre de composants définissant ultimement un objet dont la géométrie est générée à l'aide des blocs. Nous avons appliqué notre concept de modélisation par composants à la génération d'édifices complets, avec intérieurs et extérieurs cohérents. Ce nouveau système s'avère général et bien adapté pour le partionnement des espaces, l'insertion d'ouvertures (portes et fenêtres), l'intégration d'escaliers, la décoration de façades et de murs, l'agencement de meubles, et diverses autres opérations nécessaires lors de la construction d'un édifice complet. / The realism of computer graphics images requires the creation of objects (or scenes) of increasing complexity, which leads to considerable costs. Procedural modeling can help to automate the creation process, to simplify the modification process or to generate multiple variations of an object instance. However although several procedural methods exist, no single method allows the creation of all types of complex objects, including in particular a complete building. This thesis proposes two solutions to the problem of procedural modeling: one solution addressing the geometry level, and the other introducing a general system suitable for complex object modeling. First, we present a simple and general modeling primitive, called a block, based on a generalized cuboid shape. Blocks are laid out and connected together to constitute the base shape of complex objects, from which is extracted a control mesh that can contain both smooth and sharp edges. The volumetric nature of the blocks allows for easy topology specification, as well as CSG operations between blocks. The surface parameterization inherited from the block faces provides support for texturing and displacement functions to apply surface details. A variety of examples illustrate the generality of our blocks in both interactive and procedural modeling contexts. Second, we present a novel procedural modeling system which unifies some techniques into a common framework. Our system relies on the concept of components to spatially and semantically define various elements. Through a series of successive statements executed on a subset of queried components, we grow a tree of components ultimately defining an object whose geometry is made from blocks. We applied our concept and representation of components to the generation of complete buildings, with coherent interiors and exteriors. It proves general and well adapted to support partitioning of spaces, insertion of openings (doors and windows), embedding of staircases, decoration of façades and walls, layout of furniture, and various other operations required when constructing a complete building.

La recherche de règles d’association intéressantes est un domaine important et actif en fouille de données. Puisque les algorithmes utilisés en extraction de connaissances à partir de données (ECD), ont tendance à générer un nombre important de règles, il est difficile à l’utilisateur de sélectionner par lui même les connaissances réellement intéressantes. Pour répondre à ce problème, un post-filtrage automatique des règles s’avère essentiel pour réduire fortement leur nombre. D’où la proposition de nombreuses mesures d’intérêt dans la littérature, parmi lesquelles l’utilisateur est supposé choisir celle qui est la plus appropriée à ses objectifs. Comme l’intérêt dépend à la fois des préférences de l’utilisateur et des données, les mesures ont été répertoriées en deux catégories : les mesures subjectives (orientées utilisateur ) et les mesures objectives (orientées données). Nous nous focalisons sur l’étude des mesures objectives. Néanmoins, il existe une pléthore de mesures objectives dans la littérature, ce qui ne facilite pas le ou les choix de l’utilisateur. Ainsi, notre objectif est d’aider l’utilisateur, dans sa problématique de sélection de mesures objectives, par une approche par catégorisation. La thèse développe deux approches pour assister l’utilisateur dans sa problématique de choix de mesures objectives : (1) étude formelle suite à la définition d’un ensemble de propriétés de mesures qui conduisent à une bonne évaluation de celles-ci ; (2) étude expérimentale du comportement des différentes mesures d’intérêt à partir du point de vue d’analyse de données. Pour ce qui concerne la première approche, nous réalisons une étude théorique approfondie d’un grand nombre de mesures selon plusieurs propriétés formelles. Pour ce faire, nous proposons tout d’abord une formalisation de ces propriétés afin de lever toute ambiguïté sur celles-ci. Ensuite, nous étudions, pour différentes mesures d’intérêt objectives, la présence ou l’absence de propriétés caractéristiques appropriées. L’évaluation des mesures est alors un point de départ pour une catégorisation de celle-ci. Différentes méthodes de classification ont été appliquées : (i) méthodes sans recouvrement (CAH et k-moyennes) qui permettent l’obtention de groupes de mesures disjoints, (ii) méthode avec recouvrement (analyse factorielle booléenne) qui permet d’obtenir des groupes de mesures qui se chevauchent. Pour ce qui concerne la seconde approche, nous proposons une étude empirique du comportement d’une soixantaine de mesures sur des jeux de données de nature différente. Ainsi, nous proposons une méthodologie expérimentale, où nous cherchons à identifier les groupes de mesures qui possèdent, empiriquement, un comportement semblable. Nous effectuons par la suite une confrontation avec les deux résultats de classification, formel et empirique dans le but de valider et mettre en valeur notre première approche. Les deux approches sont complémentaires, dans l’optique d’aider l’utilisateur à effectuer le bon choix de la mesure d’intérêt adaptée à son application. / The search for interesting association rules is an important and active field in data mining. Since knowledge discovery from databases used algorithms (KDD) tend to generate a large number of rules, it is difficult for the user to select by himself the really interesting knowledge. To address this problem, an automatic post-filtering rules is essential to significantly reduce their number. Hence, many interestingness measures have been proposed in the literature in order to filter and/or sort discovered rules. As interestingness depends on both user preferences and data, interestingness measures were classified into two categories : subjective measures (user-driven) and objective measures (data-driven). We focus on the study of objective measures. Nevertheless, there are a plethora of objective measures in the literature, which increase the user’s difficulty for choosing the appropriate measure. Thus, our goal is to avoid such difficulty by proposing groups of similar measures by means of categorization approaches. The thesis presents two approaches to assist the user in his problematic of objective measures choice : (1) formal study as per the definition of a set of measures properties that lead to a good measure evaluation ; (2) experimental study of the behavior of various interestingness measures from data analysispoint of view. Regarding the first approach, we perform a thorough theoretical study of a large number of measures in several formal properties. To do this, we offer first of all a formalization of these properties in order to remove any ambiguity about them. We then study for various objective interestingness measures, the presence or absence of appropriate characteristic properties. Interestingness measures evaluation is therefore a starting point for measures categorization. Different clustering methods have been applied : (i) non overlapping methods (CAH and k-means) which allow to obtain disjoint groups of measures, (ii) overlapping method (Boolean factor analysis) that provides overlapping groups of measures. Regarding the second approach, we propose an empirical study of the behavior of about sixty measures on datasets with different nature. Thus, we propose an experimental methodology, from which we seek to identify groups of measures that have empirically similar behavior. We do next confrontation with the two classification results, formal and empirical in order to validate and enhance our first approach. Both approaches are complementary, in order to help the user making the right choice of the appropriate interestingness measure to his application.

Cette thèse porte sur l’utilisation d’une langue contrôlée pour les spécifications des besoins du logiciel en thaï. L’étudedécrit les ambiguïtés syntaxiques et sémantiques ainsi que les problèmes rencontrés dans les spécifications des besoins dulogiciel en thaï. Ce travail explique également la nature de la langue thaïe. Le modèle de la langue contrôlée pour lesspécifications des besoins du logiciel en thaï, proposé dans cette étude, comprend trois composantes: l’analyse lexicale,l’analyse syntaxique et l’analyse sémantique. Pour l’analyse syntaxique, une syntaxe contrôlée est conçue en utilisant laforme du Backus-Naur (BNF). Quant à l’analyse lexicale, nous créons une ressource lexicale sous forme de langage XMLpour stocker tous les mots classés selon leur domaine. Les mots reçus de la ressource XML sont corrects d’un point de vueconceptuel mais ne sont pas pertinents d’un point de vue sémantique. Pour résoudre ce problème, nous faisons alors usage dematrices booléennes pour aligner les phrases sémantiquement. Ainsi les phrases produites par le modèle serontsyntaxiquement et sémantiquement correctes.Après avoir créé le modèle, nous avons construit un logiciel pour tester son efficacité. Il est ainsi évalué par quatreméthodes d’évaluation : 1. le test de fonctionnement syntaxique pour vérifier la syntaxe de la phrase; 2. le test defonctionnement sémantique pour tester la sémantique de la phrase; 3. le test d’acceptation en terme de satisfaction desutilisateurs avec le logiciel; et 4. le test d’acceptation en terme d’acception des données de sortie.Des résultats positifs montrent que : 1. les phrases produites par le modèle proposé sont syntaxiquement correctes; 2. lesphrases produites par le modèle proposé sont sémantiquement correctes; 3. les utilisateurs sont satisfaits et acceptent lelogiciel; et 4. les utilisateurs acceptent et comprennent les phrases produites par ce modèle. / This thesis focuses on using controlled language for Thai software requirements specifications. The studydescribes the ambiguities and problems encountered in Thai software requirements specifications; both syntacticambiguity and semantic ambiguity. The study also describes the nature of the Thai language. The model of controlledlanguage for Thai software requirements specifications is composed of three main components: lexical analysis,syntactic analysis, and semantic analysis. For syntactic analysis, a controlled syntax is created using Backus-NaurForm (BNF). In the lexical analysis stage, an XML format lexical resource is built to store words according to theirdomain. The words received from the XML resource are conceptually correct but may be semantically irrelevant. Tosolve this issue, the model applies Boolean Matrices to align sentences semantically. As a result, the sentencesproduced from the model are guaranteed to be syntactically and semantically correct.After having created this model, a program for testing the efficiency of the model is developed. The model isevaluated using four testing methods as follows: 1. functional testing for the correctness of the sentence’s syntax, 2.functional testing for the semantic correctness of the sentences produced by the model, 3. acceptance testing in termsof user satisfaction with the program, and 4. acceptance testing in terms of the validity of the outputs.The positive results signify that: 1. the sentences produced by the proposed model are syntactically correct, 2. thesentences produced by the proposed model are semantically correct, 3. the users are satisfied and accept the softwarecreated, and 4. the users approve and understand the sentences produced from this model.