OpenRaiser/Intern-Atlas huggingface dataset:
DroidLink: Automated Generation of Deep Links for Android Apps
Venue: arXiv cs.SE 2016
Year: 2016

The mobile application (app) has become the main entrance to access the Internet on handheld devices. Unlike the Web where each webpage has a global URL to reach directly, a specific "content page" of an app can be opened only by exploring the app with several operations from the landing page. The interoperability between apps is quite fixed and thus limits the value-added "linked data" between apps. Recently, deep link has been proposed to enable targeting and opening a specific page of an app externally with an accessible uniform resource identifier (URI). However, implementing deep link for mobile apps requires a lot of manual efforts by app developers, which can be very error-prone and time-consuming. In this paper, we propose DroidLink to automatically generating deep links for existing Android apps. We design a deep link model suitable for automatic generation. Then we explore the transition of pages and build a navigation graph based on static and dynamic analysis of Android apps. Next, we realize an updating mechanism that keeps on revisiting the target app and discover new pages, and thus generates deep links for every single page of the app. Finally, we repackage the app with deep link supports, but requires no additional deployment requirements. We generate deep links for some popular apps and demonstrate the feasibility of DroidLink.
No value restriction is needed for algebraic effects and handlers
Venue: arXiv cs.PL 2016
Year: 2016

We present a straightforward, sound Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which allows type variable generalisation of arbitrary computations, not just values. This result is surprising. On the one hand, the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations. On the other hand, many programming examples can be recast to use effect handlers instead of these effects. Analysing the expressive power of effect handlers with respect to state effects, we claim handlers cannot express reference cells, and show they can simulate dynamically scoped state.
Extracting Higher-Order Goals from the Mizar Mathematical Library
Venue: arXiv cs.LO 2016
Year: 2016

Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theorem proving problems from Mizar articles that make use of these constructs. In particular, higher-order logic is used to represent schemes, a global choice construct and set level binders. The higher-order automated theorem provers Satallax and LEO-II have been run on collections of these problems and the results are discussed.
Phase retrieval from multiple-window short-time Fourier measurements
Venue: arXiv cs.IT 2016
Year: 2016

In this paper, we introduce two symmetric directed graphs depending on supports of signals and windows, and we show that the connectivity of those graphs provides either necessary and sufficient conditions to phase retrieval of a signal from magnitude measurements of its multiple-window short-time Fourier transform. Also we propose an algebraic reconstruction algorithm, and provide an error estimate to our algorithm when magnitude measurements are corrupted by deterministic/random noises.
A Free Energy Foundation of Semantic Similarity in Automata and Languages
Venue: arXiv cs.FL 2016
Year: 2016

This paper develops a free energy theory from physics including the variational principles for automata and languages and also provides algorithms to compute the energy as well as efficient algorithms for estimating the nondeterminism in a nondeterministic finite automaton. This theory is then used as a foundation to define a semantic similarity metric for automata and languages. Since automata are a fundamental model for all modern programs while languages are a fundamental model for the programs' behaviors, we believe that the theory and the metric developed in this paper can be further used for real-word programs as well.
Dense CNN Learning with Equivalent Mappings
Venue: arXiv cs.CV 2016
Year: 2016

Large receptive field and dense prediction are both important for achieving high accuracy in pixel labeling tasks such as semantic segmentation. These two properties, however, contradict with each other. A pooling layer (with stride 2) quadruples the receptive field size but reduces the number of predictions to 25\%. Some existing methods lead to dense predictions using computations that are not equivalent to the original model. In this paper, we propose the equivalent convolution (eConv) and equivalent pooling (ePool) layers, leading to predictions that are both dense and equivalent to the baseline CNN model. Dense prediction models learned using eConv and ePool can transfer the baseline CNN's parameters as a starting point, and can inverse transfer the learned parameters in a dense model back to the original one, which has both fast testing speed and high accuracy. The proposed eConv and ePool layers have achieved higher accuracy than baseline CNN in various tasks, including semantic segmentation, object localization, image categorization and apparent age estimation, not only in those tasks requiring dense pixel labeling.
Deterministic Time-Space Tradeoffs for k-SUM
Venue: arXiv cs.DS 2016
Year: 2016

Given a set of numbers, the $k$-SUM problem asks for a subset of $k$ numbers that sums to zero. When the numbers are integers, the time and space complexity of $k$-SUM is generally studied in the word-RAM model; when the numbers are reals, the complexity is studied in the real-RAM model, and space is measured by the number of reals held in memory at any point. We present a time and space efficient deterministic self-reduction for the $k$-SUM problem which holds for both models, and has many interesting consequences. To illustrate: * $3$-SUM is in deterministic time $O(n^2 \lg\lg(n)/\lg(n))$ and space $O\left(\sqrt{\frac{n \lg(n)}{\lg\lg(n)}}\right)$. In general, any polylogarithmic-time improvement over quadratic time for $3$-SUM can be converted into an algorithm with an identical time improvement but low space complexity as well. * $3$-SUM is in deterministic time $O(n^2)$ and space $O(\sqrt n)$, derandomizing an algorithm of Wang. * A popular conjecture states that 3-SUM requires $n^{2-o(1)}$ time on the word-RAM. We show that the 3-SUM Conjecture is in fact equivalent to the (seemingly weaker) conjecture that every $O(n^{.51})$-space algorithm for $3$-SUM requires at least $n^{2-o(1)}$ time on the word-RAM. * For $k \ge 4$, $k$-SUM is in deterministic $O(n^{k - 2 + 2/k})$ time and $O(\sqrt{n})$ space.
Adaptive Beaconing Approaches for Vehicular ad hoc Networks: A Survey
Venue: arXiv cs.NI 2016
Year: 2016

Vehicular communication requires vehicles to self-organize through the exchange of periodic beacons. Recent analysis on beaconing indicates that the standards for beaconing restrict the desired performance of vehicular applications. This situation can be attributed to the quality of the available transmission medium, persistent change in the traffic situation and the inability of standards to cope with application requirements. To this end, this paper is motivated by the classifications and capability evaluations of existing adaptive beaconing approaches. To begin with, we explore the anatomy and the performance requirements of beaconing. Then, the beaconing design is analyzed to introduce a design-based beaconing taxonomy. A survey of the state-of-the-art is conducted with an emphasis on the salient features of the beaconing approaches. We also evaluate the capabilities of beaconing approaches using several key parameters. A comparison among beaconing approaches is presented, which is based on the architectural and implementation characteristics. The paper concludes by discussing open challenges in the field.
An Innovative, Open, Interoperable Citizen Engagement Cloud Platform for Smart Government and Users' Interaction
Venue: arXiv cs.CY 2016
Year: 2016

This paper introduces an open, interoperable, and cloud-computing-based citizen engagement platform for the management of administrative processes of public administrations, which also increases the engagement of citizens. The citizen engagement platform is the outcome of a 3-year Italian national project called PRISMA (Interoperable cloud platforms for smart government). The aim of the project is to constitute a new model of digital ecosystem that can support and enable new methods of interaction among public administrations, citizens, companies, and other stakeholders surrounding cities. The platform has been defined by the media as a flexible (enable the addition of any kind of application or service) and open (enable access to open services) Italian "cloud" that allows public administrations to access to a vast knowledge base represented as linked open data to be reused by a stakeholder community with the aim of developing new applications ("Cloud Apps") tailored to the specific needs of citizens. The platform has been used by Catania and Syracuse municipalities, two of the main cities of southern Italy, located in the Sicilian region. The fully adoption of the platform is rapidly spreading around the whole region (local developers have already used available application programming interfaces (APIs) to create additional services for citizens and administrations) to such an extent that other provinces of Sicily and Italy in general expressed their interest for its usage. The platform is available online and, as mentioned above, is open source and provides APIs for full exploitation.
Phase reconstruction of spectrograms with linear unwrapping: application to audio signal restoration
Venue: arXiv cs.SD 2016
Year: 2016

This paper introduces a novel technique for reconstructing the phase of modified spectrograms of audio signals. From the analysis of mixtures of sinusoids we obtain relationships between phases of successive time frames in the Time-Frequency (TF) domain. To obtain similar relationships over frequencies, in particular within onset frames, we study an impulse model. Instantaneous frequencies and attack times are estimated locally to encompass the class of non-stationary signals such as vibratos. These techniques ensure both the vertical coherence of partials (over frequencies) and the horizontal coherence (over time). The method is tested on a variety of data and demonstrates better performance than traditional consistency-based approaches. We also introduce an audio restoration framework and observe that our technique outperforms traditional methods.
Leveraging Over Priors for Boosting Control of Prosthetic Hands
Venue: arXiv cs.LG 2016
Year: 2016

The Electromyography (EMG) signal is the electrical activity produced by cells of skeletal muscles in order to provide a movement. The non-invasive prosthetic hand works with several electrodes, placed on the stump of an amputee, that record this signal. In order to favour the control of prosthesis, the EMG signal is analyzed with algorithms based on machine learning theory to decide the movement that the subject is going to do. In order to obtain a significant control of the prosthesis and avoid mismatch between desired and performed movements, a long training period is needed when we use the traditional algorithm of machine learning (i.e. Support Vector Machines). An actual challenge in this field concerns the reduction of the time necessary for an amputee to learn how to use the prosthesis. Recently, several algorithms that exploit a form of prior knowledge have been proposed. In general, we refer to prior knowledge as a past experience available in the form of models. In our case an amputee, that attempts to perform some movements with the prosthesis, could use experience from different subjects that are already able to perform those movements. The aim of this work is to verify, with a computational investigation, if for an amputee this kind of previous experience is useful in order to reduce the training time and boost the prosthetic control. Furthermore, we want to understand if and how the final results change when the previous knowledge of intact or amputated subjects is used for a new amputee. Our experiments indicate that: (1) the use of experience, from other subjects already trained to perform a task, makes us able to reduce the training time of about an order of magnitude; (2) it seems that an amputee that tries to learn to use the prosthesis doesn't reach different results when he/she exploits previous experience of amputees or intact.
Green Cloudlet Network: A Distributed Green Mobile Cloud Network
Venue: arXiv cs.NI 2016
Year: 2016

This article introduces a Green Cloudlet Network (GCN) architecture in the context of mobile cloud computing. The proposed architecture is aimed at providing seamless and low End-to-End (E2E) delay between a User Equipment (UE) and its Avatar (its software clone) in the cloudlets to facilitate the application workloads offloading process. Furthermore, Software Define Networking (SDN) based core network is introduced in the GCN architecture by replacing the traditional Evolved Packet Core (EPC) in the LTE network in order to provide efficient communications connections between different end points. Cloudlet Network File System (CNFS) is designed based on the proposed architecture in order to protect Avatars' dataset against hardware failure and improve the Avatars' performance in terms of data access latency. Moreover, green energy supplement is proposed in the architecture in order to reduce the extra Operational Expenditure (OPEX) and CO2 footprint incurred by running the distributed cloudlets. Owing to the temporal and spatial dynamics of both the green energy generation and energy demands of Green Cloudlet Systems (GCSs), designing an optimal green energy management strategy based on the characteristics of the green energy generation and the energy demands of eNBs and cloudlets to minimize the on-grid energy consumption is critical to the cloudlet provider.
AUTO2, a saturation-based heuristic prover for higher-order logic
Venue: arXiv cs.LO 2016
Year: 2016

We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle/HOL, and applied it to several formalization projects in mathematics and computer science, demonstrating the high level of automation it can provide in a variety of possible proof tasks.
Blind Analysis of CT Image Noise Using Residual Denoised Images
Venue: arXiv cs.CV 2016
Year: 2016

CT protocol design and quality control would benefit from automated tools to estimate the quality of generated CT images. These tools could be used to identify erroneous CT acquisitions or refine protocols to achieve certain signal to noise characteristics. This paper investigates blind estimation methods to determine global signal strength and noise levels in chest CT images. Methods: We propose novel performance metrics corresponding to the accuracy of noise and signal estimation. We implement and evaluate the noise estimation performance of six spatial- and frequency- based methods, derived from conventional image filtering algorithms. Algorithms were tested on patient data sets from whole-body repeat CT acquisitions performed with a higher and lower dose technique over the same scan region. Results: The proposed performance metrics can evaluate the relative tradeoff of filter parameters and noise estimation performance. The proposed automated methods tend to underestimate CT image noise at low-flux levels. Initial application of methodology suggests that anisotropic diffusion and Wavelet-transform based filters provide optimal estimates of noise. Furthermore, methodology does not provide accurate estimates of absolute noise levels, but can provide estimates of relative change and/or trends in noise levels.
Understanding Content Placement Strategies in Smartrouter-based Peer CDN for Video Streaming
Venue: arXiv cs.MM 2016
Year: 2016

Recent years have witnessed a new video delivery paradigm: smartrouter-based peer video content delivery network, which is enabled by smartrouters deployed at users' homes. ChinaCache (one of the largest CDN providers in China) and Youku (a video provider using smartrouters to assist video delivery) announced their cooperation in 2015, to create a new paradigm of content delivery based on householders' network resources. This new paradigm is different from the conventional peer-to-peer (P2P) approach, because millions of dedicated smartrouters are operated by the centralized video service providers in a coordinative manner. Thus it is intriguing to study the content placement strategies used in a smartrouter-based content delivery system, as well as its potential impact on the content delivery ecosystem. In this paper, we carry out measurement studies of Youku's peer video CDN, who has deployed over 300K smartrouter devices for its video delivery. In our measurement studies, 104K videos were investigated and 4TB traffic has been analyzed, over controlled smartrouter nodes and players. Our measurement insights are as follows. First, a global content replication strategy is essential for the peer CDN systems. Second, such peer CDN deployment itself can form an effective sub-system for end-to-end QoS monitoring, which can be used for fine-grained request redirection (e.g., user-level) and content replication. We also show our analysis on the performance limitations and propose potential improvements to the peer CDN systems.
Cooperative Tx/Rx Caching in Interference Channels: A Storage-Latency Tradeoff Study
Venue: arXiv cs.IT 2016
Year: 2016

This paper studies the storage-latency tradeoff in the $3\times3$ wireless interference network with caches equipped at all transmitters and receivers. The tradeoff is characterized by the so-called fractional delivery time (FDT) at given normalized transmitter and receiver cache sizes. We first propose a generic cooperative transmitter/receiver caching strategy with adjustable file splitting ratios. Based on this caching strategy, we then design the delivery phase carefully to turn the considered interference channel opportunistically into broadcast channel, multicast channel, X channel, or a hybrid form of these channels. After that, we obtain an achievable upper bound of the minimum FDT by solving a linear programming problem of the file splitting ratios. The achievable FDT is a convex and piece-wise linear decreasing function of the cache sizes. Receiver local caching gain, coded multicasting gain, and transmitter cooperation gain (interference alignment and interference neutralization) are leveraged in different cache size regions.
Improving energy efficiency and classification accuracy of neuromorphic chips by learning binary synaptic crossbars
Venue: arXiv cs.NE 2016
Year: 2016

Deep Neural Networks (DNN) have achieved human level performance in many image analytics tasks but DNNs are mostly deployed to GPU platforms that consume a considerable amount of power. Brain-inspired spiking neuromorphic chips consume low power and can be highly parallelized. However, for deploying DNNs to energy efficient neuromorphic chips the incompatibility between continuous neurons and synaptic weights of traditional DNNs, discrete spiking neurons and synapses of neuromorphic chips has to be overcome. Previous work has achieved this by training a network to learn continuous probabilities and deployment to a neuromorphic architecture by random sampling these probabilities. An ensemble of sampled networks is needed to approximate the performance of the trained network. In the work presented in this paper, we have extended previous research by directly learning binary synaptic crossbars. Results on MNIST show that better performance can be achieved with a small network in one time step (92.7% maximum observed accuracy vs 95.98% accuracy in our work). Top results on a larger network are similar to previously published results (99.42% maximum observed accuracy vs 99.45% accuracy in our work). More importantly, in our work a smaller ensemble is needed to achieve similar or better accuracy than previous work, which translates into significantly decreased energy consumption for both networks. Results of our work are stable since they do not require random sampling.
Using instantaneous frequency and aperiodicity detection to estimate F0 for high-quality speech synthesis
Venue: arXiv cs.SD 2016
Year: 2016

This paper introduces a general and flexible framework for F0 and aperiodicity (additive non periodic component) analysis, specifically intended for high-quality speech synthesis and modification applications. The proposed framework consists of three subsystems: instantaneous frequency estimator and initial aperiodicity detector, F0 trajectory tracker, and F0 refinement and aperiodicity extractor. A preliminary implementation of the proposed framework substantially outperformed (by a factor of 10 in terms of RMS F0 estimation error) existing F0 extractors in tracking ability of temporally varying F0 trajectories. The front end aperiodicity detector consists of a complex-valued wavelet analysis filter with a highly selective temporal and spectral envelope. This front end aperiodicity detector uses a new measure that quantifies the deviation from periodicity. The measure is less sensitive to slow FM and AM and closely correlates with the signal to noise ratio.
SS4MCT: A Statistical Stemmer for Morphologically Complex Texts
Venue: arXiv cs.IR 2016
Year: 2016

There have been multiple attempts to resolve various inflection matching problems in information retrieval. Stemming is a common approach to this end. Among many techniques for stemming, statistical stemming has been shown to be effective in a number of languages, particularly highly inflected languages. In this paper we propose a method for finding affixes in different positions of a word. Common statistical techniques heavily rely on string similarity in terms of prefix and suffix matching. Since infixes are common in irregular/informal inflections in morphologically complex texts, it is required to find infixes for stemming. In this paper we propose a method whose aim is to find statistical inflectional rules based on minimum edit distance table of word pairs and the likelihoods of the rules in a language. These rules are used to statistically stem words and can be used in different text mining tasks. Experimental results on CLEF 2008 and CLEF 2009 English-Persian CLIR tasks indicate that the proposed method significantly outperforms all the baselines in terms of MAP.
Constructing Data Graphs for Keyword Search
Venue: arXiv cs.DB 2016
Year: 2016

A data graph is a convenient paradigm for supporting keyword search that takes into account available semantic structure and not just textual relevance. However, the problem of constructing data graphs that facilitate both efficiency and effectiveness of the underlying system has hardly been addressed. A conceptual model for this task is proposed. Principles for constructing good data graphs are explained. Transformations for generating data graphs from RDB and XML are developed. The results obtained from these transformations are analyzed. It is shown that XML is a better starting point for getting a good data graph.