OpenRaiser/Intern-Atlas huggingface dataset:
Using Program Synthesis for Program Analysis
Venue: arXiv cs.LO 2015
Year: 2015

In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the {\it synthesis fragment}. Satisfiability of a formula in the synthesis fragment is decidable over finite domains; specifically the decision problem is NEXPTIME-complete. If a formula in this fragment is satisfiable, a solution consists of a satisfying assignment from the second order variables to \emph{functions over finite domains}. To concretely find these solutions, we synthesise \emph{programs} that compute the functions. Our program synthesis algorithm is complete for finite state programs, i.e. every \emph{function} over finite domains is computed by some \emph{program} that we can synthesise. We can therefore use our synthesiser as a decision procedure for the synthesis fragment of second-order logic, which in turn allows us to use it as a powerful backend for many program analysis tasks. To show the tractability of our approach, we evaluate the program synthesiser on several static analysis problems.
Value function approximation via low-rank models
Venue: arXiv cs.LG 2015
Year: 2015

We propose a novel value function approximation technique for Markov decision processes. We consider the problem of compactly representing the state-action value function using a low-rank and sparse matrix model. The problem is to decompose a matrix that encodes the true value function into low-rank and sparse components, and we achieve this using Robust Principal Component Analysis (PCA). Under minimal assumptions, this Robust PCA problem can be solved exactly via the Principal Component Pursuit convex optimization problem. We experiment the procedure on several examples and demonstrate that our method yields approximations essentially identical to the true function.
A Telescopic Binary Learning Machine for Training Neural Networks
Venue: arXiv cs.NE 2015
Year: 2015

This paper proposes a new algorithm based on multi-scale stochastic local search with binary representation for training neural networks. In particular, we study the effects of neighborhood evaluation strategies, the effect of the number of bits per weight and that of the maximum weight range used for mapping binary strings to real values. Following this preliminary investigation, we propose a telescopic multi-scale version of local search where the number of bits is increased in an adaptive manner, leading to a faster search and to local minima of better quality. An analysis related to adapting the number of bits in a dynamic way is also presented. The control on the number of bits, which happens in a natural manner in the proposed method, is effective to increase the generalization performance. Benchmark tasks include a highly non-linear artificial problem, a control problem requiring either feed-forward or recurrent architectures for feedback control, and challenging real-world tasks in different application domains. The results demonstrate the effectiveness of the proposed method.
Target Tracking in Confined Environments with Uncertain Sensor Positions
Venue: arXiv cs.OH 2015
Year: 2015

To ensure safety in confined environments such as mines or subway tunnels, a (wireless) sensor network can be deployed to monitor various environmental conditions. One of its most important applications is to track personnel, mobile equipment and vehicles. However, the state-of-the-art algorithms assume that the positions of the sensors are perfectly known, which is not necessarily true due to imprecise placement and/or dropping of sensors. Therefore, we propose an automatic approach for simultaneous refinement of sensors' positions and target tracking. We divide the considered area in a finite number of cells, define dynamic and measurement models, and apply a discrete variant of belief propagation which can efficiently solve this high-dimensional problem, and handle all non-Gaussian uncertainties expected in this kind of environments. Finally, we use ray-tracing simulation to generate an artificial mine-like environment and generate synthetic measurement data. According to our extensive simulation study, the proposed approach performs significantly better than standard Bayesian target tracking and localization algorithms, and provides robustness against outliers.
Robust Face Recognition via Multimodal Deep Face Representation
Venue: arXiv cs.CV 2015
Year: 2015

Face images appeared in multimedia applications, e.g., social networks and digital entertainment, usually exhibit dramatic pose, illumination, and expression variations, resulting in considerable performance degradation for traditional face recognition algorithms. This paper proposes a comprehensive deep learning framework to jointly learn face representation using multimodal information. The proposed deep learning structure is composed of a set of elaborately designed convolutional neural networks (CNNs) and a three-layer stacked auto-encoder (SAE). The set of CNNs extracts complementary facial features from multimodal data. Then, the extracted features are concatenated to form a high-dimensional feature vector, whose dimension is compressed by SAE. All the CNNs are trained using a subset of 9,000 subjects from the publicly available CASIA-WebFace database, which ensures the reproducibility of this work. Using the proposed single CNN architecture and limited training data, 98.43% verification rate is achieved on the LFW database. Benefited from the complementary information contained in multimodal data, our small ensemble system achieves higher than 99.0% recognition rate on LFW using publicly available training set.
Algorithms for Network-on-Chip Design with Guaranteed QoS
Venue: arXiv cs.NI 2015
Year: 2015

We present algorithms that design NoCs with guaranteed quality of service. Given a topology, a mapping of tasks to processing elements, and traffic requirements between the tasks, the algorithm computes the interconnection widths, a detailed static routing, and a periodic scheduling. No headers, control messages, or acknowledgments are required. The algorithm employs fractional Multi-Commodity Flow (MCF) that determines the widths of the interconnections as well as the routes of the flits. The MCF is rounded to a periodic TDM schedule which is translated to local periodic control of switches and network interfaces. Our algorithm is applicable to large instances since every stage is efficient. The algorithm supports arbitrary topologies and traffic patterns. Routing along multiple paths is allowed in order to increase utilization and decrease latency. We implemented the algorithm and tested it with the MCSL benchmark. Experiments demonstrate that our solution is stable and satisfies all the real-time constraints.
Transformée en scattering sur la spirale temps-chroma-octave
Venue: arXiv cs.SD 2015
Year: 2015

We introduce a scattering representation for the analysis and classification of sounds. It is locally translation-invariant, stable to deformations in time and frequency, and has the ability to capture harmonic structures. The scattering representation can be interpreted as a convolutional neural network which cascades a wavelet transform in time and along a harmonic spiral. We study its application for the analysis of the deformations of the source-filter model.
On Minimizing Crossings in Storyline Visualizations
Venue: arXiv cs.DS 2015
Year: 2015

In a storyline visualization, we visualize a collection of interacting characters (e.g., in a movie, play, etc.) by $x$-monotone curves that converge for each interaction, and diverge otherwise. Given a storyline with $n$ characters, we show tight lower and upper bounds on the number of crossings required in any storyline visualization for a restricted case. In particular, we show that if (1) each meeting consists of exactly two characters and (2) the meetings can be modeled as a tree, then we can always find a storyline visualization with $O(n\log n)$ crossings. Furthermore, we show that there exist storylines in this restricted case that require $Ω(n\log n)$ crossings. Lastly, we show that, in the general case, minimizing the number of crossings in a storyline visualization is fixed-parameter tractable, when parameterized on the number of characters $k$. Our algorithm runs in time $O(k!^2k\log k + k!^2m)$, where $m$ is the number of meetings.
Disaster-Resilient Control Plane Design and Mapping in Software-Defined Networks
Venue: arXiv cs.NI 2015
Year: 2015

Communication networks, such as core optical networks, heavily depend on their physical infrastructure, and hence they are vulnerable to man-made disasters, such as Electromagnetic Pulse (EMP) or Weapons of Mass Destruction (WMD) attacks, as well as to natural disasters. Large-scale disasters may cause huge data loss and connectivity disruption in these networks. As our dependence on network services increases, the need for novel survivability methods to mitigate the effects of disasters on communication networks becomes a major concern. Software-Defined Networking (SDN), by centralizing control logic and separating it from physical equipment, facilitates network programmability and opens up new ways to design disaster-resilient networks. On the other hand, to fully exploit the potential of SDN, along with data-plane survivability, we also need to design the control plane to be resilient enough to survive network failures caused by disasters. Several distributed SDN controller architectures have been proposed to mitigate the risks of overload and failure, but they are optimized for limited faults without addressing the extent of large-scale disaster failures. For disaster resiliency of the control plane, we propose to design it as a virtual network, which can be solved using Virtual Network Mapping techniques. We select appropriate mapping of the controllers over the physical network such that the connectivity among the controllers (controller-to-controller) and between the switches to the controllers (switch-to-controllers) is not compromised by physical infrastructure failures caused by disasters. We formally model this disaster-aware control-plane design and mapping problem, and demonstrate a significant reduction in the disruption of controller-to-controller and switch-to-controller communication channels using our approach.
Pinterest Board Recommendation for Twitter Users
Venue: arXiv cs.SI 2015
Year: 2015

Pinboard on Pinterest is an emerging media to engage online social media users, on which users post online images for specific topics. Regardless of its significance, there is little previous work specifically to facilitate information discovery based on pinboards. This paper proposes a novel pinboard recommendation system for Twitter users. In order to associate contents from the two social media platforms, we propose to use MultiLabel classification to map Twitter user followees to pinboard topics and visual diversification to recommend pinboards given user interested topics. A preliminary experiment on a dataset with 2000 users validated our proposed system.
Enhancement and Recognition of Reverberant and Noisy Speech by Extending Its Coherence
Venue: arXiv cs.SD 2015
Year: 2015

Most speech enhancement algorithms make use of the short-time Fourier transform (STFT), which is a simple and flexible time-frequency decomposition that estimates the short-time spectrum of a signal. However, the duration of short STFT frames are inherently limited by the nonstationarity of speech signals. The main contribution of this paper is a demonstration of speech enhancement and automatic speech recognition in the presence of reverberation and noise by extending the length of analysis windows. We accomplish this extension by performing enhancement in the short-time fan-chirp transform (STFChT) domain, an overcomplete time-frequency representation that is coherent with speech signals over longer analysis window durations than the STFT. This extended coherence is gained by using a linear model of fundamental frequency variation of voiced speech signals. Our approach centers around using a single-channel minimum mean-square error log-spectral amplitude (MMSE-LSA) estimator proposed by Habets, which scales coefficients in a time-frequency domain to suppress noise and reverberation. In the case of multiple microphones, we preprocess the data with either a minimum variance distortionless response (MVDR) beamformer, or a delay-and-sum beamformer (DSB). We evaluate our algorithm on both speech enhancement and recognition tasks for the REVERB challenge dataset. Compared to the same processing done in the STFT domain, our approach achieves significant improvement in terms of objective enhancement metrics (including PESQ---the ITU-T standard measurement for speech quality). In terms of automatic speech recognition (ASR) performance as measured by word error rate (WER), our experiments indicate that the STFT with a long window is more effective for ASR.
Achieving Energy Efficiency for Altruistic DISH: Three Properties
Venue: arXiv cs.NI 2015
Year: 2015

In an altruistic DISH protocol, additional nodes called "altruists" are deployed in a multi-channel ad hoc network to achieve energy efficiency while still maintaining the original throughput-delay performance. The responsibility of altruists is to constantly monitor the control channel and awaken other (normal) nodes when necessary (to perform data transmissions). Altruists never sleep while other nodes sleep as far as possible. This technical report proves three properties related to this cooperative protocol. The first is the conditions for forming an unsafe pair (UP) in an undirected graph. The second is the necessary and sufficient conditions for full cooperation coverage to achieve the void of multi-channel coordination (MCC) problems. The last is the NP-hardness of determining the minimum number and locations of altruistic nodes to achieve full cooperation coverage.
Backhaul-Aware Caching Placement for Wireless Networks
Venue: arXiv cs.IT 2015
Year: 2015

As the capacity demand of mobile applications keeps increasing, the backhaul network is becoming a bottleneck to support high quality of experience (QoE) in next-generation wireless networks. Content caching at base stations (BSs) is a promising approach to alleviate the backhaul burden and reduce user-perceived latency. In this paper, we consider a wireless caching network where all the BSs are connected to a central controller via backhaul links. In such a network, users can obtain the required data from candidate BSs if the data are pre-cached. Otherwise, the user data need to be first retrieved from the central controller to local BSs, which introduces extra delay over the backhaul. In order to reduce the download delay, the caching placement strategy needs to be optimized. We formulate such a design problem as the minimization of the average download delay over user requests, subject to the caching capacity constraint of each BS. Different from existing works, our model takes BS cooperation in the radio access into consideration and is fully aware of the propagation delay on the backhaul links. The design problem is a mixed integer programming problem and is highly complicated, and thus we relax the problem and propose a low-complexity algorithm. Simulation results will show that the proposed algorithm can effectively determine the near-optimal caching placement and provide significant performance gains over conventional caching placement strategies.
On Normalized Compression Distance and Large Malware
Venue: arXiv cs.CR 2015
Year: 2015

Normalized Compression Distance (NCD) is a popular tool that uses compression algorithms to cluster and classify data in a wide range of applications. Existing discussions of NCD's theoretical merit rely on certain theoretical properties of compression algorithms. However, we demonstrate that many popular compression algorithms don't seem to satisfy these theoretical properties. We explore the relationship between some of these properties and file size, demonstrating that this theoretical problem is actually a practical problem for classifying malware with large file sizes, and we then introduce some variants of NCD that mitigate this problem.
Constant Compositions in the Sphere Packing Bound for Classical-Quantum Channels
Venue: arXiv cs.IT 2015
Year: 2015

The sphere packing bound, in the form given by Shannon, Gallager and Berlekamp, was recently extended to classical-quantum channels, and it was shown that this creates a natural setting for combining probabilistic approaches with some combinatorial ones such as the Lovász theta function. In this paper, we extend the study to the case of constant composition codes. We first extend the sphere packing bound for classical-quantum channels to this case, and we then show that the obtained result is related to a variation of the Lovász theta function studied by Marton. We then propose a further extension to the case of varying channels and codewords with a constant conditional composition given a particular sequence. This extension is then applied to auxiliary channels to deduce a bound which can be interpreted as an extension of the Elias bound.
Recognizing Weighted Disk Contact Graphs
Venue: arXiv cs.CG 2015
Year: 2015

Disk contact representations realize graphs by mapping vertices bijectively to interior-disjoint disks in the plane such that two disks touch each other if and only if the corresponding vertices are adjacent in the graph. Deciding whether a vertex-weighted planar graph can be realized such that the disks' radii coincide with the vertex weights is known to be NP-hard. In this work, we reduce the gap between hardness and tractability by analyzing the problem for special graph classes. We show that it remains NP-hard for outerplanar graphs with unit weights and for stars with arbitrary weights, strengthening the previous hardness results. On the positive side, we present constructive linear-time recognition algorithms for caterpillars with unit weights and for embedded stars with arbitrary weights.
A Big Data Analyzer for Large Trace Logs
Venue: arXiv cs.DC 2015
Year: 2015

Current generation of Internet-based services are typically hosted on large data centers that take the form of warehouse-size structures housing tens of thousands of servers. Continued availability of a modern data center is the result of a complex orchestration among many internal and external actors including computing hardware, multiple layers of intricate software, networking and storage devices, electrical power and cooling plants. During the course of their operation, many of these components produce large amounts of data in the form of event and error logs that are essential not only for identifying and resolving problems but also for improving data center efficiency and management. Most of these activities would benefit significantly from data analytics techniques to exploit hidden statistical patterns and correlations that may be present in the data. The sheer volume of data to be analyzed makes uncovering these correlations and patterns a challenging task. This paper presents BiDAl, a prototype Java tool for log-data analysis that incorporates several Big Data technologies in order to simplify the task of extracting information from data traces produced by large clusters and server farms. BiDAl provides the user with several analysis languages (SQL, R and Hadoop MapReduce) and storage backends (HDFS and SQLite) that can be freely mixed and matched so that a custom tool for a specific task can be easily constructed. BiDAl has a modular architecture so that it can be extended with other backends and analysis languages in the future. In this paper we present the design of BiDAl and describe our experience using it to analyze publicly-available traces from Google data clusters, with the goal of building a realistic model of a complex data center.
Combinatorial Properties of Triangle-Free Rectangle Arrangements and the Squarability Problem
Venue: arXiv cs.CG 2015
Year: 2015

We consider arrangements of axis-aligned rectangles in the plane. A geometric arrangement specifies the coordinates of all rectangles, while a combinatorial arrangement specifies only the respective intersection type in which each pair of rectangles intersects. First, we investigate combinatorial contact arrangements, i.e., arrangements of interior-disjoint rectangles, with a triangle-free intersection graph. We show that such rectangle arrangements are in bijection with the 4-orientations of an underlying planar multigraph and prove that there is a corresponding geometric rectangle contact arrangement. Moreover, we prove that every triangle-free planar graph is the contact graph of such an arrangement. Secondly, we introduce the question whether a given rectangle arrangement has a combinatorially equivalent square arrangement. In addition to some necessary conditions and counterexamples, we show that rectangle arrangements pierced by a horizontal line are squarable under certain sufficient conditions.
Energy Harvesting Transmitters that Heat Up: Throughput Maximization under Temperature Constraints
Venue: arXiv cs.IT 2015
Year: 2015

Motivated by damage due to heating in sensor operation, we consider the throughput optimal offline data scheduling problem in an energy harvesting transmitter such that the resulting temperature increase remains below a critical level. We model the temperature dynamics of the transmitter as a linear system and determine the optimal transmit power policy under such temperature constraints as well as energy harvesting constraints over an AWGN channel. We first derive the structural properties of the solution for the general case with multiple energy arrivals. We show that the optimal power policy is piecewise monotone decreasing with possible jumps at the energy harvesting instants. We derive analytical expressions for the optimal solution in the single energy arrival case. We show that, in the single energy arrival case, the optimal power is monotone decreasing, the resulting temperature is monotone increasing, and both remain constant after the temperature hits the critical level. We then generalize the solution for the multiple energy arrival case.
Exploiting Challenges of Sub-20 nm CMOS for Affordable Technology Scaling
Venue: arXiv cs.ET 2015
Year: 2015

For the past four decades, cost and features have driven CMOS scaling. Severe lithography and material limitations seen below the 20 nm node, however, are challenging the fundamental premise of affordable CMOS scaling. Just continuing to co-optimize leaf cell circuit and layout designs with process technology does not enable us to exploit the challenges of a sub-20 nm CMOS. For affordable scaling it is imperative to work past sub-20 nm technology impediments while exploiting its features. To this end, we propose to broaden the scope of design technology co-optimization (DTCO) to be more holistic by including micro-architecture design and CAD, along with circuits, layout and process technology. Applying such holistic DTCO to the most significant block in a system-on-chip (SoC), embedded memory, we can synthesize smarter and efficient embedded memory blocks that are customized to application needs. To evaluate the efficacy of the proposed holistic DTCO process, we designed, fabricated and tested several design experiments in a state-of-the-art IBM 14SOI process. DTCOed leaf cells, standard cells and SRAM bitcells were robust during testing, but failed to meet node to node area scaling requirements. Holistic DTCO, when applied to a widely used parallel access SRAM sub-block, consumed 25% less area with a 50% better performance per watt compared to a traditional implementation using compiled SRAM blocks and standard cells. To extend the benefits of holistic DTCO to other embedded memory intensive sub-blocks in SoCs, we developed a readily customizable smart memory synthesis framework (SMSF). We believe that such an approach is important to establish an affordable path for sub-20 nm scaling.