OpenRaiser/Intern-Atlas huggingface dataset:
Specialization of Generic Array Accesses After Inlining
Venue: arXiv cs.PL 2017
Year: 2017

We have implemented an optimization that specializes type-generic array accesses after inlining of polymorphic functions in the native-code OCaml compiler. Polymorphic array operations (read and write) in OCaml require runtime type dispatch because of ad hoc memory representations of integer and float arrays. It cannot be removed even after being monomorphized by inlining because the intermediate language is mostly untyped. We therefore extended it with explicit type application like System F (while keeping implicit type abstraction by means of unique identifiers for type variables). Our optimization has achieved up to 21% speed-up of numerical programs.
RFID Localisation For Internet Of Things Smart Homes: A Survey
Venue: arXiv cs.NI 2017
Year: 2017

The Internet of Things (IoT) enables numerous business opportunities in fields as diverse as e-health, smart cities, smart homes, among many others. The IoT incorporates multiple long-range, short-range, and personal area wireless networks and technologies into the designs of IoT applications. Localisation in indoor positioning systems plays an important role in the IoT. Location Based IoT applications range from tracking objects and people in real-time, assets management, agriculture, assisted monitoring technologies for healthcare, and smart homes, to name a few. Radio Frequency based systems for indoor positioning such as Radio Frequency Identification (RFID) is a key enabler technology for the IoT due to its costeffective, high readability rates, automatic identification and, importantly, its energy efficiency characteristic. This paper reviews the state-of-the-art RFID technologies in IoT Smart Homes applications. It presents several comparable studies of RFID based projects in smart homes and discusses the applications, techniques, algorithms, and challenges of adopting RFID technologies in IoT smart home systems.
Automatically Annotated Turkish Corpus for Named Entity Recognition and Text Categorization using Large-Scale Gazetteers
Venue: arXiv cs.CL 2017
Year: 2017

Turkish Wikipedia Named-Entity Recognition and Text Categorization (TWNERTC) dataset is a collection of automatically categorized and annotated sentences obtained from Wikipedia. We constructed large-scale gazetteers by using a graph crawler algorithm to extract relevant entity and domain information from a semantic knowledge base, Freebase. The constructed gazetteers contains approximately 300K entities with thousands of fine-grained entity types under 77 different domains. Since automated processes are prone to ambiguity, we also introduce two new content specific noise reduction methodologies. Moreover, we map fine-grained entity types to the equivalent four coarse-grained types: person, loc, org, misc. Eventually, we construct six different dataset versions and evaluate the quality of annotations by comparing ground truths from human annotators. We make these datasets publicly available to support studies on Turkish named-entity recognition (NER) and text categorization (TC).
Iterative Multi-document Neural Attention for Multiple Answer Prediction
Venue: arXiv cs.CL 2017
Year: 2017

People have information needs of varying complexity, which can be solved by an intelligent agent able to answer questions formulated in a proper way, eventually considering user context and preferences. In a scenario in which the user profile can be considered as a question, intelligent agents able to answer questions can be used to find the most relevant answers for a given user. In this work we propose a novel model based on Artificial Neural Networks to answer questions with multiple answers by exploiting multiple facts retrieved from a knowledge base. The model is evaluated on the factoid Question Answering and top-n recommendation tasks of the bAbI Movie Dialog dataset. After assessing the performance of the model on both tasks, we try to define the long-term goal of a conversational recommender system able to interact using natural language and to support users in their information seeking processes in a personalized way.
Refining Trace Abstraction using Abstract Interpretation
Venue: arXiv cs.LO 2017
Year: 2017

The CEGAR loop in software model checking notoriously diverges when the abstraction refinement procedure does not derive a loop invariant. An abstraction refinement procedure based on an SMT solver is applied to a trace, i.e., a restricted form of a program (without loops). In this paper, we present a new abstraction refinement procedure that aims at circumventing this restriction whenever possible. We apply abstract interpretation to a program that we derive from the given trace. If the program contains a loop, we are guaranteed to obtain a loop invariant. We call an SMT solver only in the case where the abstract interpretation returns an indefinite answer. That is, the idea is to use abstract interpretation and an SMT solver in tandem. An experimental evaluation in the setting of trace abstraction indicates the practical potential of this idea.
Random Linear Fountain Code with Improved Decoding Success Probability
Venue: arXiv cs.NI 2017
Year: 2017

In this paper we study the problem of increasing the decoding success probability of random linear fountain code over GF(2) for small packet lengths used in delay-intolerant applications such as multimedia streaming. Such code over GF(2) are attractive as they have lower decoding complexity than codes over larger field size, but suffer from high transmission redundancy. In our proposed coding scheme we construct a codeword which is not a linear combination of any codewords previously transmitted to mitigate such transmission redundancy. We then note the observation that the probability of receiving a linearly dependent codeword is highest when the receiver has received k-1 linearly independent codewords. We propose using the BlockACK frame so that the codeword received after k-1 linearly independent codeword is always linearly independent, this reduces the expected redundancy by a factor of three.
A Family of Approximation Algorithms for the Maximum Duo-Preservation String Mapping Problem
Venue: arXiv cs.DS 2017
Year: 2017

In the Maximum Duo-Preservation String Mapping problem we are given two strings and wish to map the letters of the former to the letters of the latter so as to maximise the number of duos. A duo is a pair of consecutive letters that is mapped to a pair of consecutive letters in the same order. This is complementary to the well-studied Minimum Common String Partition problem, where the goal is to partition the former string into blocks that can be permuted and concatenated to obtain the latter string. Maximum Duo-Preservation String Mapping is APX-hard. After a series of improvements, Brubach [WABI 2016] showed a polynomial-time $3.25$-approximation algorithm. Our main contribution is that for any $ε>0$ there exists a polynomial-time $(2+ε)$-approximation algorithm. Similarly to a previous solution by Boria et al. [CPM 2016], our algorithm uses the local search technique. However, this is used only after a certain preliminary greedy procedure, which gives us more structure and makes a more general local search possible. We complement this with a specialised version of the algorithm that achieves $2.67$-approximation in quadratic time.
An Interface-Tracking Technique for Multiphase Flow with Soluble Surfactant
Venue: arXiv cs.CE 2017
Year: 2017

We adapt and extend a formulation for soluble surfactant transport in multiphase flows recently presented by Muradoglu & Tryggvason (JCP 274 (2014) 737-757) to the context of the Level Contour Reconstruction Method (Shin et al. IJNMF 60 (2009) 753-778) which is a hybrid method that combines the advantages of the Front-tracking and Level Set methods. Particularly close attention is paid to the formulation and numerical implementation of the surface gradients of surfactant concentration and surface tension. Various benchmark tests are performed to demonstrate the accuracy of different elements of the algorithm. To verify surfactant mass conservation, values for surfactant diffusion along the interface are compared with the exact solution for the problem of uniform expansion of a sphere. The numerical implementation of the discontinuous boundary condition for the source term in the bulk concentration is compared with the approximate solution. Surface tension forces are tested for Marangoni drop translation. Our numerical results for drop deformation in simple shear are compared with experiments and results from previous simulations. All benchmarking tests compare well with existing data thus providing confidence that our adapted LCRM formulation for surfactant advection and diffusion is accurate and effective in three-dimensional multiphase flows. We also demonstrate that this approach applies easily to massively parallel simulations.
Hash functions using chaotic iterations
Venue: arXiv cs.CR 2017
Year: 2017

In this paper, a novel formulation of discrete chaotic iterations in the field of dynamical systems is given. Their topological properties are studied: it is mathematically proved that, under some conditions, these iterations have a chaotic behavior in the meaning of Devaney. This chaotic behavior allows us to propose a way to generate new hash functions. An illustration example is detailed in order to show how to use our theoretical study in practice.
Causal Regularization
Venue: arXiv cs.LG 2017
Year: 2017

In application domains such as healthcare, we want accurate predictive models that are also causally interpretable. In pursuit of such models, we propose a causal regularizer to steer predictive models towards causally-interpretable solutions and theoretically study its properties. In a large-scale analysis of Electronic Health Records (EHR), our causally-regularized model outperforms its L1-regularized counterpart in causal accuracy and is competitive in predictive performance. We perform non-linear causality analysis by causally regularizing a special neural network architecture. We also show that the proposed causal regularizer can be used together with neural representation learning algorithms to yield up to 20% improvement over multilayer perceptron in detecting multivariate causation, a situation common in healthcare, where many causal factors should occur simultaneously to have an effect on the target variable.
Smartphone app to investigate the relationship between social connectivity and mental health
Venue: arXiv cs.SI 2017
Year: 2017

Interpersonal relationships are necessary for successful daily functioning and wellbeing. Numerous studies have demonstrated the importance of social connectivity for mental health, both through direct peer-to-peer influence and by the location of individuals within their social network. Passive monitoring using smartphones provides an advanced tool to map social networks based on the proximity between individuals. This study investigates the feasibility of using a smartphone app to measure and assess the relationship between social network metrics and mental health. The app collected Bluetooth and mental health data in 63 participants. Social networks of proximity were estimated from Bluetooth data and 95% of the edges were scanned at least every 30 minutes. The majority of participants found this method of data collection acceptable and reported that they would be likely to participate in future studies using this app. These findings demonstrate the feasibility of using a smartphone app that participants can install on their own phone to investigate the relationship between social connectivity and mental health.
Wideband Distributed Spectrum Sharing with Multichannel Immediate Multiple Access
Venue: arXiv cs.IT 2017
Year: 2017

This paper describes a radio architecture for distributed spectrum sharing of multiple channels among secondary users (SUs) in a wide band of frequencies and a localized area. A novel Multichannel Immediate Multiple Access (MIMA) physical layer is developed such that each SU can monitor all the channels simultaneously for incoming signals and achieve fast rendezvous within the multiple channels. The spectrum utilized by an SU pair can be changed dynamically based upon spectrum sensing at the transmitter and tracking synchronization and control messages at the receiver. Although information about the number of active SUs can be used to improve the spectrum sharing efficiency, the improvement is small relative to the cost of obtaining such information. Therefore, the architecture adopts Multichannel Carrier Sense Multiple Access (CSMA) for medium access control regardless of the number of active SUs. A prototype implementation of the architecture has been developed using an advanced software defined radio (SDR) platform. System tests demonstrate that the spectrum sharing efficiency of the prototype is close to an upper bound if the signal-to-noise ratio (SNR) is sufficiently high. Among other practical issues, imaged interference caused by hardware IQ imbalance limits system performance. In the prototype, the MIMA is based on an LTE waveform. Therefore, the spectrum sharing radio can be potentially applied to the 3.5 GHz radar band for Citizens Broadband Radio Service (CBRS).
Proving linearizability using forward simulations
Venue: arXiv cs.PL 2017
Year: 2017

Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy&Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to conceptually simple and natural correctness proofs for these implementations that are amenable to automation.
Mining User/Movie Preferred Features Based on Reviews for Video Recommendation System
Venue: arXiv cs.IR 2017
Year: 2017

In this work, we present an approach for mining user preferences and recommendation based on reviews. There have been various studies worked on recommendation problem. However, most of the studies beyond one aspect user generated- content such as user ratings, user feedback and so on to state user preferences. There is a prob- lem in one aspect mining is lacking for stating user preferences. As a demonstration, in collaborative filter recommendation, we try to figure out the preference trend of crowded users, then use that trend to predict current user preference. Therefore, there is a gap between real user preferences and the trend of the crowded people. Additionally, user preferences can be addressed from mining user reviews since user often comment about various aspects of products. To solve this problem, we mainly focus on mining product aspects and user aspects inside user reviews to directly state user preferences. We also take into account Social Network Analysis for cold-start item problem. With cold-start user problem, collaborative filter algorithm is employed in our work. The framework is general enough to be applied to different recommendation domains. Theoretically, our method would achieve a significant enhancement.
UStore: A Distributed Storage With Rich Semantics
Venue: arXiv cs.DB 2017
Year: 2017

Today's storage systems expose abstractions which are either too low-level (e.g., key-value store, raw-block store) that they require developers to re-invent the wheels, or too high-level (e.g., relational databases, Git) that they lack generality to support many classes of applications. In this work, we propose and implement a general distributed data storage system, called UStore, which has rich semantics. UStore delivers three key properties, namely immutability, sharing and security, which unify and add values to many classes of today's applications, and which also open the door for new applications. By keeping the core properties within the storage, UStore helps reduce application development efforts while offering high performance at hand. The storage embraces current hardware trends as key enablers. It is built around a data-structure similar to that of Git, a popular source code versioning system, but it also synthesizes many designs from distributed systems and databases. Our current implementation of UStore has better performance than general in-memory key-value storage systems, especially for version scan operations. We port and evaluate four applications on top of UStore: a Git-like application, a collaborative data science application, a transaction management application, and a blockchain application. We demonstrate that UStore enables faster development and the UStore-backed applications can have better performance than the existing implementations.
Complexity Classification Of The Six-Vertex Model
Venue: arXiv cs.CC 2017
Year: 2017

We prove a complexity dichotomy theorem for the six-vertex model. For every setting of the parameters of the model, we prove that computing the partition function is either solvable in polynomial time or #P-hard. The dichotomy criterion is explicit.
Bezier developable surfaces
Venue: arXiv cs.GR 2017
Year: 2017

In this paper we address the issue of designing developable surfaces with Bezier patches. We show that developable surfaces with a polynomial edge of regression are the set of developable surfaces which can be constructed with Aumann's algorithm. We also obtain the set of polynomial developable surfaces which can be constructed using general polynomial curves. The conclusions can be extended to spline surfaces as well.
Online and Offline Domain Adaptation for Reducing BCI Calibration Effort
Venue: arXiv cs.LG 2017
Year: 2017

Many real-world brain-computer interface (BCI) applications rely on single-trial classification of event-related potentials (ERPs) in EEG signals. However, because different subjects have different neural responses to even the same stimulus, it is very difficult to build a generic ERP classifier whose parameters fit all subjects. The classifier needs to be calibrated for each individual subject, using some labeled subject-specific data. This paper proposes both online and offline weighted adaptation regularization (wAR) algorithms to reduce this calibration effort, i.e., to minimize the amount of labeled subject-specific EEG data required in BCI calibration, and hence to increase the utility of the BCI system. We demonstrate using a visually-evoked potential oddball task and three different EEG headsets that both online and offline wAR algorithms significantly outperform several other algorithms. Moreover, through source domain selection, we can reduce their computational cost by about 50%, making them more suitable for real-time applications.
Comprehensive Survey of Evolutionary Morphological Soft Robotic Systems
Venue: arXiv cs.RO 2017
Year: 2017

Evolutionary robotics aims to automatically design autonomous adaptive morphological robots that can evolve to accomplish a specific task while adapting to environmental changes. Soft robotics have demonstrated the feasibility of evolutionary robotics for the synthesis of robots control and morphology. The motivation of developing evolutionary soft computing techniques to that can generate task oriented structures for morphological robots makes the domain of soft robotics worthy of serious investigation and research, and hence this article summarizes an important volume of research for a computational and software architecture perspective. This paper reviews the literature and discusses various aspects of evolutionary robotics including the application on morphological soft robots to allow self assembly, self reconfiguration, self repair, and self reproduction. Then, major milestones are outlined along with important morphological soft robotic prototypes due to their importance in the field. Finally, the current state of the art in the field is assessed.
Idiomatic and Reproducible Software Builds using Containers for Reliable Computing
Venue: arXiv cs.SE 2017
Year: 2017

Containers as the unit of application delivery are the 'next big thing' in the software development world. They enable developers to create an executable image containing an application bundled with all its dependencies which a user can run inside a controlled environment with virtualized resources. Complex workflows for business-critical applications and research environments require a high degree of reproducibility which can be accomplished using uniquely identified images as units of computation. It will be shown in this thesis that the most widely used approaches to create an image from pre-existing software or from source code lack the ability to provide idiomaticity in their use of the technology as well as proper reproducibility safe-guards. In the first part, existing approaches are formalized and discussed and a new approach is introduced. The approaches are then evaluated using a suite of three different examples. This thesis provides a framework for formalizing operations involving a layered file system, containers and images, and a novel approach to the creation of images using utility containers and layer donning fulfilling the idiomaticity and reproducibility criteria.
Finer-grained Locking in Concurrent Dynamic Planar Convex Hulls
Venue: arXiv cs.DC 2017
Year: 2017

The convex hull of a planar point set is the smallest convex polygon containing each point in the set. The dynamic convex hull problem concerns efficiently maintaining the convex hull of a set of points subject to additions and removals. One algorithm for this problem uses two external balanced binary search trees (BSTs) (M. H. Overmars, J. van Leeuwen 1981). We present the first concurrent solution for this problem, which uses a single BST that stores references to intermediate convex hull solutions at each node. We implement and evaluate two lock-based approaches: a) fine-grained locking, where each node of the tree is protected by a lock, and b) "finer-grained locking", where each node contains a separate lock for each of the left and right chains. In our throughput experiments, we observe that finer-grained locking yields an 8-60% improvement over fine-grained locking, and a 38-61x improvement over coarsegrained locking and software transactional memory (STM). When applied to find the convex hull of static point sets, our approach outperforms a parallel divide-and-conquer implementation by 2-4x using an equivalent number of threads.
UsingWord Embedding for Cross-Language Plagiarism Detection
Venue: arXiv cs.CL 2017
Year: 2017

This paper proposes to use distributed representation of words (word embeddings) in cross-language textual similarity detection. The main contributions of this paper are the following: (a) we introduce new cross-language similarity detection methods based on distributed representation of words; (b) we combine the different methods proposed to verify their complementarity and finally obtain an overall F1 score of 89.15% for English-French similarity detection at chunk level (88.5% at sentence level) on a very challenging corpus.
An Approach to Controller Design Based on the Generalized Cloud Model
Venue: arXiv cs.SY 2017
Year: 2017

In this paper, an approach to controller design based on the cloud models, without using the analog plant model is presented.