OpenRaiser/Intern-Atlas huggingface dataset:
Automatic Inference of Specifications in the K Framework
Venue: arXiv cs.PL 2015
Year: 2015

Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this paper we propose a technique for automatically discovering specifications from real code. The proposed methodology relies on the symbolic execution capabilities recently provided by the K framework that we exploit to automatically infer formal specifications from programs that are written in a non-trivial fragment of C, called KernelC. Roughly speaking, our symbolic analysis of KernelC programs explains the execution of a (modifier) function by using other (observer) routines in the program. We implemented our technique in the automated tool Kindspec 2.0, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures (i.e., result values and state change). We describe the implementation of our system and discuss the differences w.r.t. our previous work on inferring specifications from C code.
Two-faced processes and random number generators
Venue: arXiv cs.IT 2015
Year: 2015

We describe random processes (with binary alphabet) whose entropy is less than 1 (per letter), but they mimic true random process, i.e., by definition, generated sequence can be interpreted as the result of the flips of a fair coin with sides that are labeled 0 and 1. It gives a possibility to construct Random Number Generators which possess theoretical guarantees. This, in turn, is important for applications such as those in cryptography.
Multi-Instance Visual-Semantic Embedding
Venue: arXiv cs.CV 2015
Year: 2015

Visual-semantic embedding models have been recently proposed and shown to be effective for image classification and zero-shot learning, by mapping images into a continuous semantic label space. Although several approaches have been proposed for single-label embedding tasks, handling images with multiple labels (which is a more general setting) still remains an open problem, mainly due to the complex underlying corresponding relationship between image and its labels. In this work, we present Multi-Instance visual-semantic Embedding model (MIE) for embedding images associated with either single or multiple labels. Our model discovers and maps semantically-meaningful image subregions to their corresponding labels. And we demonstrate the superiority of our method over the state-of-the-art on two tasks, including multi-label image annotation and zero-shot learning.
The risk of divergence
Venue: arXiv cs.GT 2015
Year: 2015

We present infinite extensive strategy profiles with perfect information and we show that replacing finite by infinite changes the notions and the reasoning tools. The presentation uses a formalism recently developed by logicians and computer science theoreticians, called coinduction. This builds a bridge between economic game theory and the most recent advance in theoretical computer science and logic. The key result is that rational agents may have strategy leading to divergence .
Conflict Solution According to "Aggressiveness" of Agents in Floor-Field-Based Model
Venue: arXiv cs.MA 2015
Year: 2015

This contribution introduces an element of "aggressiveness" into the Floor-Field based model with adaptive time-span. The aggressiveness is understood as an ability to win conflicts and push through the crowd. From experiments it is observed that this ability is not directly correlated with the desired velocity in the free flow regime. The influence of the aggressiveness is studied by means of the dependence of the travel time on the occupancy of a room. A simulation study shows that the conflict solution based on the aggressiveness parameter can mimic the observations from the experiment.
Plug-and-Play Priors for Bright Field Electron Tomography and Sparse Interpolation
Venue: arXiv cs.CV 2015
Year: 2015

Many material and biological samples in scientific imaging are characterized by non-local repeating structures. These are studied using scanning electron microscopy and electron tomography. Sparse sampling of individual pixels in a 2D image acquisition geometry, or sparse sampling of projection images with large tilt increments in a tomography experiment, can enable high speed data acquisition and minimize sample damage caused by the electron beam. In this paper, we present an algorithm for electron tomographic reconstruction and sparse image interpolation that exploits the non-local redundancy in images. We adapt a framework, termed plug-and-play (P&P) priors, to solve these imaging problems in a regularized inversion setting. The power of the P&P approach is that it allows a wide array of modern denoising algorithms to be used as a "prior model" for tomography and image interpolation. We also present sufficient mathematical conditions that ensure convergence of the P&P approach, and we use these insights to design a new non-local means denoising algorithm. Finally, we demonstrate that the algorithm produces higher quality reconstructions on both simulated and real electron microscope data, along with improved convergence properties compared to other methods.
A Deep Generative Deconvolutional Image Model
Venue: arXiv cs.CV 2015
Year: 2015

A deep generative model is developed for representation and analysis of images, based on a hierarchical convolutional dictionary-learning framework. Stochastic {\em unpooling} is employed to link consecutive layers in the model, yielding top-down image generation. A Bayesian support vector machine is linked to the top-layer features, yielding max-margin discrimination. Deep deconvolutional inference is employed when testing, to infer the latent features, and the top-layer features are connected with the max-margin classifier for discrimination tasks. The model is efficiently trained using a Monte Carlo expectation-maximization (MCEM) algorithm, with implementation on graphical processor units (GPUs) for efficient large-scale learning, and fast testing. Excellent results are obtained on several benchmark datasets, including ImageNet, demonstrating that the proposed model achieves results that are highly competitive with similarly sized convolutional neural networks.
Exploiting Hierarchy for Ranking-based Recommendation
Venue: arXiv cs.IR 2015
Year: 2015

The purpose of this master's thesis is to study and develop a new algorithmic framework for collaborative filtering (CF) to generate recommendations. The method we propose is based on the exploitation of the hierarchical structure of the item space and intuitively "stands" on the property of Near Complete Decomposability (NCD) which is inherent in the structure of the majority of hierarchical systems. Building on the intuition behind the NCDawareRank algorithm and its related concept of NCD proximity, we model our system in a way that illuminates its endemic characteristics and we propose a new algorithmic framework for recommendations, called HIR. We focus on combining the direct with the NCD "neighborhoods" of items to achieve better characterization of the inter-item relations, in order to improve the quality of recommendations and alleviate sparsity related problems.
Evaluation-as-a-Service: Overview and Outlook
Venue: arXiv cs.CY 2015
Year: 2015

Evaluation in empirical computer science is essential to show progress and assess technologies developed. Several research domains such as information retrieval have long relied on systematic evaluation to measure progress: here, the Cranfield paradigm of creating shared test collections, defining search tasks, and collecting ground truth for these tasks has persisted up until now. In recent years, however, several new challenges have emerged that do not fit this paradigm very well: extremely large data sets, confidential data sets as found in the medical domain, and rapidly changing data sets as often encountered in industry. Also, crowdsourcing has changed the way that industry approaches problem-solving with companies now organizing challenges and handing out monetary awards to incentivize people to work on their challenges, particularly in the field of machine learning. This white paper is based on discussions at a workshop on Evaluation-as-a-Service (EaaS). EaaS is the paradigm of not providing data sets to participants and have them work on the data locally, but keeping the data central and allowing access via Application Programming Interfaces (API), Virtual Machines (VM) or other possibilities to ship executables. The objective of this white paper are to summarize and compare the current approaches and consolidate the experiences of these approaches to outline the next steps of EaaS, particularly towards sustainable research infrastructures. This white paper summarizes several existing approaches to EaaS and analyzes their usage scenarios and also the advantages and disadvantages. The many factors influencing EaaS are overviewed, and the environment in terms of motivations for the various stakeholders, from funding agencies to challenge organizers, researchers and participants, to industry interested in supplying real-world problems for which they require solutions.
Fast and compact self-stabilizing verification, computation, and fault detection of an MST
Venue: arXiv cs.DC 2015
Year: 2015

This paper demonstrates the usefulness of distributed local verification of proofs, as a tool for the design of self-stabilizing algorithms.In particular, it introduces a somewhat generalized notion of distributed local proofs, and utilizes it for improving the time complexity significantly, while maintaining space optimality. As a result, we show that optimizing the memory size carries at most a small cost in terms of time, in the context of Minimum Spanning Tree (MST). That is, we present algorithms that are both time and space efficient for both constructing an MST and for verifying it.This involves several parts that may be considered contributions in themselves.First, we generalize the notion of local proofs, trading off the time complexity for memory efficiency. This adds a dimension to the study of distributed local proofs, which has been gaining attention recently. Specifically, we design a (self-stabilizing) proof labeling scheme which is memory optimal (i.e., $O(\log n)$ bits per node), and whose time complexity is $O(\log ^2 n)$ in synchronous networks, or $O(Δ\log ^3 n)$ time in asynchronous ones, where $Δ$ is the maximum degree of nodes. This answers an open problem posed by Awerbuch and Varghese (FOCS 1991). We also show that $Ω(\log n)$ time is necessary, even in synchronous networks. Another property is that if $f$ faults occurred, then, within the requireddetection time above, they are detected by some node in the $O(f\log n)$ locality of each of the faults.Second, we show how to enhance a known transformer that makes input/output algorithms self-stabilizing. It now takes as input an efficient construction algorithm and an efficient self-stabilizing proof labeling scheme, and produces an efficient self-stabilizing algorithm. When used for MST, the transformer produces a memory optimal self-stabilizing algorithm, whose time complexity, namely, $O(n)$, is significantly better even than that of previous algorithms. (The time complexity of previous MST algorithms that used $Ω(\log^2 n)$ memory bits per node was $O(n^2)$, and the time for optimal space algorithms was $O(n|E|)$.) Inherited from our proof labelling scheme, our self-stabilising MST construction algorithm also has the following two properties: (1) if faults occur after the construction ended, then they are detected by some nodes within $O(\log ^2 n)$ time in synchronous networks, or within $O(Δ\log ^3 n)$ time in asynchronous ones, and (2) if $f$ faults occurred, then, within the required detection time above, they are detected within the $O(f\log n)$ locality of each of the faults. We also show how to improve the above two properties, at the expense of some increase in the memory.
PersisDroid: Android Performance Diagnosis via Anatomizing Asynchronous Executions
Venue: arXiv cs.SE 2015
Year: 2015

Android applications (apps) grow dramatically in recent years. Apps are user interface (UI) centric typically. Rapid UI responsiveness is key consideration to app developers. However, we still lack a handy tool for profiling app performance so as to diagnose performance problems. This paper presents PersisDroid, a tool specifically designed for this task. The key notion of PersisDroid is that the UI-triggered asynchronous executions also contribute to the UI performance, and hence its performance should be properly captured to facilitate performance diagnosis. However, Android allows tremendous ways to start the asynchronous executions, posing a great challenge to profiling such execution. This paper finds that they can be grouped into six categories. As a result, they can be tracked and profiled according to the specifics of each category with a dynamic instrumentation approach carefully tailored for Android. PersisDroid can then properly profile the asynchronous executions in task granularity, which equips it with low-overhead and high compatibility merits. Most importantly, the profiling data can greatly help the developers in detecting and locating performance anomalies. We code and open-source release PersisDroid. The tool is applied in diagnosing 20 open-source apps, and we find 11 of them contain potential performance problems, which shows its effectiveness in performance diagnosis for Android apps.
Campaigning in Heterogeneous Social Networks: Optimal Control of SI Information Epidemics
Venue: arXiv cs.SI 2015
Year: 2015

We study the optimal control problem of maximizing the spread of an information epidemic on a social network. Information propagation is modeled as a Susceptible-Infected (SI) process and the campaign budget is fixed. Direct recruitment and word-of-mouth incentives are the two strategies to accelerate information spreading (controls). We allow for multiple controls depending on the degree of the nodes/individuals. The solution optimally allocates the scarce resource over the campaign duration and the degree class groups. We study the impact of the degree distribution of the network on the controls and present results for Erdos-Renyi and scale free networks. Results show that more resource is allocated to high degree nodes in the case of scale free networks but medium degree nodes in the case of Erdos-Renyi networks. We study the effects of various model parameters on the optimal strategy and quantify the improvement offered by the optimal strategy over the static and bang-bang control strategies. The effect of the time varying spreading rate on the controls is explored as the interest level of the population in the subject of the campaign may change over time. We show the existence of a solution to the formulated optimal control problem, which has non-linear isoperimetric constraints, using novel techniques that is general and can be used in other similar optimal control problems. This work may be of interest to political, social awareness, or crowdfunding campaigners and product marketing managers, and with some modifications may be used for mitigating biological epidemics.
Assessment of texture measures susceptibility to noise in conventional and contrast enhanced computed tomography lung tumour images
Venue: arXiv cs.CV 2015
Year: 2015

Noise is one of the major problems that hinder an effective texture analysis of disease in medical images, which may cause variability in the reported diagnosis. In this paper seven texture measurement methods (two wavelet, two model and three statistical based) were applied to investigate their susceptibility to subtle noise caused by acquisition and reconstruction deficiencies in computed tomography (CT) images. Features of lung tumours were extracted from two different conventional and contrast enhanced CT image data-sets under filtered and noisy conditions. When measuring the noise in the background open-air region of the analysed CT images, noise of Gaussian and Rayleigh distributions with varying mean and variance was encountered, and Fisher distance was used to differentiate between an original extracted lung tumour region of interest (ROI) with the filtered and noisy reconstructed versions. It was determined that the wavelet packet (WP) and fractal dimension measures were the least affected, while the Gaussian Markov random field, run-length and co-occurrence matrices were the most affected by noise. Depending on the selected ROI size, it was concluded that texture measures with fewer extracted features can decrease susceptibility to noise, with the WP and the Gabor filter having a stable performance in both filtered and noisy CT versions and for both data-sets. Knowing how robust each texture measure under noise presence is can assist physicians using an automated lung texture classification system in choosing the appropriate feature extraction algorithm for a more accurate diagnosis.
Data Driven Robust Image Guided Depth Map Restoration
Venue: arXiv cs.CV 2015
Year: 2015

Depth maps captured by modern depth cameras such as Kinect and Time-of-Flight (ToF) are usually contaminated by missing data, noises and suffer from being of low resolution. In this paper, we present a robust method for high-quality restoration of a degraded depth map with the guidance of the corresponding color image. We solve the problem in an energy optimization framework that consists of a novel robust data term and smoothness term. To accommodate not only the noise but also the inconsistency between depth discontinuities and the color edges, we model both the data term and smoothness term with a robust exponential error norm function. We propose to use Iteratively Re-weighted Least Squares (IRLS) methods for efficiently solving the resulting highly non-convex optimization problem. More importantly, we further develop a data-driven adaptive parameter selection scheme to properly determine the parameter in the model. We show that the proposed approach can preserve fine details and sharp depth discontinuities even for a large upsampling factor ($8\times$ for example). Experimental results on both simulated and real datasets demonstrate that the proposed method outperforms recent state-of-the-art methods in coping with the heavy noise, preserving sharp depth discontinuities and suppressing the texture copy artifacts.
Eventual Wait-Free Synchronization
Venue: arXiv cs.DC 2015
Year: 2015

Eventually linearizable objects are novel shared memory programming constructs introduced as an analogy to eventual consistency in message-passing systems. However, their behaviors in shared memory systems are so mysterious that very little general theoretical properties of them is known. In this paper, we lay the theoretical foundation of the study of eventually linearizable objects. We prove that the n-process eventually linearizable fetch-and-cons (n-FAC) object is universal and can be used to classify the eventually linearizable objects. In particular, we define the concept of eventual consensus number of an abstract data type and prove that the eventual consensus number can be used as a good characterization of the synchronization power of eventual objects. Thus we got a complete hierarchy of eventually linearizable objects, as a perfect analogy of the consensus hierarchy. In this way, the synchronization power of eventual linearizability become much more well understood.
Guarding the Vertices of an Orthogonal Terrain using Vertex Guards
Venue: arXiv cs.CG 2015
Year: 2015

A terrain T is an x-monotone polygonal chain in the plane; T is orthogonal if each edge of T is either horizontal or vertical. In this paper, we give an exact algorithm for the problem of guarding the convex vertices of an orthogonal terrain with the minimum number of reflex vertices.
Non-Asymptotic Delay Bounds for (k,l) Fork-Join Systems and Multi-Stage Fork-Join Networks
Venue: arXiv cs.PF 2015
Year: 2015

Parallel systems have received increasing attention with numerous recent applications such as fork-join systems, load-balancing, and l-out-of-k redundancy. Common to these systems is a join or resequencing stage, where tasks that have finished service may have to wait for the completion of other tasks so that they leave the system in a predefined order. These synchronization constraints make the analysis of parallel systems challenging and few explicit results are known. In this work, we model parallel systems using a max-plus approach that enables us to derive statistical bounds of waiting and sojourn times. Taking advantage of max-plus system theory, we also show end-to-end delay bounds for multi-stage fork-join networks. We contribute solutions for basic G|G|1 fork-join systems, parallel systems with load-balancing, as well as general (k,l) fork-join systems with redundancy. Our results provide insights into the respective advantages of l-out-of-k redundancy vs. load-balancing.
Data Migration among Different Clouds
Venue: arXiv cs.DC 2015
Year: 2015

Cloud computing services are becoming more and more popular. However, the high concentration of data and services on the clouds make them attractive targets for various security attacks, including DoS, data theft, and privacy attacks. Additionally, cloud providers may fail to comply with service level agreement in terms of performance, availability, and security guarantees. Moreover, users may choose to utilize public cloud services from multiple vendors for various reasons including fault tolerance and availability. Therefore, it is of paramount importance to have secure and efficient mechanisms that enable users to transparently copy and move their data from one provider to another. In this paper, we explore the state of the art inter cloud migration techniques and identify the potential security threats in the scope of Hadoop Distributed File System HDFS. We propose an inter cloud data migration mechanism that offers better security guarantees and faster response time for migrating large scale data files in cloud database management systems. The proposed approach enhances the data security processes used to achieve secure data migration between cloud nodes thus improves applications response time and throughput. The performance of the proposed approach is validated by measuring its impact on response time and throughput, and comparing the performance to that of other techniques in the literature.
Outlier Detection In Large-scale Traffic Data By Naïve Bayes Method and Gaussian Mixture Model Method
Venue: arXiv cs.CV 2015
Year: 2015

It is meaningful to detect outliers in traffic data for traffic management. However, this is a massive task for people from large-scale database to distinguish outliers. In this paper, we present two methods: Kernel Smoothing Naïve Bayes (NB) method and Gaussian Mixture Model (GMM) method to automatically detect any hardware errors as well as abnormal traffic events in traffic data collected at a four-arm junction in Hong Kong. Traffic data was recorded in a video format, and converted to spatial-temporal (ST) traffic signals by statistics. The ST signals are then projected to a two-dimensional (2D) (x,y)-coordinate plane by Principal Component Analysis (PCA) for dimension reduction. We assume that inlier data are normal distributed. As such, the NB and GMM methods are successfully applied in outlier detection (OD) for traffic data. The kernel smooth NB method assumes the existence of kernel distributions in traffic data and uses Bayes' Theorem to perform OD. In contrast, the GMM method believes the traffic data is formed by the mixture of Gaussian distributions and exploits confidence region for OD. This paper would address the modeling of each method and evaluate their respective performances. Experimental results show that the NB algorithm with Triangle kernel and GMM method achieve up to 93.78% and 94.50% accuracies, respectively.