OpenRaiser/Intern-Atlas huggingface dataset:
Framework for Version Control & Dependency Link of Components & Products in a Software Product Line
Venue: arXiv cs.SE 2015
Year: 2015

Software product line deals with the assembly of products from existing core assets commonly known as components and continuous growth in the core assets as we proceed with production. This idea has emerged as vital in terms of software development from component-based architecture. Since in software product line one has to deal with number of products and components simultaneous therefore there is a need to develop a strategy, which will help to store components and products information in such a way that they can be traced easily for further development. This storage strategy should reflect a relationship between products and components so that product history with reference to components can be traced and vise versa. In this paper we have presented a tree structure based storage strategy for components and products in software product line. This strategy will enable us to store the vital information about components and products with a relationship of their composition and utilization. We implemented this concept and simulated the software product line environment.
Bargaining Mechanisms for One-Way Games
Venue: arXiv cs.GT 2015
Year: 2015

We introduce one-way games, a framework motivated by applications in large-scale power restoration, humanitarian logistics, and integrated supply-chains. The distinguishable feature of the games is that the payoff of some player is determined only by her own strategy and does not depend on actions taken by other players. We show that the equilibrium outcome in one-way games without payments and the social cost of any ex-post efficient mechanism, can be far from the optimum. We also show that it is impossible to design a Bayes-Nash incentive-compatible mechanism for one-way games that is budget-balanced, individually rational, and efficient. To address this negative result, we propose a privacy-preserving mechanism that is incentive-compatible and budget-balanced, satisfies ex-post individual rationality conditions, and produces an outcome which is more efficient than the equilibrium without payments. The mechanism is based on a single-offer bargaining and we show that a randomized multi-offer extension brings no additional benefit.
Optimal Power Allocation for LTE Users with Different Modulations
Venue: arXiv cs.NI 2015
Year: 2015

In this paper, we demonstrate the optimal power allocation for QPSK, 16-QAM, and 64-QAM modulation schedules and the role of channel quality indicator (CQI). We used sigmoidal-like utility functions to represent the probability of successful reception of packets at user equipment (UE). CQI as a feedback to the base station (BS) indicates the data rate that a downlink channel can support. With Levenberg-Marquardt (LM) Optimization method, we present utility functions of different CQI values for standardized 15 Modulation order and Coding Scheme (MCS) in $3^{rd}$ Generation Partnership Project (3GPP). Finally, we simulate and show the results of the optimal power allocation algorithm.
Spatial mixing and approximate counting for Potts model on graphs with bounded average degree
Venue: arXiv cs.DS 2015
Year: 2015

We propose a notion of contraction function for a family of graphs and establish its connection to the strong spatial mixing for spin systems. More specifically, we show that for anti-ferromagnetic Potts model on families of graphs characterized by a specific contraction function, the model exhibits strong spatial mixing, and if further the graphs exhibit certain local sparsity which are very natural and easy to satisfy by typical sparse graphs, then we also have FPTAS for computing the partition function. This new characterization of strong spatial mixing of multi-spin system does not require maximum degree of the graphs to be bounded, but instead it relates the decay of correlation of the model to a notion of effective average degree measured by the contraction of a function on the family of graphs. It also generalizes other notion of effective average degree which may determine the strong spatial mixing, such as the connective constant, whose connection to strong spatial mixing is only known for very simple models and is not extendable to general spin systems. As direct consequences: (1) we obtain FPTAS for the partition function of $q$-state anti-ferromagnetic Potts model with activity $0\leβ<1$ on graphs of maximum degree bounded by $d$ when $q> 3(1-β)d+1$, improving the previous best bound $β> 3(1-β)d$ and asymptotically approaching the inapproximability threshold $q=(1-β)d$, and (2) we obtain an efficient sampler (in the same sense of fully polynomial-time almost uniform sampler, FPAUS) for the Potts model on Erdős-Rényi random graph $\mathcal{G}(n,d/n)$ with sufficiently large constant $d$, provided that $q> 3(1-β)d+4$. In particular when $β=0$, the sampler becomes an FPAUS for for proper $q$-coloring in $\mathcal{G}(n,d/n)$ with $q> 3d+4$, improving the current best bound $q> 5.5d$ for FPAUS for $q$-coloring in $\mathcal{G}(n,d/n)$.
Molecular Communications: Channel Model and Physical Layer Techniques
Venue: arXiv cs.ET 2015
Year: 2015

This article examines recent research in molecular communications from a telecommunications system design perspective. In particular, it focuses on channel models and state-of-the-art physical layer techniques. The goal is to provide a foundation for higher layer research and motivation for research and development of functional prototypes. In the first part of the article, we focus on the channel and noise model, comparing molecular and radio-wave pathloss formulae. In the second part, the article examines, equipped with the appropriate channel knowledge, the design of appropriate modulation and error correction coding schemes. The third reviews transmitter and receiver side signal processing methods that suppress inter-symbol-interference. Taken together, the three parts present a series of physical layer techniques that are necessary to producing reliable and practical molecular communications.
A model for the temporal evolution of the spatial coherence in decaying reverberant sound fields
Venue: arXiv cs.SD 2015
Year: 2015

Reverberant sound fields are often modeled as isotropic. However, it has been observed that spatial properties change during the decay of the sound field energy, due to non-isotropic attenuation in non-ideal rooms. In this letter, a model for the spatial coherence between two sensors in a decaying reverberant sound field is developed for rectangular rooms. The modeled coherence function depends on room dimensions, surface reflectivity and orientation of the sensor pair, but is independent of the position of source and sensors in the room. The model includes the spherically isotropic (diffuse) and cylindrically isotropic sound field models as special cases.
Application of Kullback-Leibler divergence for short-term user interest detection
Venue: arXiv cs.IR 2015
Year: 2015

Classical approaches in recommender systems such as collaborative filtering are concentrated mainly on static user preference extraction. This approach works well as an example for music recommendations when a user behavior tends to be stable over long period of time, however the most common situation in e-commerce is different which requires reactive algorithms based on a short-term user activity analysis. This paper introduces a small mathematical framework for short-term user interest detection formulated in terms of item properties and its application for recommender systems enhancing. The framework is based on the fundamental concept of information theory --- Kullback-Leibler divergence.
Resource Allocation in Cellular Systems for Applications with Random Parameters
Venue: arXiv cs.NI 2015
Year: 2015

In this paper, we conduct a study to optimize resource allocation for adaptive real-time and delay-tolerant applications in cellular systems. To represent the user applications via several devices and equipment, sigmoidal-like and logarithm utility functions are used. A fairness proportional utility functions policy approach is used to allocate the resources among the user equipment (UE)s in a utility percentage form and to ensure a minimum level of customer satisfaction for all the subscribers. Meanwhile, the priority of resources allocation is given to the real-time applications. We measure the effect of the stochastic variations of the adaptive real-time applications on the optimal rate allocation process and compare the results of deterministic and stochastic systems. Our work is distinct from the other resource allocation optimization works in that we use bisection method besides convex optimization techniques to optimally allocate rates, and we present the adaptive real- time applications in a stochastic form. We use Microsoft Visual Basic for Applications with Arena Simulation Software interface to simulate the optimization problem. Finally, we present our optimization algorithm results.
Featherweight VeriFast
Venue: arXiv cs.LO 2015
Year: 2015

VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFast's operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq.
Forensic Analysis of WhatsApp Messenger on Android Smartphones
Venue: arXiv cs.CR 2015
Year: 2015

We present the forensic analysis of the artifacts left on Android devices by \textit{WhatsApp Messenger}, the client of the WhatsApp instant messaging system. We provide a complete description of all the artifacts generated by WhatsApp Messenger, we discuss the decoding and the interpretation of each one of them, and we show how they can be correlated together to infer various types of information that cannot be obtained by considering each one of them in isolation. By using the results discussed in this paper, an analyst will be able to reconstruct the list of contacts and the chronology of the messages that have been exchanged by users. Furthermore, thanks to the correlation of multiple artifacts, (s)he will be able to infer information like when a specific contact has been added, to recover deleted contacts and their time of deletion, to determine which messages have been deleted, when these messages have been exchanged, and the users that exchanged them.
On the Unicity of Smartphone Applications
Venue: arXiv cs.CR 2015
Year: 2015

Prior works have shown that the list of apps installed by a user reveal a lot about user interests and behavior. These works rely on the semantics of the installed apps and show that various user traits could be learnt automatically using off-the-shelf machine-learning techniques. In this work, we focus on the re-identifiability issue and thoroughly study the unicity of smartphone apps on a dataset containing 54,893 Android users collected over a period of 7 months. Our study finds that any 4 apps installed by a user are enough (more than 95% times) for the re-identification of the user in our dataset. As the complete list of installed apps is unique for 99% of the users in our dataset, it can be easily used to track/profile the users by a service such as Twitter that has access to the whole list of installed apps of users. As our analyzed dataset is small as compared to the total population of Android users, we also study how unicity would vary with larger datasets. This work emphasizes the need of better privacy guards against collection, use and release of the list of installed apps.
Occlusion-Aware Object Localization, Segmentation and Pose Estimation
Venue: arXiv cs.CV 2015
Year: 2015

We present a learning approach for localization and segmentation of objects in an image in a manner that is robust to partial occlusion. Our algorithm produces a bounding box around the full extent of the object and labels pixels in the interior that belong to the object. Like existing segmentation aware detection approaches, we learn an appearance model of the object and consider regions that do not fit this model as potential occlusions. However, in addition to the established use of pairwise potentials for encouraging local consistency, we use higher order potentials which capture information at the level of im- age segments. We also propose an efficient loss function that targets both localization and segmentation performance. Our algorithm achieves 13.52% segmentation error and 0.81 area under the false-positive per image vs. recall curve on average over the challenging CMU Kitchen Occlusion Dataset. This is a 42.44% decrease in segmentation error and a 16.13% increase in localization performance compared to the state-of-the-art. Finally, we show that the visibility labelling produced by our algorithm can make full 3D pose estimation from a single image robust to occlusion.
Sparse Multidimensional Patient Modeling using Auxiliary Confidence Labels
Venue: arXiv cs.LG 2015
Year: 2015

In this work, we focus on the problem of learning a classification model that performs inference on patient Electronic Health Records (EHRs). Often, a large amount of costly expert supervision is required to learn such a model. To reduce this cost, we obtain confidence labels that indicate how sure an expert is in the class labels she provides. If meaningful confidence information can be incorporated into a learning method, fewer patient instances may need to be labeled to learn an accurate model. In addition, while accuracy of predictions is important for any inference model, a model of patients must be interpretable so that clinicians can understand how the model is making decisions. To these ends, we develop a novel metric learning method called Confidence bAsed MEtric Learning (CAMEL) that supports inclusion of confidence labels, but also emphasizes interpretability in three ways. First, our method induces sparsity, thus producing simple models that use only a few features from patient EHRs. Second, CAMEL naturally produces confidence scores that can be taken into consideration when clinicians make treatment decisions. Third, the metrics learned by CAMEL induce multidimensional spaces where each dimension represents a different "factor" that clinicians can use to assess patients. In our experimental evaluation, we show on a real-world clinical data set that our CAMEL methods are able to learn models that are as or more accurate as other methods that use the same supervision. Furthermore, we show that when CAMEL uses confidence scores it is able to learn models as or more accurate as others we tested while using only 10% of the training instances. Finally, we perform qualitative assessments on the metrics learned by CAMEL and show that they identify and clearly articulate important factors in how the model performs inference.
TDD for Embedded Systems: A Basic Approach and Toolset
Venue: arXiv cs.SE 2015
Year: 2015

The evolution of information technology and electronics in general has been consistently increasing the use of embedded systems. While hardware development for these systems is already consistent, software development for embedded systems still lacks a consolidated methodology. This paper describes a process and toolset for Embedded Systems Validation and Verification using FSM (Finite State Machines) and TDD (Test Driven Development).
AFDI: A Virtualization-based Accelerated Fault Diagnosis Innovation for High Availability Computing
Venue: arXiv cs.SE 2015
Year: 2015

Fault diagnosis has attracted extensive attention for its importance in the exceedingly fault management framework for cloud virtualization, despite the fact that fault diagnosis becomes more difficult due to the increasing scalability and complexity in a heterogeneous environment for a virtualization technique. Most existing fault diagnoses methods are based on active probing techniques which can be used to detect the faults rapidly and precisely. However, most of those methods suffer from the limitation of traffic overhead and diagnosis of faults, which leads to a reduction in system performance. In this paper, we propose a new hybrid model named accelerated fault diagnosis invention (AFDI) to monitor various system metrics for VMs and physical server hosting, such as CPU, memory, and network usages based on the severity of fault levels and anomalies. The proposed method takes the advantages of the multi-valued decision diagram (MDD), A Naive Bayes Classifier (NBC) models and virtual sensors cloud to achieve high availability for cloud services.
Rewriting Modulo βin the λΠ-Calculus Modulo
Venue: arXiv cs.LO 2015
Year: 2015

The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. But this is too restrictive. To handle the case where non confluence comes from the interference between the beta-reduction and rewrite rules with lambda-abstraction on their left-hand side, we introduce a notion of rewriting modulo beta for the lambda-Pi-calculus Modulo. We prove that confluence of rewriting modulo beta is enough to ensure subject reduction and uniqueness of types. We achieve our goal by encoding the lambda-Pi-calculus Modulo into Higher-Order Rewrite System (HRS). As a consequence, we also make the confluence results for HRSs available for the lambda-Pi-calculus Modulo.
Tabling as a Library with Delimited Control
Venue: arXiv cs.PL 2015
Year: 2015

Tabling is probably the most widely studied extension of Prolog. But despite its importance and practicality, tabling is not implemented by most Prolog systems. Existing approaches require substantial changes to the Prolog engine, which is an investment out of reach of most systems. To enable more widespread adoption, we present a new implementation of tabling in under 600 lines of Prolog code. Our lightweight approach relies on delimited control and provides reasonable performance.
Property irrelevant predicates
Venue: arXiv cs.PL 2015
Year: 2015

Although slicing removes code which has no bearing on property checking. However even after that, our study has found that there are predicates in program which have no bearing on property validation, although slicing could not eliminate them. We have cope up with a criteria to identify such predicates and then give a process to leverage them in scale up of property checking.
A Network-Aware Approach for Searching As-You-Type in Social Media (Extended Version)
Venue: arXiv cs.IR 2015
Year: 2015

We present in this paper a novel approach for as-you-type top-$k$ keyword search over social media. We adopt a natural "network-aware" interpretation for information relevance, by which information produced by users who are closer to the seeker is considered more relevant. In practice, this query model poses new challenges for effectiveness and efficiency in online search, even when a complete query is given as input in one keystroke. This is mainly because it requires a joint exploration of the social space and classic IR indexes such as inverted lists. We describe a memory-efficient and incremental prefix-based retrieval algorithm, which also exhibits an anytime behavior, allowing to output the most likely answer within any chosen running-time limit. We evaluate it through extensive experiments for several applications and search scenarios, including searching for posts in micro-blogging (Twitter and Tumblr), as well as searching for businesses based on reviews in Yelp. They show that our solution is effective in answering real-time as-you-type searches over social media.
Flow Rounding
Venue: arXiv cs.DS 2015
Year: 2015

We consider flow rounding: finding an integral flow from a fractional flow. Costed flow rounding asks that we find an integral flow with no worse cost. Randomized flow rounding requires we randomly find an integral flow such that the expected flow along each edge matches the fractional flow. Both problems are reduced to cycle canceling, for which we develop an $O(m \log(n^2/m))$ algorithm.
Fast Biclustering by Dual Parameterization
Venue: arXiv cs.DS 2015
Year: 2015

We study two clustering problems, Starforest Editing, the problem of adding and deleting edges to obtain a disjoint union of stars, and the generalization Bicluster Editing. We show that, in addition to being NP-hard, none of the problems can be solved in subexponential time unless the exponential time hypothesis fails. Misra, Panolan, and Saurabh (MFCS 2013) argue that introducing a bound on the number of connected components in the solution should not make the problem easier: In particular, they argue that the subexponential time algorithm for editing to a fixed number of clusters (p-Cluster Editing) by Fomin et al. (J. Comput. Syst. Sci., 80(7) 2014) is an exception rather than the rule. Here, p is a secondary parameter, bounding the number of components in the solution. However, upon bounding the number of stars or bicliques in the solution, we obtain algorithms which run in time $2^{5 \sqrt{pk}} + O(n+m)$ for p-Starforest Editing and $2^{O(p \sqrt{k} \log(pk))} + O(n+m)$ for p-Bicluster Editing. We obtain a similar result for the more general case of t-Partite p-Cluster Editing. This is subexponential in k for fixed number of clusters, since p is then considered a constant. Our results even out the number of multivariate subexponential time algorithms and give reasons to believe that this area warrants further study.
Asymmetric Topologies on Statistical Manifolds
Venue: arXiv cs.IT 2015
Year: 2015

Asymmetric information distances are used to define asymmetric norms and quasimetrics on the statistical manifold and its dual space of random variables. Quasimetric topology, generated by the Kullback-Leibler (KL) divergence, is considered as the main example, and some of its topological properties are investigated.