OpenRaiser/Intern-Atlas huggingface dataset:
Extracting Herbrand trees from Coq
Venue: arXiv cs.LO 2013
Year: 2013

Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the assumption that the libraries meet their specifications. In particular, a bug in these libraries might still impact the certified program. In this case, the difficulty that arises is to isolate the defective library function and provide a counter-example. In this paper, we show that this problem can be logically formalized as the construction of a Herbrand tree for a contradictory universal theory and address it. The solution we propose is based on a proof of Herbrand's theorem in the proof assistant Coq. Classical program extraction using Krivine's classical realizability then translates this proof into a certified program that computes Herbrand trees. Using this tree and calls to the library functions, we are able to determine which function is defective and explicitly produce a counter-example to its specification.
On the Benefits of Sampling in Privacy Preserving Statistical Analysis on Distributed Databases
Venue: arXiv cs.CR 2013
Year: 2013

We consider a problem where mutually untrusting curators possess portions of a vertically partitioned database containing information about a set of individuals. The goal is to enable an authorized party to obtain aggregate (statistical) information from the database while protecting the privacy of the individuals, which we formalize using Differential Privacy. This process can be facilitated by an untrusted server that provides storage and processing services but should not learn anything about the database. This work describes a data release mechanism that employs Post Randomization (PRAM), encryption and random sampling to maintain privacy, while allowing the authorized party to conduct an accurate statistical analysis of the data. Encryption ensures that the storage server obtains no information about the database, while PRAM and sampling ensures individual privacy is maintained against the authorized party. We characterize how much the composition of random sampling with PRAM increases the differential privacy of system compared to using PRAM alone. We also analyze the statistical utility of our system, by bounding the estimation error - the expected l2-norm error between the true empirical distribution and the estimated distribution - as a function of the number of samples, PRAM noise, and other system parameters. Our analysis shows a tradeoff between increasing PRAM noise versus decreasing the number of samples to maintain a desired level of privacy, and we determine the optimal number of samples that balances this tradeoff and maximizes the utility. In experimental simulations with the UCI "Adult Data Set" and with synthetically generated data, we confirm that the theoretically predicted optimal number of samples indeed achieves close to the minimal empirical error, and that our analytical error bounds match well with the empirical results.
An Adaptive and Intelligent Tutor by Expert Systems for Mobile Devices
Venue: arXiv cs.CY 2013
Year: 2013

Mobile Learning (M-Learning) is an emerging discipline in the area of education and educational technology. So researchers are trying to optimize and expanding its application in the field of education. The aim of this paper is to investigate the role of mobile devices and expert systems in disseminating and supporting the knowledge gained by intelligent tutors and to propose a system based on integration of intelligent M-Learning with expert systems. It acts as an intelligent tutor which can perform three processes - pre-test, learning concept and post-test - according to characteristic of the learner. The proposed system can improves the education efficiency highly as well as decreases costs. As a result, every time and everywhere (ETEW) simple and cheap learning would be provided via SMS, MMS and so on in this system. The global intention of M-Learning is to make learning "a way of being".
Generalized Public Key Transformations with Side Information
Venue: arXiv cs.CR 2013
Year: 2013

This paper presents results on generalized public key cryptography with exponentials modulo primes and composite numbers where the mapping is not one-to-one and the uniqueness is achieved by additional side information. Such transformations may be used for oblivious transfer and generate events of specific probabilities.
Developing a General algorithm for Ball Curve with GC2
Venue: arXiv cs.CG 2013
Year: 2013

This paper dwells in developing a general algorithm for constructing a piecewise Ball Curve with curvature continuity (GC2). The proposed algorithm requires GC2 data in which the designer must define unit tangent vectors and signed curvatures at each interpolating points. As a numerical example, a vase is constructed using GC2 piecewise Ball Curve
Computing Enclosures of Overdetermined Interval Linear Systems
Venue: arXiv cs.NA 2013
Year: 2013

This work considers special types of interval linear systems - overdetermined systems. Simply said these systems have more equations than variables. The solution set of an interval linear system is a collection of all solutions of all instances of an interval system. By the instance we mean a point real system that emerges when we independently choose a real number from each interval coefficient of the interval system. Enclosing the solution set of these systems is in some ways more difficult than for square systems. The main goal of this work is to present various methods for solving overdetermined interval linear systems. We would like to present them in an understandable way even for nonspecialists in a field of linear systems. The second goal is a numerical comparison of all the methods on random interval linear systems regarding widths of enclosures, computation times and other special properties of methods.
Feasibility study on distributed simulations of BGP
Venue: arXiv cs.NI 2013
Year: 2013

The Autonomous System (AS)-level topology of the Internet that currently comprises 40k ASs, is growing at a rate of about 10% per year. In these conditions, Border Gateway Protocol (BGP), the inter-domain routing protocol of the Internet starts to show its limits, among others in terms of the number of routing table entries it can dynamically process and control. To overcome this challenging situation, the design but also the evaluation of alternative dynamic routing models and their comparison with BGP shall be performed by means of simulation. For this purpose, DRMSim, a Dynamic Routing Model Simulator, was developed that provides the means for large-scale simulations of various routing models including BGP. By means of this discrete-event simulator, execution of path-vector routing, e.g. BGP, and other compact routing models have been successfully performed on network topologies comprising more than ten thousand (abstract) nodes. However, to simulate dynamic routing schemes like BGP, DRMSim needs enhancements to support current Internet size (40k ASs) and even more by considering its evolution (up to 100k ASs). This paper proposes a feasibility study of the extension of DRMSim so as to support the Distributed Parallel Discrete Event paradigm. We first detail the possible distribution models and their associated communication overhead. Then, we analyze the communication overhead of such a distributed simulator by executing BGP on a partitioned topology according to different scenarios. Finally, we conclude on the feasibility of such a simulator by computing the expected additional time required by a distributed simulation of BGP compared to its sequential simulation.
Recursive Mechanism: Towards Node Differential Privacy and Unrestricted Joins [Full Version, Draft 0.1]
Venue: arXiv cs.DB 2013
Year: 2013

Existing studies on differential privacy mainly consider aggregation on data sets where each entry corresponds to a particular participant to be protected. In many situations, a user may pose a relational algebra query on a sensitive database, and desires differentially private aggregation on the result of the query. However, no known work is capable to release this kind of aggregation when the query contains unrestricted join operations. This severely limits the applications of existing differential privacy techniques because many data analysis tasks require unrestricted joins. One example is subgraph counting on a graph. Existing methods for differentially private subgraph counting address only edge differential privacy and are subject to very simple subgraphs. Before this work, whether any nontrivial graph statistics can be released with reasonable accuracy under node differential privacy is still an open problem. In this paper, we propose a novel differentially private mechanism to release an approximation to a linear statistic of the result of some positive relational algebra calculation over a sensitive database. Unrestricted joins are supported in our mechanism. The error bound of the approximate answer is roughly proportional to the \emph{empirical sensitivity} of the query --- a new notion that measures the maximum possible change to the query answer when a participant withdraws its data from the sensitive database. For subgraph counting, our mechanism provides the first solution to achieve node differential privacy, for any kind of subgraphs.
Friends, Strangers, and the Value of Ego Networks for Recommendation
Venue: arXiv cs.SI 2013
Year: 2013

Two main approaches to using social network information in recommendation have emerged: augmenting collaborative filtering with social data and algorithms that use only ego-centric data. We compare the two approaches using movie and music data from Facebook, and hashtag data from Twitter. We find that recommendation algorithms based only on friends perform no worse than those based on the full network, even though they require much less data and computational resources. Further, our evidence suggests that locality of preference, or the non-random distribution of item preferences in a social network, is a driving force behind the value of incorporating social network information into recommender algorithms. When locality is high, as in Twitter data, simple k-nn recommenders do better based only on friends than they do if they draw from the entire network. These results help us understand when, and why, social network information is likely to support recommendation systems, and show that systems that see ego-centric slices of a complete network (such as websites that use Facebook logins) or have computational limitations (such as mobile devices) may profitably use ego-centric recommendation algorithms.
Formation control with binary information
Venue: arXiv cs.SY 2013
Year: 2013

In this paper, we study the problem of formation keeping of a network of strictly passive systems when very coarse information is exchanged. We assume that neighboring agents only know whether their relative position is larger or smaller than the prescribed one. This assumption results in very simple control laws that direct the agents closer or away from each other and take values in finite sets. We show that the task of formation keeping while tracking a desired trajectory and rejecting matched disturbances is still achievable under the very coarse information scenario. In contrast with other results of practical convergence with coarse or quantized information, here the control task is achieved exactly.
Fast exact digital differential analyzer for circle generation
Venue: arXiv cs.GR 2013
Year: 2013

In the first part of the paper we present a short review of applications of digital differential analyzers (DDA) to generation of circles showing that they can be treated as one-step numerical schemes. In the second part we present and discuss a novel fast algorithm based on a two-step numerical scheme (explicit midpoint rule). Although our algorithm is as cheap as the simplest one-step DDA algoritm (and can be represented in terms of shifts and additions), it generates circles with maximal accuracy, i.e., it is exact up to round-off errors.
Combinaison d'information visuelle, conceptuelle, et contextuelle pour la construction automatique de hierarchies semantiques adaptees a l'annotation d'images
Venue: arXiv cs.CV 2013
Year: 2013

This paper proposes a new methodology to automatically build semantic hierarchies suitable for image annotation and classification. The building of the hierarchy is based on a new measure of semantic similarity. The proposed measure incorporates several sources of information: visual, conceptual and contextual as we defined in this paper. The aim is to provide a measure that best represents image semantics. We then propose rules based on this measure, for the building of the final hierarchy, and which explicitly encode hierarchical relationships between different concepts. Therefore, the built hierarchy is used in a semantic hierarchical classification framework for image annotation. Our experiments and results show that the hierarchy built improves classification results. Ce papier propose une nouvelle methode pour la construction automatique de hierarchies semantiques adaptees a la classification et a l'annotation d'images. La construction de la hierarchie est basee sur une nouvelle mesure de similarite semantique qui integre plusieurs sources d'informations: visuelle, conceptuelle et contextuelle que nous definissons dans ce papier. L'objectif est de fournir une mesure qui est plus proche de la semantique des images. Nous proposons ensuite des regles, basees sur cette mesure, pour la construction de la hierarchie finale qui encode explicitement les relations hierarchiques entre les differents concepts. La hierarchie construite est ensuite utilisee dans un cadre de classification semantique hierarchique d'images en concepts visuels. Nos experiences et resultats montrent que la hierarchie construite permet d'ameliorer les resultats de la classification.
Blind Non-parametric Statistics for Multichannel Detection Based on Statistical Covariances
Venue: arXiv cs.IT 2013
Year: 2013

We consider the problem of detecting the presence of a spatially correlated multichannel signal corrupted by additive Gaussian noise (i.i.d across sensors). No prior knowledge is assumed about the system parameters such as the noise variance, number of sources and correlation among signals. It is well known that the GLRT statistics for this composite hypothesis testing problem are asymptotically optimal and sensitive to variation in system model or its parameter. To address these shortcomings we present a few non-parametric statistics which are functions of the elements of Bartlett decomposed sample covariance matrix. They are designed such that the detection performance is immune to the uncertainty in the knowledge of noise variance. The analysis presented verifies the invariability of threshold value and identifies a few specific scenarios where the proposed statistics have better performance compared to GLRT statistics. The sensitivity of the statistic to correlation among streams, number of sources and sample size at low signal to noise ratio are discussed.
Simplifying Generalized Belief Propagation on Redundant Region Graphs
Venue: arXiv cs.IT 2013
Year: 2013

The cluster variation method has been developed into a general theoretical framework for treating short-range correlations in many-body systems after it was first proposed by Kikuchi in 1951. On the numerical side, a message-passing approach called generalized belief propagation (GBP) was proposed by Yedidia, Freeman and Weiss about a decade ago as a way of computing the minimal value of the cluster variational free energy and the marginal distributions of clusters of variables. However the GBP equations are often redundant, and it is quite a non-trivial task to make the GBP iteration converges to a fixed point. These drawbacks hinder the application of the GBP approach to finite-dimensional frustrated and disordered systems. In this work we report an alternative and simple derivation of the GBP equations starting from the partition function expression. Based on this derivation we propose a natural and systematic way of removing the redundance of the GBP equations. We apply the simplified generalized belief propagation (SGBP) equations to the two-dimensional and the three-dimensional ferromagnetic Ising model and Edwards-Anderson spin glass model. The numerical results confirm that the SGBP message-passing approach is able to achieve satisfactory performance on these model systems. We also suggest that a subset of the SGBP equations can be neglected in the numerical iteration process without affecting the final results.
DEMO: Simulation of Realistic Mobility Model and Implementation of 802.11p (DSRC) for Vehicular Networks (VANET)
Venue: arXiv cs.NI 2013
Year: 2013

An ad hoc network of vehicles (VANET) consists of vehicles that exchange information via radio in order to improve road safety, traffic management and do better distribution of traffic load in time and space. Along with this it allows Internet access for passengers and users of vehicles. A significant characteristic while studying VANETs is the requirement of having a mobility model that gives aspects of real vehicular traffic. These scenarios play an important role in performance of VANETs. In our paper we have demonstration and description of generating realistic mobility model using various tools such as eWorld, OpenStreetMap, SUMO and TraNS. Generated mobility scenario is added to NS-2.34 (Network Simulator) for analysis of DSR and AODV routing protocol under 802.11p (DSRC/WAVE) and 802.11a. Results after analysis shows 802.11p is more suitable than 802.11a for VANET.
Some approximations in Model Checking and Testing
Venue: arXiv cs.LO 2013
Year: 2013

Model checking and testing are two areas with a similar goal: to verify that a system satisfies a property. They start with different hypothesis on the systems and develop many techniques with different notions of approximation, when an exact verification may be computationally too hard. We present some notions of approximation with their logic and statistics backgrounds, which yield several techniques for model checking and testing: Bounded Model Checking, Approximate Model Checking, Approximate Black-Box Checking, Approximate Model-based Testing and Approximate Probabilistic Model Checking. All these methods guarantee some quality and efficiency of the verification.
Trust Management Model for Cloud Computing Environment
Venue: arXiv cs.CR 2013
Year: 2013

Software as a service or (SaaS) is a new software development and deployment paradigm over the cloud and offers Information Technology services dynamically as "on-demand" basis over the internet. Trust is one of the fundamental security concepts on storing and delivering such services. In general, trust factors are integrated into such existent security frameworks in order to add a security level to entities collaborations through the trust relationship. However, deploying trust factor in the secured cloud environment are more complex engineering task due to the existence of heterogeneous types of service providers and consumers. In this paper, a formal trust management model has been introduced to manage the trust and its properties for SaaS in cloud computing environment. The model is capable to represent the direct trust, recommended trust, reputation etc. formally. For the analysis of the trust properties in the cloud environment, the proposed approach estimates the trust value and uncertainty of each peer by computing decay function, number of positive interactions, reputation factor and satisfaction level for the collected information.
An Introduction to Quantum Programming in Quipper
Venue: arXiv cs.PL 2013
Year: 2013

Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial introduction to the language, through a demonstration of how to make use of some of its key features. We illustrate many of Quipper's language features by developing a few well known examples of Quantum computation, including quantum teleportation, the quantum Fourier transform, and a quantum circuit for addition.
Solving Wave Equations on Unstructured Geometries
Venue: arXiv cs.MS 2013
Year: 2013

Waves are all around us--be it in the form of sound, electromagnetic radiation, water waves, or earthquakes. Their study is an important basic tool across engineering and science disciplines. Every wave solver serving the computational study of waves meets a trade-off of two figures of merit--its computational speed and its accuracy. Discontinuous Galerkin (DG) methods fall on the high-accuracy end of this spectrum. Fortuitously, their computational structure is so ideally suited to GPUs that they also achieve very high computational speeds. In other words, the use of DG methods on GPUs significantly lowers the cost of obtaining accurate solutions. This article aims to give the reader an easy on-ramp to the use of this technology, based on a sample implementation which demonstrates a highly accurate, GPU-capable, real-time visualizing finite element solver in about 1500 lines of code.
On Integrating Deductive Synthesis and Verification Systems
Venue: arXiv cs.PL 2013
Year: 2013

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures.
Particularities of Analog FCS Optimization
Venue: arXiv cs.IT 2013
Year: 2013

There is analyzed a performance of optimal feedback communication systems with the analog transmitters in the forward channel (AFCS). It is shown that measures and limit boundaries of AFCS performance are similar but differ from those used in digital communications and information theory. The causes of the differences are discussed.
Analytic Feature Selection for Support Vector Machines
Venue: arXiv cs.LG 2013
Year: 2013

Support vector machines (SVMs) rely on the inherent geometry of a data set to classify training data. Because of this, we believe SVMs are an excellent candidate to guide the development of an analytic feature selection algorithm, as opposed to the more commonly used heuristic methods. We propose a filter-based feature selection algorithm based on the inherent geometry of a feature set. Through observation, we identified six geometric properties that differ between optimal and suboptimal feature sets, and have statistically significant correlations to classifier performance. Our algorithm is based on logistic and linear regression models using these six geometric properties as predictor variables. The proposed algorithm achieves excellent results on high dimensional text data sets, with features that can be organized into a handful of feature types; for example, unigrams, bigrams or semantic structural features. We believe this algorithm is a novel and effective approach to solving the feature selection problem for linear SVMs.