OpenRaiser/Intern-Atlas huggingface dataset:
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
Venue: arXiv cs.LO 2014
Year: 2014

Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking functions over mathematical integers. This class of functions is insufficient for proving termination of many terminating programs, and furthermore a termination argument for a program operating on mathematical integers does not always lead to a termination argument for the same program operating on fixed-width machine integers. We propose a termination analysis able to generate nonlinear, lexicographic ranking functions and nonlinear recurrence sets that are correct for fixed-width machine arithmetic and floating-point arithmetic Our technique is based on a reduction from program \emph{termination} to second-order \emph{satisfaction}. We provide formulations for termination and non-termination in a fragment of second-order logic with restricted quantification which is decidable over finite domains. The resulted technique is a sound and complete analysis for the termination of finite-state programs with fixed-width integers and IEEE floating-point arithmetic.
Fostering of innovative usability testing to develop mobile application for mobile collaborative learning (MCL)
Venue: arXiv cs.CY 2014
Year: 2014

Emergence of latest technologies has diverted the focus of people form Computer-Supported Collaborative Learning (CSCL) to mobile supported collaborative learning. MCL is highly demanded in educational organizations to substantiate the pedagogical activities. Some of the MCL supportive architectures including applications are introduced in several fields to improve the activities of those organizations, but they need more concise paradigm to support both types of collaboration: synchronous and asynchronous. This paper introduces the new preusability testing method that provides educational support and gives complete picture for developing new pedagogical group application for MCL. The feature of application includes asynchronous and synchronous collaboration support. To validate the features of application, we conduct the post usability testing and heuristic evaluation, which helps in collecting the empirical data to prove the effectiveness and suitability of Group application. Further, application aims to improve learning impact and educate people at anytime and anywhere.
On the Compound Broadcast Channel: Multiple Description Coding and Interference Decoding
Venue: arXiv cs.IT 2014
Year: 2014

This work investigates the general two-user Compound Broadcast Channel (BC) where an encoder wishes to transmit common and private messages to two receivers while being oblivious to two possible channel realizations controlling the communication. The focus is on the characterization of the largest achievable rate region by resorting to more evolved encoding and decoding techniques than the conventional coding for the standard BC. The role of the decoder is first explored, and an achievable rate region is derived based on the principle of "Interference Decoding" (ID) where each receiver decodes its intended message and chooses to (non-uniquely) decode or not the interfering message. This inner bound is shown to be capacity achieving for a class of non-trivial compound BEC/BSC broadcast channels while the worst-case of Marton's inner bound -based on "Non Interference Decoding" (NID)- fails to achieve the capacity region. The role of the encoder is then studied, and an achievable rate region is derived based on "Multiple Description" (MD) coding where the encoder transmits a common as well as multiple dedicated private descriptions to the many instances of the users channels. It turns out that MD coding outperforms the single description scheme -Common Description (CD) coding- for a class of compound Multiple Input Single Output Broadcast Channels (MISO BC).
The field of the Reals and the Random Graph are not Finite-Word Ordinal-Automatic
Venue: arXiv cs.FL 2014
Year: 2014

Recently, Schlicht and Stephan lifted the notion of automatic-structures to the notion of (finite-word) ordinal-automatic structures. These are structures whose domain and relations can be represented by automata reading finite words whose shape is some fixed ordinal $α$. We lift Delhommé's relative-growth-technique from the automatic and tree-automatic setting to the ordinal-automatic setting. This result implies that the random graph is not ordinal-automatic and infinite integral domains are not ordinal-automatic with respect to ordinals below $ω_1+ω^ω$ where $ω_1$ is the first uncountable ordinal.
Interactive Error Correction in Implicative Theories
Venue: arXiv cs.AI 2014
Year: 2014

Errors in implicative theories coming from binary data are studied. First, two classes of errors that may affect implicative theories are singled out. Two approaches for finding errors of these classes are proposed, both of them based on methods of Formal Concept Analysis. The first approach uses the cardinality minimal (canonical or Duquenne-Guigues) implication base. The construction of such a base is computationally intractable. Using an alternative approach one checks possible errors on the fly in polynomial time via computing closures of subsets of attributes. Both approaches are interactive, based on questions about the validity of certain implications. Results of computer experiments are presented and discussed.
Learning to Rank Binary Codes
Venue: arXiv cs.CV 2014
Year: 2014

Binary codes have been widely used in vision problems as a compact feature representation to achieve both space and time advantages. Various methods have been proposed to learn data-dependent hash functions which map a feature vector to a binary code. However, considerable data information is inevitably lost during the binarization step which also causes ambiguity in measuring sample similarity using Hamming distance. Besides, the learned hash functions cannot be changed after training, which makes them incapable of adapting to new data outside the training data set. To address both issues, in this paper we propose a flexible bitwise weight learning framework based on the binary codes obtained by state-of-the-art hashing methods, and incorporate the learned weights into the weighted Hamming distance computation. We then formulate the proposed framework as a ranking problem and leverage the Ranking SVM model to offline tackle the weight learning. The framework is further extended to an online mode which updates the weights at each time new data comes, thereby making it scalable to large and dynamic data sets. Extensive experimental results demonstrate significant performance gains of using binary codes with bitwise weighting in image retrieval tasks. It is appealing that the online weight learning leads to comparable accuracy with its offline counterpart, which thus makes our approach practical for realistic applications.
Where do goals come from? A Generic Approach to Autonomous Goal-System Development
Venue: arXiv cs.LG 2014
Year: 2014

Goals express agents' intentions and allow them to organize their behavior based on low-dimensional abstractions of high-dimensional world states. How can agents develop such goals autonomously? This paper proposes a detailed conceptual and computational account to this longstanding problem. We argue to consider goals as high-level abstractions of lower-level intention mechanisms such as rewards and values, and point out that goals need to be considered alongside with a detection of the own actions' effects. We propose Latent Goal Analysis as a computational learning formulation thereof, and show constructively that any reward or value function can by explained by goals and such self-detection as latent mechanisms. We first show that learned goals provide a highly effective dimensionality reduction in a practical reinforcement learning problem. Then, we investigate a developmental scenario in which entirely task-unspecific rewards induced by visual saliency lead to self and goal representations that constitute goal-directed reaching.
Optimal randomized incremental construction for guaranteed logarithmic planar point location
Venue: arXiv cs.CG 2014
Year: 2014

Given a planar map of $n$ segments in which we wish to efficiently locate points, we present the first randomized incremental construction of the well-known trapezoidal-map search-structure that only requires expected $O(n \log n)$ preprocessing time while deterministically guaranteeing worst-case linear storage space and worst-case logarithmic query time. This settles a long standing open problem; the best previously known construction time of such a structure, which is based on a directed acyclic graph, so-called the history DAG, and with the above worst-case space and query-time guarantees, was expected $O(n \log^2 n)$. The result is based on a deeper understanding of the structure of the history DAG, its depth in relation to the length of its longest search path, as well as its correspondence to the trapezoidal search tree. Our results immediately extend to planar maps induced by finite collections of pairwise interior disjoint well-behaved curves.
The Unreasonable Effectiveness of Blood Pressure Measurement: Molecular Communication in Biological Systems
Venue: arXiv cs.IT 2014
Year: 2014

Arterial blood pressure is a key vital sign for the health of the human body. As such, accurate and reproducible measurement techniques are necessary for successful diagnosis. Blood pressure measurement is an example of molecular communication in regulated biological systems. In general, communication in regulated biological systems is difficult because the act of encoding information about the state of the system can corrupt the message itself. In this paper, we propose three strategies to cope with this problem to facilitate reliable molecular communication links: communicate from the outskirts; build it in; and leave a small footprint. Our strategies---inspired by communication in natural biological systems---provide a classification to guide the design of molecular communication mechanisms in synthetic biological systems. We illustrate our classification using examples of the first two strategies in natural systems. We then consider a molecular link within a model based on the Michaelis-Menten kinetics. In particular, we compute the capacity of the link, which reveals the potential of communicating using our leave a small footprint strategy. This provides a way of identifying whether the molecular link can be improved without affecting the function, and a guide to the design of synthetic biological systems.
Methods for the generation of normalized citation impact scores in bibliometrics: Which method best reflects the judgements of experts?
Venue: arXiv cs.DL 2014
Year: 2014

Evaluative bibliometrics compares the citation impact of researchers, research groups and institutions with each other across time scales and disciplines. Both factors - discipline and period - have an influence on the citation count which is independent of the quality of the publication. Normalizing the citation impact of papers for these two factors started in the mid-1980s. Since then, a range of different methods have been presented for producing normalized citation impact scores. The current study uses a data set of over 50,000 records to test which of the methods so far presented correlate better with the assessment of papers by peers. The peer assessments come from F1000Prime - a post-publication peer review system of the biomedical literature. Of the normalized indicators, the current study involves not only cited-side indicators, such as the mean normalized citation score, but also citing-side indicators. As the results show, the correlations of the indicators with the peer assessments all turn out to be very similar. Since F1000 focuses on biomedicine, it is important that the results of this study are validated by other studies based on datasets from other disciplines or (ideally) based on multi-disciplinary datasets.
Optimal Feature Selection from VMware ESXi 5.1 Feature Set
Venue: arXiv cs.DC 2014
Year: 2014

A study of VMware ESXi 5.1 server has been carried out to find the optimal set of parameters which suggest usage of different resources of the server. Feature selection algorithms have been used to extract the optimum set of parameters of the data obtained from VMware ESXi 5.1 server using esxtop command. Multiple virtual machines (VMs) are running in the mentioned server. K-means algorithm is used for clustering the VMs. The goodness of each cluster is determined by Davies Bouldin index and Dunn index respectively. The best cluster is further identified by the determined indices. The features of the best cluster are considered into a set of optimal parameters.
Zig-Zag Numberlink is NP-Complete
Venue: arXiv cs.CC 2014
Year: 2014

When can $t$ terminal pairs in an $m \times n$ grid be connected by $t$ vertex-disjoint paths that cover all vertices of the grid? We prove that this problem is NP-complete. Our hardness result can be compared to two previous NP-hardness proofs: Lynch's 1975 proof without the ``cover all vertices'' constraint, and Kotsuma and Takenaga's 2010 proof when the paths are restricted to have the fewest possible corners within their homotopy class. The latter restriction is a common form of the famous Nikoli puzzle \emph{Numberlink}; our problem is another common form of Numberlink, sometimes called \emph{Zig-Zag Numberlink} and popularized by the smartphone app \emph{Flow Free}.
Replacing the computer mouse
Venue: arXiv cs.HC 2014
Year: 2014

In a few months the computer mouse will be half-a-century-old. It is known to have many drawbacks, the main ones being: loss of productivity due to constant switching between keyboard and mouse, and health issues such as RSI. Like the keyboard, it is an unnatural human-computer interface. However the vast majority of computer users still use computer mice nowadays. In this article, we explore computer mouse alternatives. Our research shows that moving the mouse cursor can be done efficiently with camera-based head tracking system such as the SmartNav device, and mouse clicks can be emulated in many complementary ways. We believe that computer users can increase their productivity and improve their long-term health by using these alternatives.
An Improved UGS Scheduling with QoE Metrics in WiMAX Network
Venue: arXiv cs.NI 2014
Year: 2014

WiMAX (Worldwide Interoperability for Microwave Access) technology has emerged in response to the increasing demand for multimedia services in the internet broadband networks. WiMAX standard has defined five different scheduling services to meet the QoS (Quality of Service) requirement of multimedia applications and this paper investigates one specific scheduling service, i.e. UGS scheduling. In parallel, it was observed that in the difference of the traditional quality assessment approaches, nowadays, current researches are centered on the user perception of the quality, the existing scheduling approaches take into account the QoS, mobility and many other parameters, but do not consider the Quality of Experience (QoE). In order to control the packet transmission rate so as to match with the minimum subjective rate requirements of each user and therefore reduce packet loss and delays, an efficient scheduling approach has been proposed in this paper. The solution has been implemented and evaluated in the WiMAX simulation platform developed based on NS-2. Simulation results show that by applying various levels of MOS (Mean Opinion Score) the QoE provided to the users is enhanced in term of jitter, packet loss rate, throughput and delay.
A unified approach to linear probing hashing with buckets
Venue: arXiv cs.DS 2014
Year: 2014

We give a unified analysis of linear probing hashing with a general bucket size. We use both a combinatorial approach, giving exact formulas for generating functions, and a probabilistic approach, giving simple derivations of asymptotic results. Both approaches complement nicely, and give a good insight in the relation between linear probing and random walks. A key methodological contribution, at the core of Analytic Combinatorics, is the use of the symbolic method (based on q-calculus) to directly derive the generating functions to analyze.
Posimodular Function Optimization
Venue: arXiv cs.DS 2014
Year: 2014

Given a posimodular function $f: 2^V \to \mathbb{R}$ on a finite set $V$, we consider the problem of finding a nonempty subset $X$ of $V$ that minimizes $f(X)$. Posimodular functions often arise in combinatorial optimization such as undirected cut functions. In this paper, we show that any algorithm for the problem requires $Ω(2^{\frac{n}{7.54}})$ oracle calls to $f$, where $n=|V|$. It contrasts to the fact that the submodular function minimization, which is another generalization of cut functions, is polynomially solvable. When the range of a given posimodular function is restricted to be $D=\{0,1,...,d\}$ for some nonnegative integer $d$, we show that $Ω(2^{\frac{d}{15.08}})$ oracle calls are necessary, while we propose an $O(n^dT_f+n^{2d+1})$-time algorithm for the problem. Here, $T_f$ denotes the time needed to evaluate the function value $f(X)$ for a given $X \subseteq V$. We also consider the problem of maximizing a given posimodular function. We show that $Ω(2^{n-1})$ oracle calls are necessary for solving the problem, and that the problem has time complexity $Θ(n^{d-1}T_f) $ when $D=\{0,1,..., d\}$ is the range of $f$ for some constant $d$.
Permutation Reconstruction from Differences
Venue: arXiv cs.CC 2014
Year: 2014

We prove that the problem of reconstructing a permutation $π_1,\dotsc,π_n$ of the integers $[1\dotso n]$ given the absolute differences $|π_{i+1}-π_i|$, $i = 1,\dotsc,n-1$ is NP-complete. As an intermediate step we first prove the NP-completeness of the decision version of a new puzzle game that we call Crazy Frog Puzzle. The permutation reconstruction from differences is one of the simplest combinatorial problems that have been proved to be computationally intractable.
Enable Portrait Privacy Protection in Photo Capturing and Sharing
Venue: arXiv cs.CR 2014
Year: 2014

The wide adoption of wearable smart devices with onboard cameras greatly increases people's concern on privacy infringement. Here we explore the possibility of easing persons from photos captured by smart devices according to their privacy protection requirements. To make this work, we need to address two challenges: 1) how to let users explicitly express their privacy protection intention, and 2) how to associate the privacy requirements with persons in captured photos accurately and efficiently. Furthermore, the association process itself should not cause portrait information leakage and should be accomplished in a privacy-preserving way. In this work, we design, develop, and evaluate a protocol, that enables a user to flexibly express her privacy requirement and empowers the photo service provider (or image taker) to exert the privacy protection policy.Leveraging the visual distinguishability of people in the field-of-view and the dimension-order-independent property of vector similarity measurement, we achieves high accuracy and low overhead. We implement a prototype system, and our evaluation results on both the trace-driven and real-life experiments confirm the feasibility and efficiency of our system.
Hiding Sound in Image by K-LSB Mutation
Venue: arXiv cs.MM 2014
Year: 2014

In this paper a novel approach to hide sound files in a digital image is proposed and implemented such that it becomes difficult to conclude about the existence of the hidden data inside the image. In this approach, we utilize the rightmost k-LSB of pixels in an image to embed MP3 sound bits into a pixel. The pixels are so chosen that the distortion in image would be minimized due to embedding. This requires comparing all the possible permutations of pixel values, which may would lead to exponential time computation. To speed up this, Cuckoo Search (CS) could be used to find the most optimal solution. The advantage of using proposed CS is that it is easy to implement and is very effective at converging in relatively less iterations/generations.
StegExpose - A Tool for Detecting LSB Steganography
Venue: arXiv cs.MM 2014
Year: 2014

Steganalysis tools play an important part in saving time and providing new angles of attack for forensic analysts. StegExpose is a solution designed for use in the real world, and is able to analyse images for LSB steganography in bulk using proven attacks in a time efficient manner. When steganalytic methods are combined intelligently, they are able generate even more accurate results. This is the prime focus of StegExpose.
Matching Entities Across Online Social Networks
Venue: arXiv cs.SI 2014
Year: 2014

Online Social Networks (OSNs), such as Facebook and Twitter, have become an integral part of our daily lives. There are hundreds of OSNs, each with its own focus in that each offers particular services and functionalities. Recent studies show that many OSN users create several accounts on multiple OSNs using the same or different personal information. Collecting all the available data of an individual from several OSNs and fusing it into a single profile can be useful for many purposes. In this paper, we introduce novel machine learning based methods for solving Entity Resolution (ER), a problem for matching user profiles across multiple OSNs. The presented methods are able to match between two user profiles from two different OSNs based on supervised learning techniques, which use features extracted from each one of the user profiles. By using the extracted features and supervised learning techniques, we developed classifiers which can perform entity matching between two profiles for the following scenarios: (a) matching entities across two OSNs; (b) searching for a user by similar name; and (c) de-anonymizing a user's identity. The constructed classifiers were tested by using data collected from two popular OSNs, Facebook and Xing. We then evaluated the classifiers' performances using various evaluation measures, such as true and false positive rates, accuracy, and the Area Under the receiver operator Curve (AUC). The constructed classifiers were evaluated and their classification performance measured by AUC was quite remarkable, with an AUC of up to 0.982 and an accuracy of up to 95.9% in identifying user profiles across two OSNs.
On The Effect of Hyperedge Weights On Hypergraph Learning
Venue: arXiv cs.CV 2014
Year: 2014

Hypergraph is a powerful representation in several computer vision, machine learning and pattern recognition problems. In the last decade, many researchers have been keen to develop different hypergraph models. In contrast, no much attention has been paid to the design of hyperedge weights. However, many studies on pairwise graphs show that the choice of edge weight can significantly influence the performances of such graph algorithms. We argue that this also applies to hypegraphs. In this paper, we empirically discuss the influence of hyperedge weight on hypegraph learning via proposing three novel hyperedge weights from the perspectives of geometry, multivariate statistical analysis and linear regression. Extensive experiments on ORL, COIL20, JAFFE, Sheffield, Scene15 and Caltech256 databases verify our hypothesis. Similar to graph learning, several representative hyperedge weighting schemes can be concluded by our experimental studies. Moreover, the experiments also demonstrate that the combinations of such weighting schemes and conventional hypergraph models can get very promising classification and clustering performances in comparison with some recent state-of-the-art algorithms.