OpenRaiser/Intern-Atlas huggingface dataset:
Stepwise Debugging of Answer-Set Programs
Venue: arXiv cs.AI 2017
Year: 2017

We introduce a stepping methodology for answer-set programming (ASP) that allows for debugging answer-set programs and is based on the stepwise application of rules. Similar to debugging in imperative languages, where the behaviour of a program is observed during a step-by-step execution, stepping for ASP allows for observing the effects that rule applications have in the computation of an answer set. While the approach is inspired from debugging in imperative programming, it is conceptually different to stepping in other paradigms due to non-determinism and declarativity that are inherent to ASP. In particular, unlike statements in an imperative program that are executed following a strict control flow, there is no predetermined order in which to consider rules in ASP during a computation. In our approach, the user is free to decide which rule to consider active in the next step following his or her intuition. This way, one can focus on interesting parts of the debugging search space. Bugs are detected during stepping by revealing differences between the actual semantics of the program and the expectations of the user. As a solid formal basis for stepping, we develop a framework of computations for answer-set programs. For fully supporting different solver languages, we build our framework on an abstract ASP language that is sufficiently general to capture different solver languages. To this end, we make use of abstract constraints as an established abstraction for popular language constructs such as aggregates. Stepping has been implemented in SeaLion, an integrated development environment for ASP. We illustrate stepping using an example scenario and discuss the stepping plugin of SeaLion. Moreover, we elaborate on methodological aspects and the embedding of stepping in the ASP development process.
An evidential Markov decision making model
Venue: arXiv cs.AI 2017
Year: 2017

The sure thing principle and the law of total probability are basic laws in classic probability theory. A disjunction fallacy leads to the violation of these two classical laws. In this paper, an Evidential Markov (EM) decision making model based on Dempster-Shafer (D-S) evidence theory and Markov modelling is proposed to address this issue and model the real human decision-making process. In an evidential framework, the states are extended by introducing an uncertain state which represents the hesitance of a decision maker. The classical Markov model can not produce the disjunction effect, which assumes that a decision has to be certain at one time. However, the state is allowed to be uncertain in the EM model before the final decision is made. An extra uncertainty degree parameter is defined by a belief entropy, named Deng entropy, to assignment the basic probability assignment of the uncertain state, which is the key to predict the disjunction effect. A classical categorization decision-making experiment is used to illustrate the effectiveness and validity of EM model. The disjunction effect can be well predicted and the free parameters are less compared with the existing models.
Opportunities in Software Engineering Research for Web API Consumption
Venue: arXiv cs.SE 2017
Year: 2017

Nowadays, invoking third party code increasingly involves calling web services via their web APIs, as opposed to the more traditional scenario of downloading a library and invoking the library's API. However, there are also new challenges for developers calling these web APIs. In this paper, we highlight a broad set of these challenges and argue for resulting opportunities for software engineering research to support developers in consuming web APIs. We outline two specific research threads in this context: (1) web API specification curation, which enables us to know the signatures of web APIs, and (2) static analysis that is capable of extracting URLs, HTTP methods etc. of web API calls. Furthermore, we present new work on how we combine (1) and (2) to provide IDE support for application developers consuming web APIs. As web APIs are used broadly, research in supporting the consumption of web APIs offers exciting opportunities.
Who you gonna call? Analyzing Web Requests in Android Applications
Venue: arXiv cs.SE 2017
Year: 2017

Relying on ubiquitous Internet connectivity, applications on mobile devices frequently perform web requests during their execution. They fetch data for users to interact with, invoke remote functionalities, or send user-generated content or meta-data. These requests collectively reveal common practices of mobile application development, like what external services are used and how, and they point to possible negative effects like security and privacy violations, or impacts on battery life. In this paper, we assess different ways to analyze what web requests Android applications make. We start by presenting dynamic data collected from running 20 randomly selected Android applications and observing their network activity. Next, we present a static analysis tool, Stringoid, that analyzes string concatenations in Android applications to estimate constructed URL strings. Using Stringoid, we extract URLs from 30, 000 Android applications, and compare the performance with a simpler constant extraction analysis. Finally, we present a discussion of the advantages and limitations of dynamic and static analyses when extracting URLs, as we compare the data extracted by Stringoid from the same 20 applications with the dynamically collected data.
Wearable Health Monitoring Using Capacitive Voltage-Mode Human Body Communication
Venue: arXiv cs.NI 2017
Year: 2017

Rapid miniaturization and cost reduction of computing, along with the availability of wearable and implantable physiological sensors have led to the growth of human Body Area Network (BAN) formed by a network of such sensors and computing devices. One promising application of such a network is wearable health monitoring where the collected data from the sensors would be transmitted and analyzed to assess the health of a person. Typically, the devices in a BAN are connected through wireless (WBAN), which suffers from energy inefficiency due to the high-energy consumption of wireless transmission. Human Body Communication (HBC) uses the relatively low loss human body as the communication medium to connect these devices, promising order(s) of magnitude better energy-efficiency and built-in security compared to WBAN. In this paper, we demonstrate a health monitoring device and system built using Commercial-Off-The- Shelf (COTS) sensors and components, that can collect data from physiological sensors and transmit it through a) intra-body HBC to another device (hub) worn on the body or b) upload health data through HBC-based human-machine interaction to an HBC capable machine. The system design constraints and signal transfer characteristics for the implemented HBC-based wearable health monitoring system are measured and analyzed, showing reliable connectivity with >8x power savings compared to Bluetooth lowenergy (BTLE).
Improving Dynamic Analysis of Android Apps Using Hybrid Test Input Generation
Venue: arXiv cs.CR 2017
Year: 2017

The Android OS has become the most popular mobile operating system leading to a significant increase in the spread of Android malware. Consequently, several static and dynamic analysis systems have been developed to detect Android malware. With dynamic analysis, efficient test input generation is needed in order to trigger the potential run-time malicious behaviours. Most existing dynamic analysis systems employ random-based input generation methods usually built using the Android Monkey tool. Random-based input generation has several shortcomings including limited code coverage, which motivates us to explore combining it with a state-based method in order to improve efficiency. Hence, in this paper, we present a novel hybrid test input generation approach designed to improve dynamic analysis on real devices. We implemented the hybrid system by integrating a random based tool (Monkey) with a state based tool (DroidBot) in order to improve code coverage and potentially uncover more malicious behaviours. The system is evaluated using 2,444 Android apps containing 1222 benign and 1222 malware samples from the Android malware genome project. Three scenarios, random only, state-based only, and our proposed hybrid approach were investigated to comparatively evaluate their performances. Our study shows that the hybrid approach significantly improved the amount of dynamic features extracted from both benign and malware samples over the state-based and commonly used random test input generation method.
Verifying Programs via Intermediate Interpretation
Venue: arXiv cs.PL 2017
Year: 2017

We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language. A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models. We show that several safety properties of functional programs modeling a class of cache coherence protocols can be proved by a supercompiler and compare the results with our earlier work on direct verification via supercompilation not using intermediate interpretation. Our approach was in part inspired by an earlier work by De E. Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs.
A General Model for Robust Tensor Factorization with Unknown Noise
Venue: arXiv cs.CV 2017
Year: 2017

Because of the limitations of matrix factorization, such as losing spatial structure information, the concept of low-rank tensor factorization (LRTF) has been applied for the recovery of a low dimensional subspace from high dimensional visual data. The low-rank tensor recovery is generally achieved by minimizing the loss function between the observed data and the factorization representation. The loss function is designed in various forms under different noise distribution assumptions, like $L_1$ norm for Laplacian distribution and $L_2$ norm for Gaussian distribution. However, they often fail to tackle the real data which are corrupted by the noise with unknown distribution. In this paper, we propose a generalized weighted low-rank tensor factorization method (GWLRTF) integrated with the idea of noise modelling. This procedure treats the target data as high-order tensor directly and models the noise by a Mixture of Gaussians, which is called MoG GWLRTF. The parameters in the model are estimated under the EM framework and through a new developed algorithm of weighted low-rank tensor factorization. We provide two versions of the algorithm with different tensor factorization operations, i.e., CP factorization and Tucker factorization. Extensive experiments indicate the respective advantages of this two versions in different applications and also demonstrate the effectiveness of MoG GWLRTF compared with other competing methods.
Why Noise and Dispersion may Seriously Hamper Nonlinear Frequency-Division Multiplexing
Venue: arXiv cs.IT 2017
Year: 2017

The performance of optical fiber systems based on nonlinear frequency-division multiplexing (NFDM) or on more conventional transmission techniques is compared through numerical simulations. Some critical issues affecting NFDM systems-namely, the strict requirements needed to avoid burst interaction due to signal dispersion and the unfavorable dependence of performance on burst length-are investigated, highlighting their potentially disruptive effect in terms of spectral efficiency. Two digital processing techniques are finally proposed to halve the guard time between NFDM symbol bursts and reduce the size of the processing window at the receiver, increasing spectral efficiency and reducing computational complexity.
Detect Kernel-Mode Rootkits via Real Time Logging & Controlling Memory Access
Venue: arXiv cs.CR 2017
Year: 2017

Modern malware and spyware platforms attack existing antivirus solutions and even Microsoft PatchGuard. To protect users and business systems new technologies developed by Intel and AMD CPUs may be applied. To deal with the new malware we propose monitoring and controlling access to the memory in real time using Intel VT-x with EPT. We have checked this concept by developing MemoryMonRWX, which is a bare-metal hypervisor. MemoryMonRWX is able to track and trap all types of memory access: read, write, and execute. MemoryMonRWX also has the following competitive advantages: fine-grained analysis, support of multi-core CPUs and 64-bit Windows 10. MemoryMonRWX is able to protect critical kernel memory areas even when PatchGuard has been disabled by malware. Its main innovative features are as follows: guaranteed interception of every memory access, resilience, and low performance degradation.
Pixel Deconvolutional Networks
Venue: arXiv cs.LG 2017
Year: 2017

Deconvolutional layers have been widely used in a variety of deep models for up-sampling, including encoder-decoder networks for semantic segmentation and deep generative models for unsupervised learning. One of the key limitations of deconvolutional operations is that they result in the so-called checkerboard problem. This is caused by the fact that no direct relationship exists among adjacent pixels on the output feature map. To address this problem, we propose the pixel deconvolutional layer (PixelDCL) to establish direct relationships among adjacent pixels on the up-sampled feature map. Our method is based on a fresh interpretation of the regular deconvolution operation. The resulting PixelDCL can be used to replace any deconvolutional layer in a plug-and-play manner without compromising the fully trainable capabilities of original models. The proposed PixelDCL may result in slight decrease in efficiency, but this can be overcome by an implementation trick. Experimental results on semantic segmentation demonstrate that PixelDCL can consider spatial features such as edges and shapes and yields more accurate segmentation outputs than deconvolutional layers. When used in image generation tasks, our PixelDCL can largely overcome the checkerboard problem suffered by regular deconvolution operations.
The Cayley-Dickson Construction in ACL2
Venue: arXiv cs.LO 2017
Year: 2017

The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensional vectors equipped with a multiplication. The construction can be used to construct, not only the two-dimensional Complex Numbers, but also the four-dimensional Quaternions and the eight-dimensional Octonions. Each of these vector spaces has a vector multiplication, v_1*v_2, that satisfies: 1. Each nonzero vector has a multiplicative inverse. 2. For the Euclidean length of a vector |v|, |v_1 * v_2| = |v_1| |v2|. Real numbers can also be viewed as (one-dimensional) vectors with the above two properties. ACL2(r) is used to explore this question: Given a vector space, equipped with a multiplication, satisfying the Euclidean length condition 2, given above. Make pairs of vectors into "new" vectors with a multiplication. When do the newly constructed vectors also satisfy condition 2?
Deep-LK for Efficient Adaptive Object Tracking
Venue: arXiv cs.CV 2017
Year: 2017

In this paper we present a new approach for efficient regression based object tracking which we refer to as Deep- LK. Our approach is closely related to the Generic Object Tracking Using Regression Networks (GOTURN) framework of Held et al. We make the following contributions. First, we demonstrate that there is a theoretical relationship between siamese regression networks like GOTURN and the classical Inverse-Compositional Lucas & Kanade (IC-LK) algorithm. Further, we demonstrate that unlike GOTURN IC-LK adapts its regressor to the appearance of the currently tracked frame. We argue that this missing property in GOTURN can be attributed to its poor performance on unseen objects and/or viewpoints. Second, we propose a novel framework for object tracking - which we refer to as Deep-LK - that is inspired by the IC-LK framework. Finally, we show impressive results demonstrating that Deep-LK substantially outperforms GOTURN. Additionally, we demonstrate comparable tracking performance to current state of the art deep-trackers whilst being an order of magnitude (i.e. 100 FPS) computationally efficient.
Prediction of Sea Surface Temperature using Long Short-Term Memory
Venue: arXiv cs.CV 2017
Year: 2017

This letter adopts long short-term memory(LSTM) to predict sea surface temperature(SST), which is the first attempt, to our knowledge, to use recurrent neural network to solve the problem of SST prediction, and to make one week and one month daily prediction. We formulate the SST prediction problem as a time series regression problem. LSTM is a special kind of recurrent neural network, which introduces gate mechanism into vanilla RNN to prevent the vanished or exploding gradient problem. It has strong ability to model the temporal relationship of time series data and can handle the long-term dependency problem well. The proposed network architecture is composed of two kinds of layers: LSTM layer and full-connected dense layer. LSTM layer is utilized to model the time series relationship. Full-connected layer is utilized to map the output of LSTM layer to a final prediction. We explore the optimal setting of this architecture by experiments and report the accuracy of coastal seas of China to confirm the effectiveness of the proposed method. In addition, we also show its online updated characteristics.
QuickTalk: An Association-Free Communication Method for IoT Devices in Proximity
Venue: arXiv cs.NI 2017
Year: 2017

IoT devices are in general considered to be straightforward to use. However, we find that there are a number of situations where the usability becomes poor. The situations include but not limited to the followings: 1) when initializing an IoT device, 2) when trying to control an IoT device which is initialized and registered by another person, and 3) when trying to control an IoT device out of many of the same type. We tackle these situations by proposing a new association-free communication method, QuickTalk. QuickTalk lets a user device such as a smartphone pinpoint and activate an IoT device with the help of an IR transmitter and communicate with the pinpointed IoT device through the broadcast channel of WiFi. By the nature of its association-free communication, QuickTalk allows a user device to immediately give a command to a specific IoT device in proximity even when the IoT device is uninitialized, unregistered to the control interface of the user, or registered but being physically confused with others. Our experiments of QuickTalk implemented on Raspberry Pi 2 devices show that the end-to-end delay of QuickTalk is upper bounded by 2.5 seconds and its median is only about 0.74 seconds. We further confirm that even when an IoT device has ongoing data sessions, QuickTalk can still establish a reliable communication channel to the IoT device with little impact to the ongoing sessions.
Local Shape Spectrum Analysis for 3D Facial Expression Recognition
Venue: arXiv cs.CV 2017
Year: 2017

We investigate the problem of facial expression recognition using 3D data. Building from one of the most successful frameworks for facial analysis using exclusively 3D geometry, we extend the analysis from a curve-based representation into a spectral representation, which allows a complete description of the underlying surface that can be further tuned to the desired level of detail. Spectral representations are based on the decomposition of the geometry in its spatial frequency components, much like a Fourier transform, which are related to intrinsic characteristics of the surface. In this work, we propose the use of Graph Laplacian Features (GLF), which results from the projection of local surface patches into a common basis obtained from the Graph Laplacian eigenspace. We test the proposed approach in the BU-3DFE database in terms of expressions and Action Units recognition. Our results confirm that the proposed GLF produces consistently higher recognition rates than the curves-based approach, thanks to a more complete description of the surface, while requiring a lower computational complexity. We also show that the GLF outperform the most popular alternative approach for spectral representation, Shape- DNA, which is based on the Laplace Beltrami Operator and cannot provide a stable basis that guarantee that the extracted signatures for the different patches are directly comparable.
Optimized Certificate Revocation List Distribution for Secure V2X Communications
Venue: arXiv cs.CR 2017
Year: 2017

The successful deployment of safe and trustworthy Connected and Autonomous Vehicles (CAVs) will highly depend on the ability to devise robust and effective security solutions to resist sophisticated cyber attacks and patch up critical vulnerabilities. Pseudonym Public Key Infrastructure (PPKI) is a promising approach to secure vehicular networks as well as ensure data and location privacy, concealing the vehicles' real identities. Nevertheless, pseudonym distribution and management affect PPKI scalability due to the significant number of digital certificates required by a single vehicle. In this paper, we focus on the certificate revocation process and propose a versatile and low-complexity framework to facilitate the distribution of the Certificate Revocation Lists (CRL) issued by the Certification Authority (CA). CRL compression is achieved through optimized Bloom filters, which guarantee a considerable overhead reduction with a configurable rate of false positives. Our results show that the distribution of compressed CRLs can significantly enhance the system scalability without increasing the complexity of the revocation process.
Beam Design and User Scheduling for Non-Orthogonal Multiple Access with Multiple Antennas Based on Pareto-Optimality
Venue: arXiv cs.IT 2017
Year: 2017

In this paper, an efficient transmit beam design and user scheduling method is proposed for multi-user (MU) multiple-input single-output (MISO) non-orthogonal multiple access (NOMA) downlink, based on Pareto-optimality. The proposed beam design and user scheduling method groups simultaneously-served users into multiple clusters with practical two users in each cluster, and then applies spatical zeroforcing (ZF) across clusters to control inter-cluster interference (ICI) and Pareto-optimal beam design with successive interference cancellation (SIC) to two users in each cluster to remove interference to strong users and leverage signal-to-interference-plus-noise ratios (SINRs) of interference-experiencing weak users. The proposed method has flexibility to control the rates of strong and weak users and numerical results show that the proposed method yields good performance.
A High-Performance Algorithm for Identifying Frequent Items in Data Streams
Venue: arXiv cs.DS 2017
Year: 2017

Estimating frequencies of items over data streams is a common building block in streaming data measurement and analysis. Misra and Gries introduced their seminal algorithm for the problem in 1982, and the problem has since been revisited many times due its practicality and applicability. We describe a highly optimized version of Misra and Gries' algorithm that is suitable for deployment in industrial settings. Our code is made public via an open source library called DataSketches that is already used by several companies and production systems. Our algorithm improves on two theoretical and practical aspects of prior work. First, it handles weighted updates in amortized constant time, a common requirement in practice. Second, it uses a simple and fast method for merging summaries that asymptotically improves on prior work even for unweighted streams. We describe experiments confirming that our algorithms are more efficient than prior proposals.