Target of my diploma thesis is barcode study and implementation to SMT assembly processes. This thesis contains two main parts. The first one is devoted to basic types of barcodes, reading technologies and industrial process mapping in PCB assembly. The second part is devoted to theoretical proposal and physical realization of system for materials flow monitoring. Barcode is contained in this system. Practical part of this thesis is tested in a company realizing contract manufacturing in PCB assembly - SMT and THT.

Society relies on increasingly complex software and hardware systems, hence techniques capable of proving that they behave as expected are of great and growing interest. Formal verification procedures employ mathematically sound reasoning to address this need. This thesis proposes novel techniques for the verification and falsification of expressive specifications on timed and infinite-state systems. An expressive specification language allows the description of the intended behaviour of a system via compact formal statements written at an abstraction level that eases the review process. Falsifying a specification corresponds to identifying an execution of the system that violates the property (i.e. a witness). The capability of identifying witnesses is a key feature in the iterative refinement of the design of a system, since it provides a description of how a certain error can occur. The designer can analyse the witness and take correcting actions by refining either the description of the system or its specification. The contribution of this thesis is twofold. First, we propose a semantics for Metric Temporal Logic that considers four different models of time (discrete, dense, super-discrete and super-dense). We reduce its verification problem to finding an infinite fair execution (witness) for an infinite-state system with discrete time. Second, we define a novel SMT-based algorithm to identify such witnesses. The algorithm employs a general representation of such executions that is both informative to the designer and provides sufficient structure to automate the search of a witness. We apply the proposed techniques to benchmarks taken from software, infinite-state, timed and hybrid systems. The experimental results highlight that the proposed approaches compete and often outperform specific (application tailored) techniques currently used in the state of the art.

With the increase of device complexity and test-data volume required to guarantee adequate defect coverage, external testing is becoming increasingly difficult and expensive. Logic Built-in Self Test (LBIST) is a viable alternative test strategy as it helps reduce dependence on an elaborate external test equipment, enables the application of a large number of random tests, and allows for at-speed testing. The main problem with LBIST is suboptimal fault coverage achievable with random vectors. LFSR reseeding is used to increase the coverage. However, to achieve satisfactory coverage, one often needs a large number of seeds. Computing a small number of seeds for LBIST reseeding still remains a tremendous challenge, since the vectors needed to detect all faults may be spread across the huge LFSR vector space. In this work, we propose new methods to enable the computation of a small number of LFSR seeds to cover all stuck-at faults as a first-order satisfiability problem involving extended theories. We present a technique based on SMT (Satisfiability Modulo Theories) with the theory of bit-vectors to combine the tasks of test-generation and seed computation. We describe a seed reduction flow which is based on the `chaining' of faults instead of pre-computed vectors. We experimentally demonstrate that our method can produce very small sets of seeds for complete stuck-at fault coverage. Additionally, we present methods for inserting test-points to enhance the testability of a circuit in such a way as to allow even further reduction in the number of seeds. / Master of Science

Historical text constitutes a rich source of information for historians and other researchers in humanities. Many texts are however not available in an electronic format, and even if they are, there is a lack of NLP tools designed to handle historical text. In my thesis, I aim to provide a generic workflow for automatic linguistic analysis and information extraction from historical text, with spelling normalisation as a core component in the pipeline. In the spelling normalisation step, the historical input text is automatically normalised to a more modern spelling, enabling the use of existing taggers and parsers trained on modern language data in the succeeding linguistic analysis step. In the final information extraction step, certain linguistic structures are identified based on the annotation labels given by the NLP tools, and ranked in accordance with the specific information need expressed by the user. An important consideration in my implementation is that the pipeline should be applicable to different languages, time periods, genres, and information needs by simply substituting the language resources used in each module. Furthermore, the reuse of existing NLP tools developed for the modern language is crucial, considering the lack of linguistically annotated historical data combined with the high variability in historical text, making it hard to train NLP tools specifically aimed at analysing historical text. In my evaluation, I show that spelling normalisation can be a very useful technique for easy access to historical information content, even in cases where there is little (or no) annotated historical training data available. For the specific information extraction task of automatically identifying verb phrases describing work in Early Modern Swedish text, 91 out of the 100 top-ranked instances are true positives in the best setting.

We investigate a new approach for SMT system training within the streaming model of computation. We develop and test incrementally retrainable models which, given an incoming stream of new data, can efficiently incorporate the stream data online. A naive approach using a stream would use an unbounded amount of space. Instead, our online SMT system can incorporate information from unbounded incoming streams and maintain constant space and time. Crucially, we are able to match (or even exceed) translation performance of comparable systems which are batch retrained and use unbounded space. Our approach is particularly suited for situations when there is arbitrarily large amounts of new training material and we wish to incorporate it efficiently and in small space. The novel contributions of this thesis are: 1. An online, randomised language model that can model unbounded input streams in constant space and time. 2. An incrementally retrainable translationmodel for both phrase-based and grammarbased systems. The model presented is efficient enough to incorporate novel parallel text at the single sentence level. 3. Strategies for updating our stream-based language model and translation model which demonstrate how such components can be successfully used in a streaming translation setting. This operates both within a single streaming environment and also in the novel situation of having to translate multiple streams. 4. Demonstration that recent data from the stream is beneficial to translation performance. Our stream-based SMT system is efficient for tackling massive volumes of new training data and offers-up new ways of thinking about translating web data and dealing with other natural language streams.

CertiCrypt est une bibliothèque qui permet de vérifier la sécurité exacte de primitives cryptographiques dans l'assistant à la preuve Coq. CertiCrypt instrumente l'approche des preuves par jeux, et repose sur de nombreux domaines comme les probabilités, la complexité, l'algèbre, la sémantique des langages de programmation, et les optimisations de programmes. Dans cette thèse, nous présentons deux exemples d'utilisation d'EasyCrypt: le schéma d'encryption Hashed ElGamal, et les protocoles à connaissance nulle. Ces exemples, ainsi que les travaux antérieurs sur CertiCrypt, démontrent qu'il est possible de formaliser des preuves complexes; toutefois, l'utilisation de CertiCrypt demande une bonne expertise en Coq, et demeure laborieuse. Afin de faciliter l'adoption des preuves formelles par la communauté cryptographique, nous avons développé EasyCrypt, un outil semi-automatique capable de reconstruire des preuves formelles de sécurité à partir d'une ébauche formelle de preuve. EasyCrypt utilise des outils de preuves automatiques pour vérifier les ébauches de preuves, puis les compiles vers des preuves vérifiables avec CertiCrypt. Nous validons EasyCrypt en prouvant à nouveau Hashed ElGamal, et comparons cette nouvelle preuve avec celle en CertiCrypt. Nous prouvons également le schéma d'encryption Cramer-Shoup. Enfin, nous expliquerons comment étendre le langage de CertiCrypt à des classes de complexité implicite, permettant de modéliser la notion de fonctions en temps polynomial.

Multithreaded processors are now common in the industry as they offer high performance at a low cost. Traditionally, in such processors, the assignation of hardware resources between the multiple threads is done implicitly, by the hardware policies. However, a new class of multithreaded hardware allows the explicit allocation of resources to be controlled or biased by the software. Currently, there is little or no coordination between the allocation of resources done by the hardware and the prioritization of tasks done by the software.This thesis targets to narrow the gap between the software and the hardware, with respect to the hardware resource allocation, by proposing a new explicit resource allocation hardware mechanism and novel schedulers that use the currently available hardware resource allocation mechanisms.It approaches the problem in two different types of computing systems: on the high performance computing domain, we characterize the first processor to present a mechanism that allows the software to bias the allocation hardware resources, the IBM POWER5. In addition, we propose the use of hardware resource allocation as a way to balance high performance computing applications. Finally, we propose two new scheduling mechanisms that are able to transparently and successfully balance applications in real systems using the hardware resource allocation. On the soft real-time domain, we propose a hardware extension to the existing explicit resource allocation hardware and, in addition, two software schedulers that use the explicit allocation hardware to improve the schedulability of tasks in a soft real-time system.In this thesis, we demonstrate that system performance improves by making the software aware of the mechanisms to control the amount of resources given to each running thread. In particular, for the high performance computing domain, we show that it is possible to decrease the execution time of MPI applications biasing the hardware resource assignation between threads. In addition, we show that it is possible to decrease the number of missed deadlines when scheduling tasks in a soft real-time SMT system.

Power gating is a technique commonly used for runtime leakage reduction in digital CMOS circuits. In microprocessors, power gating can be implemented by using sleep transistors to selectively deactivate circuit modules when they are idle during program execution. In this dissertation, a framework for power gating arithmetic functional units in embedded microprocessors with architecture and compiler support is proposed. During compile time, program regions are identified where one or more functional units are idle and sleep instructions are inserted into the code so that those units can be put to sleep during program execution. Subsequently, when their need is detected during the instruction decode stage, they are woken up with the help of hardware control signals. For a set of benchmarks from the MiBench suite, leakage energy savings of 27% and 31% are achieved (based on a 70 nm PTM model) in the functional units of a processor, modeled on the ARM architecture, with and without floating point units, respectively. Further, the impact of traditional performance-enhancing compiler optimizations on the amount of leakage savings obtained with this framework is studied through analysis and simulations. Based on the observations, a leakage-aware compilation flow is derived that improves the effectiveness of this framework. It is observed that, through the use of various compiler optimizations, an additional savings of around 15% and even up to 9X leakage energy savings in individual functional units is possible. Finally,in the context of multi-core processors supporting multithreading, three different microarchitectural techniques, for different multithreading schemes, are investigated for state-retentive power gating of register files. In an in-order core, when a thread gets blocked due to a memory stall, the corresponding register file can be placed in a low leakage state. When the memory stall gets resolved, the register file is activated so that it may be accessed again. The overhead due to wake-up latency is completely hidden in two of the schemes, while it is hidden for the most part in the third. Experimental results on multiprogrammed workloads comprised of SPEC 2000 integer benchmarks show that, in an 8-core processor executing 64 threads, the average leakage savings in the register files, modeled in FreePDK 45 nm MTCMOS technology, are 42% in coarse-grained multithreading, while they are between 7% and 8% in fine-grained and simultaneous multithreading. The contributions of this dissertation represent a significant advancement in the quest for reducing leakage energy consumption in microprocessors with minimal degradation in performance.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-12-12T17:57:13Z No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-12-13T18:11:52Z (GMT) No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Made available in DSpace on 2017-12-13T18:11:52Z (GMT). No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) Previous issue date: 2017-09-05 / Em muitas aplica??es de m?todos formais, como verifica??o formal, s?ntese de programas, testes autom?ticos e an?lise de programas, ? comum depender de solucionadores de satisfatibilidade m?dulo teorias (SMT) como backends para resolver automaticamente condi??es que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a efici?ncia dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribui??o ? fornecer um arcabou?o uniforme e eficiente para raciocinar com f?rmulas quantificadas em solucionadores SMT, em que, geralmente, v?rias t?cnicas de instancia??o s?o empregadas para lidar com quantificadores. Mostramos que as principais t?cnicas de instancia??o podem ser lan?adas neste arcabou?o unificador para lidar com f?rmulas quantificadas com igualdade e fun??es n?o interpretadas. O arcabou?o baseia-se no problema de E-ground (dis)unifica??o, uma varia??o do problema cl?ssico de E-unifica??o r?gida. Apresentamos um c?lculo correto e completo para resolver esse problema na pr?tica: Fechamento de Congru?ncia com Vari?veis Livres (CCFV). Uma avalia??o experimental ? apresentada, na qual medimos o impacto das otimiza??es e t?cnicas de instancia??o baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementa??es exibem melhorias em rela??o ?s abordagens de ?ltima gera??o em v?rias bibliotecas de refer?ncia, decorrentes de aplica??es do mundo real. Nossa segunda contribui??o ? uma estrutura para o processamento de f?rmulas ao mesmo tempo que produz demonstra??es detalhadas. Nosso objetivo ? aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de racioc?nio automatizado similares, fornecendo justificativas que podem ser verificadas com efici?ncia de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstra??o, por exemplo, geralmente requerem a reconstru??o da justifica??o fornecida pelo solucionador em uma determinada obriga??o de prova. Os principais componentes da nossa estrutura de produ??o de demonstra??es s?o um algoritmo gen?rico de recurs?o contextual e um conjunto extens?vel de regras de infer?ncia. Clausifica??o, Skolemiza??o, simplifica??es espec?ficas de teorias e expans?o das express?es "let" s?o exemplos dessa estrutura. Com estruturas de dados adequadas, a gera??o de demonstra??es cria apenas uma sobrecarga de tempo linear, e as demonstra??es podem ser verificadas em tempo linear. Tamb?m implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do c?digo, aumentando o n?mero de problemas para os quais demonstra??es detalhadas podem ser produzidas. / In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.

This study focuses on and tries to identify areas where machine translation can be useful by examining translated fictional and non-fictional texts, and the extent to which these different text types are better or worse suited for machine translation.  It additionally evaluates the performance of the free online translation tool Google Translate (GT). The BLEU automatic evaluation metric for machine translation was used for this study, giving a score of 27.75 BLEU value for fictional texts and 32.16 for the non-fictional texts. The non-fictional texts are samples of law documents, (commercial) company reports, social science texts (religion, welfare, astronomy) and medicine. These texts were selected because of their degree of difficulty. The non-fictional sentences are longer than those of the fictional texts and in this regard MT systems have struggled. In spite of having longer sentences, the non-fictional texts got a higher BLUE score than the fictional ones. It is speculated that one reason for the higher score of non-fictional texts might be that more specific terminology is used in these texts, leaving less room for subjective interpretation than for the fictional texts. There are other levels of meaning at work in the fictional texts that the human translator needs to capture.