Cette thèse étudie la configuration télévisuelle de l’identité arabe moderne à travers un des programmes phares de la chaine satellitaire libanaise LBC-Sat : la Star Academy Middle East. Elle interroge, d’un côté, les motivations et les contraintes institutionnelles et commerciales qui orientent le processus de création de sens à la télévision et se penche, de l’autre, sur le produit fini qui porte en lui les traces des tensions et des confrontations qui ont accompagné sa conception. Elle cherche à décoder la représentation de l’arabité proposée par la chaine libanaise dans un contexte régional instable, marqué par des bouleversements profonds. Les télévisions satellitaires panarabes, reflets des nouvelles technologies qui ont inondé le marché régional à une vitesse déconcertante à partir des années 1990, ont, en effet, entrainé une contraction de l’espace et du temps oriental ainsi qu’une abolition symbolique des frontières. Elles ont permis aux citoyens arabes, urbains comme ruraux, locaux comme de la diaspora, de s’informer, en temps réel, sur l’actualité arabe et mondiale et d’interagir avec des individus proches et lointains. Elles ont, de ce fait, facilité l’émergence d’un réseau d’échange horizontal et d’un espace public transnational qui a fait renaitre de ses cendres, mais sous une forme distincte, le rêve d’unité arabe. À travers leur discours dirigé vers la « rue arabe » et orienté par des considérations plus économiques que politiques, elles ont, d’une part, fragilisé les régimes autocratiques en place, en les dépossédant de leur monopole historique sur les médias, et de l’autre regroupé, à l’échelle internationale, un ensemble d’individus partageant les mêmes convictions, les mêmes attentes ou les mêmes centres d’intérêt. En accélérant l’autonomisation des opinions publiques par rapport aux idéologies officielles, elles ont obligé les régimes arabes à se repositionner vis-à-vis de ces producteurs de sens à l’influence grandissante. Leurs discours, qu’il soit inspiré d’une rhétorique islamique ou libérale s’élabore dans une sphère publique chargée de sens et de références et s’expose à des critiques qui témoignent de l’imbrication du politique, du religieux et du culturel dans le secteur médiatique arabe. La LBC-Sat, chaine satellitaire généraliste libanaise, née de l’association entre des entrepreneurs libanais et saoudiens, a intégré cette arène symbolique en 1996. Fille de la LBCI, la télévision la plus populaire du pays des Cèdres — celle qui représente, aux yeux des téléspectateurs arabes, l’essence de la culture libanaise — elle a très tôt affiché sa volonté de séduire l’audience régionale à travers une narration qui se démarque de celle de ses concurrentes. Constituée d’un mélange d’émissions à l’esthétique occidentale, au contenu audacieux, et au ton libéré et souvent frivole, sa programmation prend ses distances vis-à-vis des conservatismes régionaux et dénote une volonté de configurer une représentation différenciée de l’identité arabe, proche d’une conception singulière de l’identité libanaise, porteuse, selon les termes des idéologues du Liban moderne, d’une mission civilisatrice auprès des pays arabes et d’un pouvoir de conciliation entre les deux cultures occidentale et orientale. Les émissions de la LBC-Sat témoignent de son rôle autoproclamé de trait d’union entre ces deux mondes et participent à populariser cette vision auprès du public arabe. Son plus grand succès transnational, l’adaptation orientale de la télé-réalité d’Endemol Star Academy, montre, en effet, qu’il est possible d’imposer cette image dans l’imaginaire collectif régional à travers la construction d’un discours sur la jeunesse orientale, caractérisé par son d’hybridité et sa position à mi-chemin entre le global et le local. / This thesis studies the representation of modern Arab identities through one of the most influential reality shows in the Arab World: Star Academy Middle East.It seeks to understand the strategic and ideological discourse over Arabism constructed by one of the leading Lebanese satellite channel in the MENA region: LBC-Sat.Through the study of both the professional and commercial context of emergence of this discourse, as well as a qualitative content analysis of the first four seasons of the show, it tries to understand its rationale as well as its impact in the Arab World.We believe that this narrative is unfolding in an arena of controversies where a multitude of positions regarding Arab identities are debated. Indeed, since the establishment of the first Arab satellite channels that led to a prosperous television industry, a pan Arab public sphere arose. TV shows became political fields in which opinions were exposed and theories regarding political and social issues were considered. The once monopolistic control over media contents of authoritarian regimes gave way to a more liberal environment, where citizens were given the chance to participate in the debates framing there lives. Today, Arab satellite channels act as a lightning rod for what is known as “New Arabism”, a sense of belonging to an imagined community that is no longer imposed by a higher power but developed by the base. With their liberal aesthetic and messages that oppose those of more conservative Arab televisions, Lebanese channels play a crucial role in redefining Arab identities. Their discourse, inspired by a cultural and ideological interpretation of Lebanon’s position in the Arab world, translates into a plea to rebuild bridges between the East and the West. As a symbolic object composed of hybrid forms and ideas, Star Academy Middle East echoes this position.

L'analyse statique de programme a pour but de prouver automatiquement qu'un programme vérifie certaines propriétés. L'interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l'ordre d'itération utilisés pendant le calcul d'invariants. Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l'analyse.Habituellement, l'interprétation abstraite consiste en un calcul de point fixe d'un opérateur obtenu après convergence d'une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d'améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement. L'interprétation abstraite peut égalementêtre rendue plus précise en distinguant tous les chemins d'exécution du programme, au prix d'une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d'utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d'itération de l'état de l'art pour obtenir des analyses plus précises.Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d'erreur. Notre technique a différents usages: elle permet de montrer qu'un état d'erreur est inatteignable, mais également d'inférer des préconditions aux boucles et aux fonctions.Nous appliquons nos méthodes d'analyse statique à l'estimation du temps d'exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d'exprimer ce problème via optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l'ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique. Enfin, nous présentons l'implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté. / Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. In this thesis, we propose several improvements on the abstract interpretation framework that enhance the overall precision of the analysis.Usually, abstract interpretation consists in computing an ascending sequence with widening, which converges towards a fixpoint which is a program invariant; then computing a descending sequence of correct solutions without widening. We describe and experiment with a method to improve a fixpoint after its computation, by starting again a new ascending/descending sequence with a smarter starting value. Abstract interpretation can also be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. Satisfiability modulo theories (SMT), whose efficiency has been considerably improved in the last decade, allows sparse representations of paths and sets of paths. We propose to combine this SMT representation of paths with various state-of-the-art iteration strategies to further improve the overall precision of the analysis.We propose a second coupling between abstract interpretation and SMT in a program verification framework called Modular Path Focusing, that computes function and loop summaries by abstract interpretation in a modular fashion, guided by error paths obtained with SMT. Our framework can be used for various purposes: it can prove the unreachability of certain error program states, but can also synthesize function/loop preconditions for which these error states are unreachable.We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis.We finally describe the design and the implementation of Pagai,a new static analyzer working over the LLVM compiler infrastructure,which computes numerical inductive invariants using the various techniques described in this thesis.Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages and benchmarks used in the community.

Society is based on communication, for which speech is the most prevalent medium. In day to day interactions we talk to each other, but it is not only the words spoken that matters, but the emotional delivery as well. Extracting emotion from speech has therefore become a topic of research in the area of speech tasks. This area as a whole has in recent years adopted a Self- Supervised Learning approach for learning speech representations from raw speech audio, without the need for any supplementary labelling. These speech representations can be leveraged for solving tasks limited by the availability of annotated data, be it for low-resource language, or a general lack of data for the task itself. This thesis aims to evaluate the performances of a set of pre-trained speech models by fine-tuning them in different multilingual environments, and evaluating their performance thereafter. The model presented in this paper is based on wav2vec 2.0 and manages to correctly classify 86.58% of samples over eight different languages and four emotional classes when trained on those same languages. Experiments were conducted to garner how well a model trained on seven languages would perform on the one left out, which showed that there is quite a large margin of similarity in how different cultures express vocal emotions, and further investigations showed that as little as just a few minutes of in-domain data is able to increase the performance substantially. This shows promising results even for niche languages, as the amount of available data may not be as large of a hurdle as one might think. With that said, increasing the amount of data from minutes to hours does still garner substantial improvements, albeit to a lesser degree. / Hela vårt samhälle är byggt på kommunikation mellan olika människor, varav tal är det vanligaste mediet. På en daglig basis interagerar vi genom att prata med varandra, men det är inte bara orden som förmedlar våra intentioner, utan även hur vi uttrycker dem. Till exempel kan samma mening ge helt olika intryck beroende på ifall den sägs med ett argt eller glatt tonfall. Talbaserad forskning är ett stort vetenskapligt område i vilket talbaserad känsloigenkänning vuxit fram. Detta stora tal-område har under de senaste åren sett en tendens att utnyttja en teknik kallad själv-övervakad inlärning för att utnyttja omärkt ljuddata för att lära sig generella språkrepresentationer, vilket kan liknas vid att lära sig strukturen av tal. Dessa representationer, eller förtränade modeller, kan sedan utnyttjas som en bas för att lösa problem med begränsad tillgång till märkt data, vilket kan vara fallet för sällsynta språk eller unika uppgifter. Målet med denna rapport är att utvärdera olika applikationer av denna representations inlärning i en flerspråkig miljö genom att finjustera förtränade modeller för känsloigenkänning. I detta syfte presenterar vi en modell baserad på wav2vec 2.0 som lyckas klassifiera 86.58% av ljudklipp tagna från åtta olika språk över fyra olika känslo-klasser, efter att modellen tränats på dessa språk. För att avgöra hur bra en modell kan klassifiera data från ett språk den inte tränats på skapades modeller tränade på sju språk, och evaluerades sedan på det språk som var kvar. Dessa experiment visar att sättet vi uttrycker känslor mellan olika kulturer är tillräckligt lika för att modellen ska prestera acceptabelt även i det fall då modellen inte sett språket under träningsfasen. Den sista undersökningen utforskar hur olika mängd data från ett språk påverkar prestandan på det språket, och visar att så lite som endast ett par minuter data kan förbättra resultet nämnvärt, vilket är lovande för att utvidga modellen för fler språk i framtiden. Med det sagt är ytterligare data att föredra, då detta medför fortsatta förbättringar, om än i en lägre grad.

Induced seismicity (earthquakes caused by injection or extraction of fluids in Earth's subsurface) is a major, new hazard in the United States, the Netherlands, and other countries, with vast economic consequences if not properly managed. Addressing this problem requires development of predictive simulations of how fluid-saturated solids containing frictional faults respond to fluid injection/extraction. Here we present a numerical method for linear poroelasticity with rate-and-state friction faults. A numerical method for approximating the fully coupled linear poroelastic equations is derived using the summation-by-parts-simultaneous-approximation-term (SBP-SAT) framework. Well-posedness is shown for a set of physical boundary conditions in 1D and in 2D. The SBP-SAT technique is used to discretize the governing equations and show semi-discrete stability and the correctness of the implementation is verified by rigorous convergence tests using the method of manufactured solutions, which shows that the expected convergence rates are obtained for a problem with spatially variable material parameters. Mandel's problem and a line source problem are studied, where simulation results and convergence studies show satisfactory numerical properties. Furthermore, two problem setups involving fault dynamics and slip on faults triggered by fluid injection are studied, where the simulation results show that fluid injection can trigger earthquakes, having implications for induced seismicity. In addition, the results show that the scheme used for solving the fully coupled problem, captures dynamics that would not be seen in an uncoupled model. Future improvements involve imposing Dirichlet boundary conditions using a different technique, extending the scheme to handle curvilinear coordinates and three spatial dimensions, as well as improving the high-performance code and extending the study of the fault dynamics.

Backtracking CSP solvers provide a powerful framework for search and reasoning. The aim of constraint learning is increase global reasoning power by learning new constraints to boost reasoning and hopefully reduce search effort. In this thesis constraint learning is developed in several ways to make it faster and more powerful. First, lazy explanation generation is introduced, where explanations are generated as needed rather than continuously during propagation. This technique is shown to be effective is reducing the number of explanations generated substantially and consequently reducing the amount of time taken to complete a search, over a wide selection of benchmarks. Second, a series of experiments are undertaken investigating constraint forgetting, where constraints are discarded to avoid time and space costs associated with learning new constraints becoming too large. A major empirical investigation into the overheads introduced by unbounded constraint learning in CSP is conducted. This is the first such study in either CSP or SAT. Two significant results are obtained. The first is that typically a small percentage of learnt constraints do most propagation. While this is conventional wisdom, it has not previously been the subject of empirical study. The second is that even constraints that do no effective propagation can incur significant time overheads. Finally, the use of forgetting techniques from the literature is shown to significantly improve the performance of modern learning CSP solvers, contradicting some previous research. Finally, learning is generalised to use disjunctions of arbitrary constraints, where before only disjunctions of assignments and disassignments have been used in practice (g-nogood learning). The details of the implementation undertaken show that major gains in expressivity are available, and this is confirmed by a proof that it can save an exponential amount of search in practice compared with g-nogood learning. Experiments demonstrate the promise of the technique.

Writing declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and test coverage as well as coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to partial evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM). / text

Esta pesquisa tem por finalidade propor um modelo de automação e padronização do processo de controle da prescrição médica e dispensação de medicamentos no Brasil, baseado no Sistema Autenticador e Transmissor (SAT) aplicado ao controle fiscal do comércio varejista e implementado no Estado de São Paulo, Brasil. Busca-se analisar o cenário atual de prescrição médica no país, suas características operacionais, os problemas cada vez mais frequentes ligados ao comércio irregular de medicamentos e o uso abusivo de substâncias controladas. São apresentadas as medidas adotadas para o controle do setor no Brasil, em Portugal e nos Estados Unidos da América, bem como seus requisitos e grau de operacionalização. Com base na lacuna encontrada nas ações adotadas pelo Brasil, apresenta-se a motivação do presente trabalho, a busca pelas características do cenário brasileiro e a respectiva não aderência do mesmo às propostas internacionais, principalmente pelo fato dessas demandarem infraestrutura técnica, ordenamento jurídico e disponibilidade de investimentos incompatíveis. Diante de referida necessidade, buscou-se em outras áreas um modelo de controle de processos que fosse aderente à realidade brasileira apresentada, razão pela qual uma solução encontrada foi a utilizada para o controle do comércio varejista, por meio do equipamento SAT (Sistema Autenticador Transmissor), que é responsável pela geração de Cupons Fiscais Eletrônicos. Assim, o trabalho consiste em utilizar os conceitos traçados para o modelo fiscal e adaptar às necessidades da prescrição médica, propondo um novo modelo de automação e controle do processo de prescrição e dispensa de medicamentos baseado na Receita Médica Eletrônica (RM-e). / This research aims to propose a model of automation and standardization of the process of control of medical prescription and dispensing of medicines in Brazil, based on the Authentication and Transmission System (Sistema Autenticador Transmissor - SAT) applied to the fiscal control of the retail trade and implemented in the State of São Paulo, Brazil. The aim is to analyze the current scenario of medical prescription in the country, its operational characteristics, the increasingly frequent problems related to irregular drug trade and the abusive use of controlled substances. The measures adopted to control the sector in Brazil, Portugal and the United States of America, as well as their requirements and degrees of operation are presented. Based on the gap found in the actions adopted by Brazil, the motivation of the present study is the search for the characteristics of the Brazilian scenario and its non-adherence to the international proposals, mainly because they require technical infrastructure, legal order and availability Incompatible investments. In view of this need, a process control model was searched in other areas that adhered to the Brazilian reality presented, which is why a solution found was used to control the retail trade, through the SAT (Authentication and Transmission System), which is responsible for the generation of Electronic Tax Coupons. Thus, the work consists of using the concepts outlined for the fiscal model and adapting to the needs of the medical prescription, proposing a new model of automation and control of the prescription and dispensing process based on Electronic Medical Prescription (Receita Médica Eletrônica RM-e).

Submitted by PPG Hist?ria (historia-pg@pucrs.br) on 2017-11-14T17:30:59Z No. of bitstreams: 1 R?mulo Brito - Tese Vers?o Digital.pdf: 15722516 bytes, checksum: 98b1d77bae5d01d07f96acea5ba3771c (MD5) / Approved for entry into archive by Caroline Xavier (caroline.xavier@pucrs.br) on 2017-11-21T12:59:28Z (GMT) No. of bitstreams: 1 R?mulo Brito - Tese Vers?o Digital.pdf: 15722516 bytes, checksum: 98b1d77bae5d01d07f96acea5ba3771c (MD5) / Made available in DSpace on 2017-11-21T13:05:21Z (GMT). No. of bitstreams: 1 R?mulo Brito - Tese Vers?o Digital.pdf: 15722516 bytes, checksum: 98b1d77bae5d01d07f96acea5ba3771c (MD5) Previous issue date: 2017-08-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / In this thesis, an analysis of the caricature work of Rafael Bordalo Pinheiro (1846-1905) is made, in order to understand how this Portuguese intellectual showed several aspects related to Brazilian society in his satirical publications. Known as the greatest Portuguese caricaturist of the nineteenth century, Bordalo also worked professionally in Brazil between 1875 and 1879, but his compositions about the country precede this stay and extend for several years after his return to Portugal. Understanding how Brazil was presented throughout all these years, the elements that influenced the author's view of the country and the possible functions that such compositions have in their work are the main objectives of this work. The study is based on the hypothesis that Brazil constitutes a transnational axis of reflection in the work of the author, being used as an instrument to think the Portuguese society and, on the other hand, having its interpretation influenced by the conceptions of the caricaturist about Portugal, in a constant process of interlocution between the two shores of the Atlantic. In order to carry out such research, we will analyze compositions produced before, during and after the stay, present in the periodicals and albums of caricatures produced by Bordalo in both Portugal and Brazil. / Nesta tese, realiza-se uma an?lise sobre a obra caricatural de Rafael Bordalo Pinheiro (1846-1905), a fim de compreender como este intelectual portugu?s mostrou v?rios aspectos relativos ? sociedade brasileira em suas publica??es sat?ricas. Conhecido como o maior caricaturista portugu?s do s?culo XIX, Bordalo tamb?m atuou profissionalmente no Brasil entre 1875 e 1879, mas suas composi??es sobre o pa?s precedem esta estadia e se estendem para v?rios anos ap?s seu retorno a Portugal. Compreender a maneira como o Brasil fora apresentado ao longo de todos estes anos, os elementos que influenciavam a vis?o do autor sobre o pa?s e as poss?veis fun??es que tais composi??es possuem em sua obra ? o principal objetivo deste trabalho. O estudo parte da hip?tese de que o Brasil se constitui enquanto um eixo transnacional de reflex?o na obra do autor, sendo utilizado como instrumento para pensar a sociedade portuguesa e, por outro lado, tendo sua interpreta??o influenciada pelas concep??es do caricaturista sobre Portugal, em um constante processo de interlocu??o entre as duas margens do Atl?ntico. A fim de realizar tal investiga??o, ser?o analisadas composi??es produzidas antes, durante e ap?s a estadia, presentes nos peri?dicos e ?lbuns de caricaturas produzidos por Bordalo tanto em Portugal quanto no Brasil.

Submitted by Maria Cristina (library@lncc.br) on 2017-08-10T18:19:02Z No. of bitstreams: 1 dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5) / Approved for entry into archive by Maria Cristina (library@lncc.br) on 2017-08-10T18:19:15Z (GMT) No. of bitstreams: 1 dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5) / Made available in DSpace on 2017-08-10T18:19:25Z (GMT). No. of bitstreams: 1 dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5) Previous issue date: 2017-02-17 / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / Nowadays, besides the growing popularity of cryptography, there is a big interest from researchers in the development of strategies that study and analyze the current crypto- graphic methods. This is due to the fact that current methods are based on mathematical problems considered safe, however, researchs points to security flaws in the presence of a quantum computer. In this work we created and developed a method capable of translating symmetric cryp- tographic algorithms into Conjunctive Normal Form and then we analyze the obtained output. Initially, we studied the cryptographic algorithm model of interest and used the software CBMC, a bounded model checker software. This software returns a SAT system to be solved, i.e, we rewrite the problem as SAT. In addition, the system can be interpreted as a graph, so we reduce it by implementing a depth-first-search before solving it, to make the problem feasible for resolution. The method proposed is then submitted to a round of tests, aiming to validate the developed tool. / Atualmente, além da popularidade da criptografia estar crescendo consideravelmente, existe grande interesse em realizar pesquisas para o desenvolvimento de estratégias que estudem e analisem os métodos criptográficos utilizados atualmente. Isto se dá pelo fato dos métodos atuais serem baseados em problemas matemáticos considerados seguros, entretanto, pesquisas atuais apontam para falhas de segurança na presença de um computador quântico. Este trabalho consiste em traduzir os algoritmos criptográficos simétricos para o sistema SAT e analisar a saída obtida. Para isto, inicialmente estudamos o modelo do algoritmo criptográfico de interesse e inserimos ele em um software verificador de modelos (CBMC). Este software nos retorna um sistema SAT a ser resolvido, ou seja, reescrevemos o problema como SAT. Além disto, o sistema pode ser interpretado como um grafo, então reduzimos o mesmo através de uma busca em profundidade antes de resolvê-lo, para tornar o problema factível de resolução. A técnica proposta é submetida a um conjunto de testes, utilizando meios propostos pela literatura e alguns meios originais do trabalho, para validar a ferramenta desenvolvida.

Esta pesquisa tem por finalidade propor um modelo de automação e padronização do processo de controle da prescrição médica e dispensação de medicamentos no Brasil, baseado no Sistema Autenticador e Transmissor (SAT) aplicado ao controle fiscal do comércio varejista e implementado no Estado de São Paulo, Brasil. Busca-se analisar o cenário atual de prescrição médica no país, suas características operacionais, os problemas cada vez mais frequentes ligados ao comércio irregular de medicamentos e o uso abusivo de substâncias controladas. São apresentadas as medidas adotadas para o controle do setor no Brasil, em Portugal e nos Estados Unidos da América, bem como seus requisitos e grau de operacionalização. Com base na lacuna encontrada nas ações adotadas pelo Brasil, apresenta-se a motivação do presente trabalho, a busca pelas características do cenário brasileiro e a respectiva não aderência do mesmo às propostas internacionais, principalmente pelo fato dessas demandarem infraestrutura técnica, ordenamento jurídico e disponibilidade de investimentos incompatíveis. Diante de referida necessidade, buscou-se em outras áreas um modelo de controle de processos que fosse aderente à realidade brasileira apresentada, razão pela qual uma solução encontrada foi a utilizada para o controle do comércio varejista, por meio do equipamento SAT (Sistema Autenticador Transmissor), que é responsável pela geração de Cupons Fiscais Eletrônicos. Assim, o trabalho consiste em utilizar os conceitos traçados para o modelo fiscal e adaptar às necessidades da prescrição médica, propondo um novo modelo de automação e controle do processo de prescrição e dispensa de medicamentos baseado na Receita Médica Eletrônica (RM-e). / This research aims to propose a model of automation and standardization of the process of control of medical prescription and dispensing of medicines in Brazil, based on the Authentication and Transmission System (Sistema Autenticador Transmissor - SAT) applied to the fiscal control of the retail trade and implemented in the State of São Paulo, Brazil. The aim is to analyze the current scenario of medical prescription in the country, its operational characteristics, the increasingly frequent problems related to irregular drug trade and the abusive use of controlled substances. The measures adopted to control the sector in Brazil, Portugal and the United States of America, as well as their requirements and degrees of operation are presented. Based on the gap found in the actions adopted by Brazil, the motivation of the present study is the search for the characteristics of the Brazilian scenario and its non-adherence to the international proposals, mainly because they require technical infrastructure, legal order and availability Incompatible investments. In view of this need, a process control model was searched in other areas that adhered to the Brazilian reality presented, which is why a solution found was used to control the retail trade, through the SAT (Authentication and Transmission System), which is responsible for the generation of Electronic Tax Coupons. Thus, the work consists of using the concepts outlined for the fiscal model and adapting to the needs of the medical prescription, proposing a new model of automation and control of the prescription and dispensing process based on Electronic Medical Prescription (Receita Médica Eletrônica RM-e).