Sequence learning describes the process of understanding the spatio-temporal relations in a sequence in order to classify it, label its elements or generate new sequences. Due to the prevalence of structured sequences in nature and everyday life, it has many practical applications including any language related processing task. One particular such task that has seen recent success using sequence learning techniques is the optical recognition of characters (OCR). State-of-the-art sequence learning solutions for OCR achieve high performance through supervised training, which requires large amounts of transcribed training data. On the other hand, few solutions have been proposed on how to apply sequence learning in the absence of such data, which is especially common for hard to transcribe historical documents. Rather than solving the unsupervised training problem, research has focused on creating efficient methods for collecting training data through smart annotation tools or generating synthetic training data. These solutions come with various limitations and do not solve all of the related problems. In this work, first the use of erroneous transcriptions for supervised sequence learning is introduced and it is described how this concept can be applied in unsupervised training scenarios by collecting or generating such transcriptions. The proposed OCR pipeline reduces the need of domain specific expertise to apply OCR, with the goal of making it more accessible. Furthermore, an approach for evaluating sequence learning OCR models in the absence of reference transcriptions is presented and its different properties compared to the standard method are discussed. In a second approach, unsupervised OCR is treated as an alignment problem between the latent features of the different language modalities. The outlined solution is to extract language properties from both the text and image domain through adversarial training and learn to align them by adding a cycle consistency constraint. The proposed approach has some strict limitations on the input data, but the results encourage future research into more widespread applications.

In the past, information and knowledge dissemination was relegated to the brick-and-mortar classrooms, newspapers, radio, and television. As these processes were simple and centralized, the models behind them were well understood and so were the empirical methods for optimizing them. In today’s world, the internet and social media has become a powerful tool for information and knowledge dissemination: Wikipedia gets more than 1 million edits per day, Stack Overflow has more than 17 million questions, 25% of US population visits Yahoo! News for articles and discussions, Twitter has more than 60 million active monthly users, and Duolingo has 25 million users learning languages online. These developments have introduced a paradigm shift in the process of dissemination. Not only has the nature of the task moved from being centralized to decentralized, but the developments have also blurred the boundary between the creator and the consumer of the content, i.e., information and knowledge. These changes have made it necessary to develop new models, which are better suited to understanding and analysing the dissemination, and to develop new methods to optimize them. At a broad level, we can view the participation of users in the process of dissemination as falling in one of two settings: collaborative or competitive. In the collaborative setting, the participants work together in crafting knowledge online, e.g., by asking questions and contributing answers, or by discussing news or opinion pieces. In contrast, as competitors, they vie for the attention of their followers on social media. This thesis investigates both these settings. The first part of the thesis focuses on the understanding and analysis of content being created online collaboratively. To this end, I propose models for understanding the complexity of the content of collaborative online discussions by looking exclusively at the signals of agreement and disagreement expressed by the crowd. This leads to a formal notion of complexity of opinions and online discussions. Next, I turn my attention to the participants of the crowd, i.e., the creators and consumers themselves, and propose an intuitive model for both, the evolution of their expertise and the value of the content they collaboratively contribute and learn from on online Q&A based forums. The second part of the thesis explores the competitive setting. It provides methods to help the creators gain more attention from their followers on social media. In particular, I consider the problem of controlling the timing of the posts of users with the aim of maximizing the attention that their posts receive under the idealized setting of full-knowledge of timing of posts of others. To solve it, I develop a general reinforcement learning based method which is shown to have good performance on the when-to-post problem and which can be employed in many other settings as well, e.g., determining the reviewing times for spaced repetition which lead to optimal learning. The last part of the thesis looks at methods for relaxing the idealized assumption of full knowledge. This basic question of determining the visibility of one’s posts on the followers’ feeds becomes difficult to answer on the internet when constantly observing the feeds of all the followers becomes unscalable. I explore the links of this problem to the well-studied problem of web-crawling to update a search engine’s index and provide algorithms with performance guarantees for feed observation policies which minimize the error in the estimate of visibility of one’s posts.

In order to improve performance or conserve energy, modern hardware implementations have adopted weak memory models; that is, models of concurrency that allow more outcomes than the classic sequentially consistent (SC) model of execution. Modern programming languages similarly provide their own language-level memory models, which strive to allow all the behaviors allowed by the various hardware-level memory models, as well as those that can occur as a result of desired compiler optimizations. As these weak memory models are often rather intricate, it can be difficult for programmers to keep track of all the possible behaviors of their programs. It is therefore very useful to have an abstraction layer over the model that can be used to ensure program correctness without reasoning about the underlying memory model. Program logics are a way of constructing such an abstraction—one can use their syntactic rules to reason about programs, without needing to understand the messy details of the memory model for which the logic has been proven sound. Unfortunately, most of the work on formal verification in general, and program logics in particular, has so far assumed the SC model of execution. This means that new logics for weak memory have to be developed. This thesis presents two such logics—fenced separation logic (FSL) and weak separation logic (Weasel)—which are sound for reasoning under two different weak memory models. FSL considers the C/C++ concurrency memory model, supporting several of its advanced features. The soundness of FSL depends crucially on a specific strengthening of the model which eliminates a certain class of undesired behaviors (so-called out-of-thin-air behaviors) that were inadvertently allowed by the original C/C++ model. Weasel works under weaker assumptions than FSL, considering a model which takes a more fine-grained approach to the out-of-thin-air problem. Weasel's focus is on exploring the programming constructs directly related to out-of-thin-air behaviors, and is therefore significantly less feature-rich than FSL. Using FSL and Weasel, the thesis explores the key challenges in reasoning under weak memory models, and what effect different solutions to the out-of-thin-air problem have on such reasoning. It explains which reasoning principles are preserved when moving from a stronger to a weaker model, and develops novel proof techniques to establish soundness of logics under weaker models.

Deep learning has achieved significant improvements in a variety of tasks in computer vision applications with an open image dataset which has a large amount of data. However, the acquisition of a large number of the dataset is a challenge in real-world applications, especially if they are new eras for deep learning. Furthermore, the distribution of class in the dataset is often imbalanced. The data imbalance problem is frequently bottlenecks of the neural network performance in classification. Recently, the potential of generative adversarial networks (GAN) as a data augmentation method on minority data has been studied. This dissertation investigates using GAN and transfer learning to improve the performance of the classification under imbalanced data conditions. We first propose a classification enhancement generative adversarial networks (CEGAN) to enhance the quality of generated synthetic minority data and more importantly, to improve the prediction accuracy in data imbalanced condition. Our experiments show that approximating the real data distribution using CEGAN improves the classification performance significantly in data imbalanced conditions compared with various standard data augmentation methods. To further improve the performance of the classification, we propose a novel supervised discriminative feature generation method (DFG) for minority class dataset. DFG is based on the modified structure of Generative Adversarial Network consisting of four independent networks: generator, discriminator, feature extractor, and classifier. To augment the selected discriminative features of minority class data by adopting attention mechanism, the generator for class-imbalanced target task is trained while feature extractor and classifier are regularized with the pre-trained ones from large source data. The experimental results show that the generator of DFG enhances the augmentation of label-preserved and diverse features, and classification results are significantly improved on the target task. In this thesis, these proposals are deployed to bearing fault detection and diagnosis of induction motor and shipping label recognition and validation for logistics. The experimental results for bearing fault detection and diagnosis conclude that the proposed GAN-based framework has good performance on the imbalanced fault diagnosis of rotating machinery. The experimental results for shipping label recognition and validation also show that the proposed method achieves better performance than many classical and state-of-the-art algorithms.

Dataflow process networks (DPNs) consist of statically defined process nodes with First-In-First-Out (FIFO) buffered point-to-point connections. DPNs are intrinsically data-driven, i.e., node actions are not synchronized among each other and may fire whenever sufficient input operands arrived at a node. In this original form, DPNs are data-driven and therefore a suitable model of computation (MoC) for asynchronous and distributed systems. For DPNs having nodes with only static consumption/production rates, however, one can easily derive an optimal schedule that can then be used to implement the DPN in a time-driven (clock-driven) way, where each node fires according to the schedule. Both data-driven and time-driven MoCs have their own advantages and disadvantages. For this reason, desynchronization techniques are used to convert clock-driven models into data-driven ones in order to more efficiently support distributed implementations. These techniques preserve the functional specification of the synchronous models and moreover preserve properties like deadlock-freedom and bounded memory usage that are otherwise difficult to ensure in DPNs. These desynchronized models are the starting point of this thesis. While the general MoC of DPNs does not impose further restrictions, many different subclasses of DPNs representing different dataflow MoCs have been considered over time like Kahn process networks, cyclo-static and synchronous DPNs. These classes mainly differ in the kinds of behaviors of the processes which affect on the one hand the expressiveness of the DPN class as well as the methods for their analysis (predictability) and synthesis (efficiency). A DPN may be heterogeneous in the sense that different processes in the network may exhibit different kinds of behaviors. A heterogeneous DPN therefore can be effectively used to model and implement different components of a system with different kinds of processes and therefore different dataflow MoCs. Design tools for modeling like Ptolemy and FERAL are used to model and to design parallel embedded systems using well-defined and precise MoCs, including different dataflow MoCs. However, there is a lack of automatic synthesis methods to analyze and to evaluate the artifacts exhibited by particular MoCs. Second, the existing design tools for synthesis are usually restricted to the weakest classes of DPNs, i.e., cyclo-static and synchronous DPNs where each tool only supports a specific dataflow MoC. This thesis presents a model-based design based on different dataflow MoCs including their heterogeneous combinations. This model-based design covers in particular the automatic software synthesis of systems from DPN models. The main objective is to validate, evaluate and compare the artifacts exhibited by different dataflow MoCs at the implementation level of embedded systems under the supervision of a common design tool. We are mainly concerned about how these different dataflow MoCs affect the synthesis, in particular, how they affect the code generation and the final implementation on the target hardware. Moreover, this thesis also aims at offering an efficient synthesis method that targets and exploits heterogeneity in DPNs by generating implementations based on the kinds of behaviors of the processes. The proposed synthesis design flow therefore generally starts from the desynchronized dataflow models and automatically synthesizes them for cross-vendor target hardware. In particular, it provides a synthesis tool chain, including different specialized code generators for specific dataflow MoCs, and a runtime system that finally maps models using a combination of different dataflow MoCs on the target hardware. Moreover, the tool chain offers a platform-independent code synthesis method based on the open computing language (OpenCL) that enables a more generalized synthesis targeting cross-vendor commercial off-the-shelf (COTS) heterogeneous platforms.

Today, information systems are often distributed to achieve high availability and low latency. These systems can be realized by building on a highly available database to manage the distribution of data. However, it is well known that high availability and low latency are not compatible with strong consistency guarantees. For application developers, the lack of strong consistency on the database layer can make it difficult to reason about their programs and ensure that applications work as intended. We address this problem from the perspective of formal verification. We present a specification technique, which allows specifying functional properties of the application. In addition to data invariants, we support history properties. These let us express relations between events, including invocations of the application API and operations on the database. To address the verification problem, we have developed a proof technique that handles concurrency using invariants and thereby reduces the problem to sequential verification. The underlying system semantics, technique and its soundness proof are all formalized in the interactive theorem prover Isabelle/HOL. Additionally, we have developed a tool named Repliss which uses the proof technique to enable partially automated verification and testing of applications. For verification, Repliss generates verification conditions via symbolic execution and then uses an SMT solver to discharge them.

In the increasingly competitive public-cloud marketplace, improving the efficiency of data centers is a major concern. One way to improve efficiency is to consolidate as many VMs onto as few physical cores as possible, provided that performance expectations are not violated. However, as a prerequisite for increased VM densities, the hypervisor’s VM scheduler must allocate processor time efficiently and in a timely fashion. As we show in this thesis, contemporary VM schedulers leave substantial room for improvements in both regards when facing challenging high-VM-density workloads that frequently trigger the VM scheduler. As root causes, we identify (i) high runtime overheads and (ii) unpredictable scheduling heuristics. To better support high VM densities, we propose Tableau, a VM scheduler that guarantees a minimum processor share and a maximum bound on scheduling delay for every VM in the system. Tableau combines a low-overhead, core-local, table-driven dispatcher with a fast on-demand table-generation procedure (triggered on VM creation/teardown) that employs scheduling techniques typically used in hard real-time systems. Further, we show that, owing to its focus on efficiency and scalability, Tableau provides comparable or better throughput than existing Xen schedulers in dedicated-core scenarios as are commonly employed in public clouds today. Tableau also extends this design by providing the ability to use idle cycles in the system to perform low-priority background work, without affecting the performance of primary VMs, a common requirement in public clouds. Finally, VM churn and workload variations in multi-tenant public clouds result in changing interference patterns at runtime, resulting in performance variation. In particular, variation in last-level cache (LLC) interference has been shown to have a significant impact on virtualized application performance in cloud environments. Tableau employs a novel technique for dealing with dynamically changing interference, which involves periodically regenerating tables with the same guarantees on utilization and scheduling latency for all VMs in the system, but having different LLC interference characteristics. We present two strategies to mitigate LLC interference: a randomized approach, and one that uses performance counters to detect VMs running cache-intensive workloads and selectively mitigate interference.

Wearable systems have been applied in various studies as a convenient and efficient solution for monitoring health and fitness. There is a large number of commercial products in the growing market of wearable systems that can be worn as wristbands, clasps, or in the form of clothing. However, these systems only provide general information about the intensity and possibly the type of user activity, which is not sufficient for monitoring strength and conditioning exercises. To achieve optimal muscular development and reduce the risk of exercise-related injury, a wearable system should provide reliable biomechanical details of body movements as well as real-time feedback during training. In addition, it should be an affordable, comfortable, and easy-to-use platform for different types of users with different levels of movement intensity and work autonomously over long periods of time. These requirements impose many challenges on the design of such systems. This study presents most of these challenges and proposes solutions. In this work, a low-cost and light-weight tracking suit is designed and developed, which integrates multiple Inertial measurement units (IMUs). A novel data acquisition approach is proposed to improve the energy efficiency of the system without the use of additional devices. Given a valid calibration, IMUs, comprising inertial sensors and magnetometers, can provide accurate orientation in three dimensions (3D). Unlike the inertial sensors, magnetometer measurements are easily disturbed by ferromagnetic materials in the vicinity of the sensor, either inside the IMU casing or in the final mounting position. Therefore, this work proposes a practical method for in-field magnetometer calibration and alignment to the coordinate system of an IMU. This method is verified experimentally in terms of magnitude deviation, heading error, plane projections, and repeatability. The results show a higher accuracy compared to the related works. Sensor to body calibration is a critical requirement for capturing accurate body movements. Therefore, a theoretical analysis of an existing method is carried out, showing its limited applicability for hip and knee joints. On this basis, by applying geometric constraints, a method is proposed for estimating the positions of three IMUs (mounted on the pelvis, upper leg, and lower leg) simultaneously. The result of experiments with different types of movements and arbitrary intensity shows that the proposed method outperforms the previous method. Moreover, two real-time tracking algorithms based on the extended Kalman filter (EKF) are proposed for lower body motion estimation. The first approach provides an estimate of the pelvis orientation. The second approach estimates the position of IMUs and the joint angles with respect to the pelvis by incorporating the result of body-IMU calibration. The modeling of the biomechanical constraint compensates for lack of a reliable horizontal reference, e.g. Earth’s magnetic field. Experiments to track strength exercises such as squat and hip abduction/adduction show promising results. In order to finally provide a monitoring application in which users can follow the exercises according to the instructions and taking into account their health status, this work proposes an approach for the identification of exercises based on an online template matching algorithm, which detects the correct performance using a previously recorded exercise in the presence of a supervisor. Therefore, unlike most identification algorithms, no large datasets are required for training. The algorithm is optimized here to reduce execution time while maintaining the accuracy. Experiments show that for the specific application of this study, i.e. squat exercise monitoring, the proposed method outperforms the related works in optimization of online template matching.

To improve efficiency of memory accesses, modern multiprocessor architectures implement a whole range of different weak memory models. The behavior of performance-critical code depends on the underlying hardware. There is a rising demand for verification tools that take the underlying memory model into account. This work examines a variety of prevalent problems in the field of program verification of increasing complexities: testing, reachability, portability and memory model synthesis. We give efficient tools to solve these problems. What sets the presented methods apart is that they are not limited to some few given architectures. They are universal: The memory model is given as part of the input. We make use of the CAT language to succinctly describe axiomatic memory models. CAT has been used to define the semantics of assembly for x86/TSO, ARMv7, ARMv8, and POWER but also the semantics of programming languages such as C/C++, including the Linux kernel concurrency primitives. This work shows that even the simple testing problem is NP-hard for most memory models. It does so using a general reduction technique that applies to a range of models. It examines the more difficult program verification under a memory model and introduces Dartagnan, a bounded model checker (BMC) that encodes the problem as an SMT-query and makes use of advanced encoding techniques. The program portability problem is shown to be even harder. Despite this, it is solved efficiently by the tool Porthos which uses a guided search to produce fast results for most practical instances. A memory model is synthesized by Aramis for a given set of reachability results. Concurrent program verification is generally undecidable even for sequential consistency. As an alternative to BMC, we propose a new CEGAR method for Petri net invariant synthesis. We again use SMT-queries as a back-end.

Optical Character Recognition (OCR) is one of the central problems in pattern recognition. Its applications have played a great role in the digitization of document images collected from het- erogeneous sources. Many of the well-known scripts have OCR systems with sufficiently high performance that enables OCR applications in industrial/commercial settings. However, OCR sys- tems yield very-good results only on a narrow domain and very-specific use cases. Thus, it is still a challenging task, and there are other exotic languages with indigenous scripts, such as Amharic, for which no well-developed OCR systems exist. As many as 100 million people speak Amharic, and it is an official working language of Ethiopia. Amharic script contains about 317 different alphabets derived from 34 consonants with small changes. The change involves shortening or elongating one of its main legs or adding small diacritics to the right, left, top, or bottom of the consonant character. Such modifications lead the characters to have similar shapes and make the recognition task complex, but this is particularly interesting for charac- ter recognition research. So far, Amharic script recognition models are developed based on classical machine learning techniques, and they are very limited in addressing the issues for Amharic OCR. The motivation of this thesis is, therefore, to explore and tailor contemporary deep learning tech- niques for the OCR of Amharic. This thesis addresses the challenges in Amharic OCR through two main contributions. The first contribution is an algorithmic contribution in which we investigate deep learning approaches that suit the demand for Amharic OCR. The second is a technical contribution that comprises several works towards the OCR model development; thus, it introduces a new Amharic database consisting of collections of images annotated at a character and text-line level. It also presents a novel CNN- based framework designed by leveraging the grapheme of characters in Fidel-Gebeta (where Fidel- Gebeta consists of the full set of Amharic characters in matrix structure) and achieves 94.97% overall character recognition accuracy. In addition to character level methods, text-line level methods are also investigated and devel- oped based on sequence-to-sequence learning. These models avoid several of the pre-processing stages used in prior works by eliminating the need to segment individual characters. In this design, we use a stack of CNNs, before the Bi-LSTM layers and train from end-to-end. This model out- performs the LSTM-CTC based network, on average, by a CER of 3.75% with the ADOCR test set. Motivated by the success of attention, in addressing the problems’ of long sequences in Neural Machine Translation (NMT), we proposed a novel attention-based methodology by blending the attention mechanism into CTC objective function. This model performs far better than the existing techniques with a CER of 1.04% and 0.93% on printed and synthetic text-line images respectively. Finally, this thesis provides details on various tasks that have been performed for the development of Amharic OCR. As per our empirical analysis, the majority of the errors are due to poor annotation of the dataset. As future work, the methods proposed in this thesis should be further investigated and extended to deal with handwritten and historical Amharic documents.