OpenRaiser/Intern-Atlas huggingface dataset:
Teaching Formal Methods and Discrete Mathematics
Venue: arXiv cs.CY 2014
Year: 2014

Despite significant advancements in the conception of (formal) integrated development environments, applying formal methods in software industry is still perceived as a difficult task. To make the task easier, providing tools that help during the development cycle is essential but we think that education of computer scientists and software engineers is also an important challenge to take up. Indeed, we believe that formal methods courses do not appear sufficiently early in compter science curricula and thus are not widely used and perceived as a valid professional skill. In this paper, we claim that teaching formal methods could be done at the undergraduate level by mixing formal methods and discrete mathematics courses and we illustrate such an approach with a small develop- ment within FoCaLiZe. We also believe that this could considerably benefit the learning of discrete mathematics.
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
Venue: arXiv cs.SE 2014
Year: 2014

OpenJML is a tool for checking code and specifications of Java programs. We describe our experience building the tool on the foundation of JML, OpenJDK and Eclipse, as well as on many advances in specification-based software verification. The implementation demonstrates the value of integrating specification tools directly in the software development IDE and in automating as many tasks as possible. The tool, though still in progress, has now been used for several college-level courses on software specification and verification and for small-scale studies on existing Java programs.
The Oblivious Transfer Capacity of the Wiretapped Binary Erasure Channel
Venue: arXiv cs.IT 2014
Year: 2014

We consider oblivious transfer between Alice and Bob in the presence of an eavesdropper Eve when there is a broadcast channel from Alice to Bob and Eve. In addition to the secrecy constraints of Alice and Bob, Eve should not learn the private data of Alice and Bob. When the broadcast channel consists of two independent binary erasure channels, we derive the oblivious transfer capacity for both 2-privacy (where the eavesdropper may collude with either party) and 1-privacy (where there are no collusions).
How to extract data from proprietary software database systems using TCP/IP?
Venue: arXiv cs.DB 2014
Year: 2014

This document is an white paper about how to connect reverse engineering and programing skills to extract data from a proprietary implementation of a database system to build EML-Tools for data format conversion into raw data. This article shows how to access data of a source software system without any interface for data conversion. We discuss how raw data can be transfered into structural format by using XML or any other custom designed software solution. For demonstration purposes only, we will use a CRM system called Harmony(r) by Harmony(r) Software AG, the programing language Python and methods of computer security, which are used to get quick access to the raw data. All trademarks are property of their owners, as Harmony(r) is of Harmony Software AG.
Sampling Techniques for Boolean Satisfiability
Venue: arXiv cs.LO 2014
Year: 2014

Boolean satisfiability ({\SAT}) has played a key role in diverse areas spanning testing, formal verification, planning, optimization, inferencing and the like. Apart from the classical problem of checking boolean satisfiability, the problems of generating satisfying uniformly at random, and of counting the total number of satisfying assignments have also attracted significant theoretical and practical interest over the years. Prior work offered heuristic approaches with very weak or no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We propose a novel approach based on limited-independence hashing that allows us to design algorithms for both problems, with strong theoretical guarantees and scalability extending to thousands of variables. Based on this approach, we present two practical algorithms, {\UniformWitness}: a near uniform generator and {\approxMC}: the first scalable approximate model counter, along with reference implementations. Our algorithms work by issuing polynomial calls to {\SAT} solver. We demonstrate scalability of our algorithms over a large set of benchmarks arising from different application domains.
Scheduling of Multicast and Unicast Services under Limited Feedback by using Rateless Codes
Venue: arXiv cs.IT 2014
Year: 2014

Many opportunistic scheduling techniques are impractical because they require accurate channel state information (CSI) at the transmitter. In this paper, we investigate the scheduling of unicast and multicast services in a downlink network with a very limited amount of feedback information. Specifically, unicast users send imperfect (or no) CSI and infrequent acknowledgements (ACKs) to a base station, and multicast users only report infrequent ACKs to avoid feedback implosion. We consider the use of physical-layer rateless codes, which not only combats channel uncertainty, but also reduces the overhead of ACK feedback. A joint scheduling and power allocation scheme is developed to realize multiuser diversity gain for unicast service and multicast gain for multicast service. We prove that our scheme achieves a near-optimal throughput region. Our simulation results show that our scheme significantly improves the network throughput over schemes employing fixed-rate codes or using only unicast communications.
Hybrid Metaheuristics for the Clustered Vehicle Routing Problem
Venue: arXiv cs.AI 2014
Year: 2014

The Clustered Vehicle Routing Problem (CluVRP) is a variant of the Capacitated Vehicle Routing Problem in which customers are grouped into clusters. Each cluster has to be visited once, and a vehicle entering a cluster cannot leave it until all customers have been visited. This article presents two alternative hybrid metaheuristic algorithms for the CluVRP. The first algorithm is based on an Iterated Local Search algorithm, in which only feasible solutions are explored and problem-specific local search moves are utilized. The second algorithm is a Hybrid Genetic Search, for which the shortest Hamiltonian path between each pair of vertices within each cluster should be precomputed. Using this information, a sequence of clusters can be used as a solution representation and large neighborhoods can be efficiently explored by means of bi-directional dynamic programming, sequence concatenations, by using appropriate data structures. Extensive computational experiments are performed on benchmark instances from the literature, as well as new large scale ones. Recommendations on promising algorithm choices are provided relatively to average cluster size.
Practical Experience Report: The Performance of Paxos in the Cloud
Venue: arXiv cs.DC 2014
Year: 2014

This experience report presents the results of an extensive performance evaluation conducted using four open-source implementations of Paxos deployed in Amazon's EC2. Paxos is a fundamental algorithm for building fault-tolerant services, at the core of state-machine replication. Implementations of Paxos are currently used in many prototypes and production systems in both academia and industry. Although all protocols surveyed in the paper implement Paxos, they are optimized in a number of different ways, resulting in very different behavior, as we show in the paper. We have considered a variety of configurations and failure-free and faulty executions. In addition to reporting our findings, we propose and assess additional optimizations to existing implementations.
Optimistic Parallel State-Machine Replication
Venue: arXiv cs.DC 2014
Year: 2014

State-machine replication, a fundamental approach to fault tolerance, requires replicas to execute commands deterministically, which usually results in sequential execution of commands. Sequential execution limits performance and underuses servers, which are increasingly parallel (i.e., multicore). To narrow the gap between state-machine replication requirements and the characteristics of modern servers, researchers have recently come up with alternative execution models. This paper surveys existing approaches to parallel state-machine replication and proposes a novel optimistic protocol that inherits the scalable features of previous techniques. Using a replicated B+-tree service, we demonstrate in the paper that our protocol outperforms the most efficient techniques by a factor of 2.4 times.
Inventions on Tree Navigators used in Graphical User Interface
Venue: arXiv cs.HC 2014
Year: 2014

A tree view or tree navigator is used to display hierarchical data organized in the form of a tree. In a tree structure there are parent and child nodes. The child nodes may further have descendants to n levels. There are many methods to make the navigation easy. Some of these are expanding and collapsing branches, splitting the tree, displaying a parent node in a separate tree, zooming branches, scrolling in various directions etc. It is still a difficult exercise to handle large trees efficiently. The effort still continues to manage large number of nodes with faster speed, greater control, user friendliness and aesthetics. This article illustrates five inventions on tree navigators selected from US patent database. Each of them tries to solve various problems relating to the tree navigator in different ways. Each invention is also analyzed from a TRIZ perspective.
Formalism of Requirements for Safety-Critical Software: Where Does the Benefit Come From?
Venue: arXiv cs.SE 2014
Year: 2014

Safety and assurance standards often rely on the principle that requirements errors can be minimised by expressing the requirements more formally. Although numerous case studies have shown that the act of formalising previously informal requirements finds requirements errors, this principle is really just a hypothesis. An industrially persuasive causal relationship between formalisation and better requirements has yet to be established. We describe multiple competing explanations for this hypothesis, in terms of the levels of precision, re-formulation, expertise, effort and automation that are typically associated with formalising requirements. We then propose an experiment to distinguish between these explanations, without necessarily excluding the possibility that none of them are correct.
On the efficacy of safety-related software standards
Venue: arXiv cs.SE 2014
Year: 2014

Difficulty of safety-related software standards to help producing software for safe systems is discussed. Some research activity and other actions are proposed to focus on and possibly resolve long-lasting related problems.
Improving Blind Source Separation Performance By Adaptive Array Geometries For Humanoid Robots
Venue: arXiv cs.SD 2014
Year: 2014

In this paper, the concept of an adaptation algorithm is proposed, which can be used to blindly adapt the microphone array geometry of a humanoid robot such that the performance of the underlying signal separation algorithm is improved. As a decisive feature, an online performance measure for blind source separation is introduced which allows a robust and reliable estimation of the instantaneous separation performance based on currently observable data. Experimental results from a simulated environment confirm the efficacy of the concept.
Interval-Valued Intuitionistic Fuzzy Matrices
Venue: arXiv cs.DM 2014
Year: 2014

In this paper, the interval-valued intuitionistic fuzzy matrix (IVIFM) is introduced. The interval-valued intuitionistic fuzzy determinant is also defined. Some fundamental operations are also presented. The need of IVIFM is explain by an example.
Deontic Logic for Human Reasoning
Venue: arXiv cs.AI 2014
Year: 2014

Deontic logic is shown to be applicable for modelling human reasoning. For this the Wason selection task and the suppression task are discussed in detail. Different versions of modelling norms with deontic logic are introduced and in the case of the Wason selection task it is demonstrated how differences in the performance of humans in the abstract and in the social contract case can be explained. Furthermore it is shown that an automated theorem prover can be used as a reasoning tool for deontic logic.
An adjustable-width window with good dynamic range
Venue: arXiv cs.NA 2014
Year: 2014

A new variable-width window is presented and compared with several other windows, both of variable and fixed widths. The comparison focuses on sensitivity and dynamic range. The equivalent noise bandwidth or ENBW (or rather, its reciprocal) is used as a proxy for the first; maximum sidelobe level and high-frequency roll-off in the Fourier transform, for the second. The new window can access any value of ENBW by appropriate choice of the width parameter. At any given value of ENBW below about 3, a setting can be found at which the sidelobes of the window are lower than those of any other in the moderate frequency regime below about 100 cycles.
An Extremal Inequality for Long Markov Chains
Venue: arXiv cs.IT 2014
Year: 2014

Let $X,Y$ be jointly Gaussian vectors, and consider random variables $U,V$ that satisfy the Markov constraint $U-X-Y-V$. We prove an extremal inequality relating the mutual informations between all ${4 \choose 2}$ pairs of random variables from the set $(U,X,Y,V)$. As a first application, we show that the rate region for the two-encoder quadratic Gaussian source coding problem follows as an immediate corollary of the the extremal inequality. In a second application, we establish the rate region for a vector-Gaussian source coding problem where Löwner-John ellipsoids are approximated based on rate-constrained descriptions of the data.
Empirical Evidences in Citation-Based Search Engines: Is Microsoft Academic Search dead?
Venue: arXiv cs.DL 2014
Year: 2014

The goal of this working paper is to summarize the main empirical evidences provided by the scientific community as regards the comparison between the two main citation based academic search engines: Google Scholar and Microsoft Academic Search, paying special attention to the following issues: coverage, correlations between journal rankings, and usage of these academic search engines. Additionally, selfelaborated data is offered, which are intended to provide current evidence about the popularity of these tools on the Web, by measuring the number of rich files PDF, PPT and DOC in which these tools are mentioned, the amount of external links that both products receive, and the search queries frequency from Google Trends. The poor results obtained by MAS led us to an unexpected and unnoticed discovery: Microsoft Academic Search is outdated since 2013. Therefore, the second part of the working paper aims at advancing some data demonstrating this lack of update. For this purpose we gathered the number of total records indexed by Microsoft Academic Search since 2000. The data shows an abrupt drop in the number of documents indexed from 2,346,228 in 2010 to 8,147 in 2013 and 802 in 2014. This decrease is offered according to 15 thematic areas as well. In view of these problems it seems logical not only that Microsoft Academic Searchwas poorly used to search for articles by academics and students, who mostly use Google or Google Scholar, but virtually ignored by bibliometricians
Time Petri Nets with Dynamic Firing Dates: Semantics and Applications
Venue: arXiv cs.LO 2014
Year: 2014

We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the current marking. Next, we allow to update the firing date of a transition when it is persistent, that is when a concurrent transition fires. We show how to carry the widely used state class abstraction to this new kind of time Petri nets and define a class of nets for which the abstraction is exact. We show the usefulness of our approach with two applications: first for scheduling preemptive task, as a poor man's substitute for stopwatch, then to model hybrid systems with non trivial continuous behavior.
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems
Venue: arXiv cs.SY 2014
Year: 2014

We present the framework of delta-complete analysis for bounded reachability problems of general hybrid systems. We perform bounded reachability checking through solving delta-decision problems over the reals. The techniques take into account of robustness properties of the systems under numerical perturbations. We prove that the verification problems become much more mathematically tractable in this new framework. Our implementation of the techniques, an open-source tool dReach, scales well on several highly nonlinear hybrid system models that arise in biomedical and robotics applications.
Fast Approximation of Rotations and Hessians matrices
Venue: arXiv cs.LG 2014
Year: 2014

A new method to represent and approximate rotation matrices is introduced. The method represents approximations of a rotation matrix $Q$ with linearithmic complexity, i.e. with $\frac{1}{2}n\lg(n)$ rotations over pairs of coordinates, arranged in an FFT-like fashion. The approximation is "learned" using gradient descent. It allows to represent symmetric matrices $H$ as $QDQ^T$ where $D$ is a diagonal matrix. It can be used to approximate covariance matrix of Gaussian models in order to speed up inference, or to estimate and track the inverse Hessian of an objective function by relating changes in parameters to changes in gradient along the trajectory followed by the optimization procedure. Experiments were conducted to approximate synthetic matrices, covariance matrices of real data, and Hessian matrices of objective functions involved in machine learning problems.
Coupled Matrix Factorization within Non-IID Context
Venue: arXiv cs.IR 2014
Year: 2014

Recommender systems research has experienced different stages such as from user preference understanding to content analysis. Typical recommendation algorithms were built on the following bases: (1) assuming users and items are IID, namely independent and identically distributed, and (2) focusing on specific aspects such as user preferences or contents. In reality, complex recommendation tasks involve and request (1) personalized outcomes to tailor heterogeneous subjective preferences; and (2) explicit and implicit objective coupling relationships between users, items, and ratings to be considered as intrinsic forces driving preferences. This inevitably involves the non-IID complexity and the need of combining subjective preference with objective couplings hidden in recommendation applications. In this paper, we propose a novel generic coupled matrix factorization (CMF) model by incorporating non-IID coupling relations between users and items. Such couplings integrate the intra-coupled interactions within an attribute and inter-coupled interactions among different attributes. Experimental results on two open data sets demonstrate that the user/item couplings can be effectively applied in RS and CMF outperforms the benchmark methods.
Modeling and Execution of Multienterprise Business Processes
Venue: arXiv cs.SE 2014
Year: 2014

We discuss a fully featured multienterprise business process plattform (ME-BPP) based on the concepts of agent-based business processes. Using the concepts of the subject-oriented business process (S-BPM) methodology we developed an architecture to realize a platform for the execution of distributed business processes. The platform is implemented based on cloud technology using commercial services. For our discussion we used the well known Service Interaction Patterns, as they are empirically developed from typical business-to-business interactions. We can demonstrate that all patterns can be easily modeled and executed based on our architecture. We propose therefore a change from a control flow based to an agent based view to model and enact business processes.
Channel-Optimized Vector Quantizer Design for Compressed Sensing Measurements
Venue: arXiv cs.IT 2014
Year: 2014

We consider vector-quantized (VQ) transmission of compressed sensing (CS) measurements over noisy channels. Adopting mean-square error (MSE) criterion to measure the distortion between a sparse vector and its reconstruction, we derive channel-optimized quantization principles for encoding CS measurement vector and reconstructing sparse source vector. The resulting necessary optimal conditions are used to develop an algorithm for training channel-optimized vector quantization (COVQ) of CS measurements by taking the end-to-end distortion measure into account.
Light Spanners
Venue: arXiv cs.DS 2014
Year: 2014

A $t$-spanner of a weighted undirected graph $G=(V,E)$, is a subgraph $H$ such that $d_H(u,v)\le t\cdot d_G(u,v)$ for all $u,v\in V$. The sparseness of the spanner can be measured by its size (the number of edges) and weight (the sum of all edge weights), both being important measures of the spanner's quality -- in this work we focus on the latter. Specifically, it is shown that for any parameters $k\ge 1$ and $ε>0$, any weighted graph $G$ on $n$ vertices admits a $(2k-1)\cdot(1+ε)$-stretch spanner of weight at most $w(MST(G))\cdot O_ε(kn^{1/k}/\log k)$, where $w(MST(G))$ is the weight of a minimum spanning tree of $G$. Our result is obtained via a novel analysis of the classic greedy algorithm, and improves previous work by a factor of $O(\log k)$.
Towards Verification of Constituent Systems through Automated Proof
Venue: arXiv cs.SE 2014
Year: 2014

This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports various contractual specification elements, such as state invariants and operation preconditions, which can be used to specify contractual obligations on the constituent systems of a SoS. To support verification of these obligations we have developed a proof obligation generator and theorem prover plugin for Symphony. The latter uses the Isabelle/HOL theorem prover to automatically discharge the proof obligations arising from a CML model. Our hope is that the resulting proofs can then be used to formally verify the conformance of each constituent system, which is turn would result in a dependable SoS.
Topology Construction in RPL Networks over Beacon-Enabled 802.15.4
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, we propose a new scheme that allows coupling beacon-enabled IEEE 802.15.4 with the RPL routing protocol while keeping full compliance with both standards. We provide a means for RPL to pass the routing information to Layer 2 before the 802.15.4 topology is created by encapsulating RPL DIO messages in beacon frames. The scheme takes advantage of 802.15.4 command frames to solicit RPL DIO messages. The effect of the command frames is to reset the Trickle timer that governs sending DIO messages. We provide a detailed analysis of the overhead incurred by the proposed scheme to understand topology construction costs. We have evaluated the scheme using Contiki and the instruction-level Cooja simulator and compared our results against the most common scheme used for dissemination of the upper-layer information in beacon-enabled PANs. The results show energy savings during the topology construction phase and in the steady state.