OpenRaiser/Intern-Atlas huggingface dataset:
Transformational Verification of Quicksort
Venue: arXiv cs.LO 2020
Year: 2020

Many transformation techniques developed for constraint logic programs, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work out a nontrivial case study through the transformation-based verification approach. We consider the familiar Quicksort program for sorting lists, written in a functional programming language, and we verify the pre/-postconditions that specify the intended correctness properties of the functions defined in the program. We verify these properties by: (1) translating them into CHCs, (2) transforming the CHCs by removing all list occurrences, and (3) checking the satisfiability of the transformed CHCs by using the Eldarica solver over booleans and integers. The transformation mentioned at Point (2) requires an extension of the algorithms for the elimination of inductively defined data structures presented in previous work, because during one stage of the transformation we use as lemmas some properties that have been proved at previous stages.
Competition Report: CHC-COMP-20
Venue: arXiv cs.LO 2020
Year: 2020

CHC-COMP-20 is the third competition of solvers for Constrained Horn Clauses. In this year, 9 solvers participated at the competition, and were evaluated in four separate tracks on problems in linear integer arithmetic, linear real arithmetic, and arrays. The competition was run in the first week of May 2020 using the StarExec computing cluster. This report gives an overview of the competition design, explains the organisation of the competition, and presents the competition results.
Deep Robust Clustering by Contrastive Learning
Venue: arXiv cs.CV 2020
Year: 2020

Recently, many unsupervised deep learning methods have been proposed to learn clustering with unlabelled data. By introducing data augmentation, most of the latest methods look into deep clustering from the perspective that the original image and its transformation should share similar semantic clustering assignment. However, the representation features could be quite different even they are assigned to the same cluster since softmax function is only sensitive to the maximum value. This may result in high intra-class diversities in the representation feature space, which will lead to unstable local optimal and thus harm the clustering performance. To address this drawback, we proposed Deep Robust Clustering (DRC). Different from existing methods, DRC looks into deep clustering from two perspectives of both semantic clustering assignment and representation feature, which can increase inter-class diversities and decrease intra-class diversities simultaneously. Furthermore, we summarized a general framework that can turn any maximizing mutual information into minimizing contrastive loss by investigating the internal relationship between mutual information and contrastive learning. And we successfully applied it in DRC to learn invariant features and robust clusters. Extensive experiments on six widely-adopted deep clustering benchmarks demonstrate the superiority of DRC in both stability and accuracy. e.g., attaining 71.6% mean accuracy on CIFAR-10, which is 7.1% higher than state-of-the-art results.
Perception Score, A Learned Metric for Open-ended Text Generation Evaluation
Venue: arXiv cs.CL 2020
Year: 2020

Automatic evaluation for open-ended natural language generation tasks remains a challenge. Existing metrics such as BLEU show a low correlation with human judgment. We propose a novel and powerful learning-based evaluation metric: Perception Score. The method measures the overall quality of the generation and scores holistically instead of only focusing on one evaluation criteria, such as word overlapping. Moreover, it also shows the amount of uncertainty about its evaluation result. By connecting the uncertainty, Perception Score gives a more accurate evaluation for the generation system. Perception Score provides state-of-the-art results on two conditional generation tasks and two unconditional generation tasks.
Orthologics for Cones
Venue: arXiv cs.AI 2020
Year: 2020

In applications that use knowledge representation (KR) techniques, in particular those that combine data-driven and logic methods, the domain of objects is not an abstract unstructured domain, but it exhibits a dedicated, deep structure of geometric objects. One example is the class of convex sets used to model natural concepts in conceptual spaces, which also links via convex optimization techniques to machine learning. In this paper we study logics for such geometric structures. Using the machinery of lattice theory, we describe an extension of minimal orthologic with a partial modularity rule that holds for closed convex cones. This logic combines a feasible data structure (exploiting convexity/conicity) with sufficient expressivity, including full orthonegation (exploiting conicity).
An integrated numerical model for coupled poro-hydro-mechanics and fracture propagation using embedded meshes
Venue: arXiv cs.CE 2020
Year: 2020

Integrated models for fluid-driven fracture propagation and general multiphase flow in porous media are valuable to the study and engineering of several systems, including hydraulic fracturing, underground disposal of waste, and geohazard mitigation across such applications. This work extends the coupled model multiphase flow and poromechanical model of \cite{ren2018embedded} to admit fracture propagation (FP). The coupled XFEM-EDFM scheme utilizes a separate fracture mesh that is embedded on a static background mesh. The onset and dynamics of fracture propagation (FP) are governed by the equivalent stress intensity factor (SIF) criterion. A domain-integral method (J integral) is applied to compute this information. An adaptive time-marching scheme is proposed to rapidly restrict and grow temporal resolution to match the underlying time-scales. The proposed model is verified with analytical solutions, and shows the capability to accurately and adaptively co-simulate fluid transport and deformation as well as the propagation of multiple fractures.
A Survey on Security and Privacy Issues in Edge Computing-Assisted Internet of Things
Venue: arXiv cs.NI 2020
Year: 2020

Internet of Things (IoT) is an innovative paradigm envisioned to provide massive applications that are now part of our daily lives. Millions of smart devices are deployed within complex networks to provide vibrant functionalities including communications, monitoring, and controlling of critical infrastructures. However, this massive growth of IoT devices and the corresponding huge data traffic generated at the edge of the network created additional burdens on the state-of-the-art centralized cloud computing paradigm due to the bandwidth and resources scarcity. Hence, edge computing (EC) is emerging as an innovative strategy that brings data processing and storage near to the end users, leading to what is called EC-assisted IoT. Although this paradigm provides unique features and enhanced quality of service (QoS), it also introduces huge risks in data security and privacy aspects. This paper conducts a comprehensive survey on security and privacy issues in the context of EC-assisted IoT. In particular, we first present an overview of EC-assisted IoT including definitions, applications, architecture, advantages, and challenges. Second, we define security and privacy in the context of EC-assisted IoT. Then, we extensively discuss the major classifications of attacks in EC-assisted IoT and provide possible solutions and countermeasures along with the related research efforts. After that, we further classify some security and privacy issues as discussed in the literature based on security services and based on security objectives and functions. Finally, several open challenges and future research directions for secure EC-assisted IoT paradigm are also extensively provided.
Extracting Backbones in Weighted Modular Complex Networks
Venue: arXiv cs.SI 2020
Year: 2020

Network science provides effective tools to model and analyze complex systems. However, the increasing size of real-world networks becomes a major hurdle in order to understand their structure and topological features. Therefore, mapping the original network into a smaller one while preserving its information is an important issue. Extracting the so-called backbone of a network is a very challenging problem that is generally handled either by coarse-graining or filter-based methods. Coarse-graining methods reduce the network size by grouping similar nodes, while filter-based methods prune the network by discarding nodes or edges based on a statistical property. In this paper, we propose and investigate two filter-based methods exploiting the overlapping community structure in order to extract the backbone in weighted networks. Indeed, highly connected nodes (hubs) and overlapping nodes are at the heart of the network. In the first method, called "overlapping nodes ego backbone", the backbone is formed simply from the set of overlapping nodes and their neighbors. In the second method, called "overlapping nodes and hubs backbone", the backbone is formed from the set of overlapping nodes and the hubs. For both methods, the links with the lowest weights are removed from the network as long as a backbone with a single connected component is preserved. Experiments have been performed on real-world weighted networks originating from various domains (social, co-appearance, collaboration, biological, and technological) and different sizes. Results show that both backbone extraction methods are quite similar. Furthermore, comparison with the most influential alternative filtering method demonstrates the greater ability of the proposed backbones extraction methods to uncover the most relevant parts of the network.
Navigating the landscape of COVID-19 research through literature analysis: A bird's eye view
Venue: arXiv cs.DL 2020
Year: 2020

Timely access to accurate scientific literature in the battle with the ongoing COVID-19 pandemic is critical. This unprecedented public health risk has motivated research towards understanding the disease in general, identifying drugs to treat the disease, developing potential vaccines, etc. This has given rise to a rapidly growing body of literature that doubles in number of publications every 20 days as of May 2020. Providing medical professionals with means to quickly analyze the literature and discover growing areas of knowledge is necessary for addressing their question and information needs. In this study we analyze the LitCovid collection, 13,369 COVID-19 related articles found in PubMed as of May 15th, 2020 with the purpose of examining the landscape of literature and presenting it in a format that facilitates information navigation and understanding. We do that by applying state-of-the-art named entity recognition, classification, clustering and other NLP techniques. By applying NER tools, we capture relevant bioentities (such as diseases, internal body organs, etc.) and assess the strength of their relationship with COVID-19 by the extent they are discussed in the corpus. We also collect a variety of symptoms and co-morbidities discussed in reference to COVID-19. Our clustering algorithm identifies topics represented by groups of related terms, and computes clusters corresponding to documents associated with the topic terms. Among the topics we observe several that persist through the duration of multiple weeks and have numerous associated documents, as well several that appear as emerging topics with fewer documents. All the tools and data are publicly available, and this framework can be applied to any literature collection. Taken together, these analyses produce a comprehensive, synthesized view of COVID-19 research to facilitate knowledge discovery from literature.
FrUITeR: A Framework for Evaluating UI Test Reuse
Venue: arXiv cs.SE 2020
Year: 2020

UI testing is tedious and time-consuming due to the manual effort required. Recent research has explored opportunities for reusing existing UI tests from an app to automatically generate new tests for other apps. However, the evaluation of such techniques currently remains manual, unscalable, and unreproducible, which can waste effort and impede progress in this emerging area. We introduce FrUITeR, a framework that automatically evaluates UI test reuse in a reproducible way. We apply FrUITeR to existing test-reuse techniques on a uniform benchmark we established, resulting in 11,917 test reuse cases from 20 apps. We report several key findings aimed at improving UI test reuse that are missed by existing work.
Performance Analysis of Cellular-V2X with Adaptive and Selective Power Control
Venue: arXiv cs.NI 2020
Year: 2020

LTE based Cellular Vehicle-To-Everything (C-V2X) allows vehicles to communicate with each other directly without the need for infrastructure and is expected to be a critical enabler for connected and autonomous vehicles. V2X communication based safety applications are built on periodic broadcast of basic safety messages with vehicle state information. Vehicles use this information to identify collision threats and take appropriate countermeasures. As the vehicle density increases, these broadcasts can congest the communication channel resulting in increased packet loss; fundamentally impacting the ability to identify threats in a timely manner. To address this issue, it is important to incorporate a congestion control mechanism. Congestion management scheme based on rate and power control has proved to be effective for DSRC. In this paper, we investigate the suitability of similar congestion control to C-V2X with particular focus on transmit power control. In our evaluation, we include periodic basic safety messages and high priority event messages that are generated when an event such as hard braking occurs. Our study reveals that while power control does not improve packet delivery performance of basic safety messages, it is beneficial to high priority event message delivery. In this paper, we investigate the reasons for this behavior using simulations and analysis.
TGK-Planner: An Efficient Topology Guided Kinodynamic Planner for Autonomous Quadrotors
Venue: arXiv cs.RO 2020
Year: 2020

In this paper, we propose a lightweight yet effective Topology Guided Kinodynamic planner (TGK-Planner) for quadrotor aggressive flights with limited onboard computing resources. The proposed system follows the traditional hierarchical planning workflow, with novel designs to improve the robustness and efficiency in both the pathfinding and trajectory optimization sub-modules. Firstly, we propose the topology guided graph, which roughly captures the topological structure of the environment and guides the state sampling of a sampling-based kinodynamic planner. In this way, we significantly improve the efficiency of finding a safe and dynamically feasible trajectory. Then, we refine the smoothness and continuity of the trajectory in an optimization framework, which incorporates the homotopy constraint to guarantee the safety of the trajectory. The optimization program is formulated as a sequence of quadratic programmings (QPs) and can be iteratively solved in a few milliseconds. Finally, the proposed system is integrated into a fully autonomous quadrotor and validated in various simulated and real-world scenarios. Benchmark comparisons show that our method outperforms state-of-the-art methods with regard to efficiency and trajectory quality. Moreover, we will release our code as an open-source package.
Visual Pattern Recognition with on On-chip Learning: towards a Fully Neuromorphic Approach
Venue: arXiv cs.NE 2020
Year: 2020

We present a spiking neural network (SNN) for visual pattern recognition with on-chip learning on neuromorphichardware. We show how this network can learn simple visual patterns composed of horizontal and vertical bars sensed by a Dynamic Vision Sensor, using a local spike-based plasticity rule. During recognition, the network classifies the pattern's identity while at the same time estimating its location and scale. We build on previous work that used learning with neuromorphic hardware in the loop and demonstrate that the proposed network can properly operate with on-chip learning, demonstrating a complete neuromorphic pattern learning and recognition setup. Our results show that the network is robust against noise on the input (no accuracy drop when adding 130% noise) and against up to 20% noise in the neuron parameters.
Optimizing Co-flows Scheduling and Routing in Data Centre Networks for Big Data Applications
Venue: arXiv cs.NI 2020
Year: 2020

This paper optimizes the scheduling and routing of the co-flows of MapReduce shuffling phase in state-of-the-art and proposed Passive Optical Networking (PON)-based Data Centre Network (DCN) architectures. A time-slotted Mixed Integer Linear Programming (MILP) model is developed and used for the optimization with the objective of minimizing either the total energy consumption or the completion time. The DCN architectures include four state-of-the-art electronic switching architectures which are spine-leaf, Fat-tree, BCube, and DCell data centres. The proposed PON-based DCN architectures include two designs that utilize ports in Optical Line Terminal (OLT) line cards for inter and possibly intra data centre networking in addition to passive interconnects for the intra data centre networking between different PON groups (i.e. racks) within a PON cell (i.e. number of PON groups connected to a single OLT port). The first design is a switch-centric design that uses two Arrayed Waveguide Grating Routers (AWGRs) and the second is a server-centric design. The study also considers different traffic patterns defined according to the distribution of map and reduce tasks in the servers and data skewness.
NASB: Neural Architecture Search for Binary Convolutional Neural Networks
Venue: arXiv cs.CV 2020
Year: 2020

Binary Convolutional Neural Networks (CNNs) have significantly reduced the number of arithmetic operations and the size of memory storage needed for CNNs, which makes their deployment on mobile and embedded systems more feasible. However, the CNN architecture after binarizing requires to be redesigned and refined significantly due to two reasons: 1. the large accumulation error of binarization in the forward propagation, and 2. the severe gradient mismatch problem of binarization in the backward propagation. Even though the substantial effort has been invested in designing architectures for single and multiple binary CNNs, it is still difficult to find an optimal architecture for binary CNNs. In this paper, we propose a strategy, named NASB, which adopts Neural Architecture Search (NAS) to find an optimal architecture for the binarization of CNNs. Due to the flexibility of this automated strategy, the obtained architecture is not only suitable for binarization but also has low overhead, achieving a better trade-off between the accuracy and computational complexity of hand-optimized binary CNNs. The implementation of NASB strategy is evaluated on the ImageNet dataset and demonstrated as a better solution compared to existing quantized CNNs. With the insignificant overhead increase, NASB outperforms existing single and multiple binary CNNs by up to 4.0% and 1.0% Top-1 accuracy respectively, bringing them closer to the precision of their full precision counterpart. The code and pretrained models will be publicly available.
A novel hand-held interface supporting the self-management of Type 1 diabetes
Venue: arXiv cs.CY 2020
Year: 2020

The paper describes the interaction design of a hand-held interface supporting the self-management of Type 1 diabetes. It addresses well-established clinical and human-computer interaction requirements. The design exploits three opportunities. One is associated with visible context, whether conspicuous or inconspicuous. A second arises from the design freedom made possible by the user's anticipated focus of attention during certain interactions. A third opportunity to provide valuable functionality arises from wearable sensors and machine learning algorithms. The resulting interface permits ``What if?'' questions: it allows a user to dynamically and manually explore predicted short-term (e.g., 2 hours) relationships between an intended meal, blood glucose level and recommended insulin dosage, and thereby readily make informed food and exercise decisions. Design activity has been informed throughout by focus groups comprising people with Type 1 diabetes in addition to experts in diabetes, interaction design and machine learning. The design is being implemented prior to a clinical trial.
Forming Local Intersections of Projections for Classifying and Searching Histopathology Images
Venue: arXiv cs.CV 2020
Year: 2020

In this paper, we propose a novel image descriptor called Forming Local Intersections of Projections (FLIP) and its multi-resolution version (mFLIP) for representing histopathology images. The descriptor is based on the Radon transform wherein we apply parallel projections in small local neighborhoods of gray-level images. Using equidistant projection directions in each window, we extract unique and invariant characteristics of the neighborhood by taking the intersection of adjacent projections. Thereafter, we construct a histogram for each image, which we call the FLIP histogram. Various resolutions provide different FLIP histograms which are then concatenated to form the mFLIP descriptor. Our experiments included training common networks from scratch and fine-tuning pre-trained networks to benchmark our proposed descriptor. Experiments are conducted on the publicly available dataset KIMIA Path24 and KIMIA Path960. For both of these datasets, FLIP and mFLIP descriptors show promising results in all experiments.Using KIMIA Path24 data, FLIP outperformed non-fine-tuned Inception-v3 and fine-tuned VGG16 and mFLIP outperformed fine-tuned Inception-v3 in feature extracting.
Tracking in Crowd is Challenging: Analyzing Crowd based on Physical Characteristics
Venue: arXiv cs.CV 2020
Year: 2020

Currently, the safety of people has become a very important problem in different places including subway station, universities, colleges, airport, shopping mall and square, city squares. Therefore, considering intelligence event detection systems is more and urgently required. The event detection method is developed to identify abnormal behavior intelligently, so public can take action as soon as possible to prevent unwanted activities. The problem is very challenging due to high crowd density in different areas. One of these issues is occlusion due to which individual tracking and analysis becomes impossible as shown in Fig. 1. Secondly, more challenging is the proper representation of individual behavior in the crowd. We consider a novel method to deal with these challenges. Considering the challenge of tracking, we partition complete frame into smaller patches, and extract motion pattern to demonstrate the motion in each individual patch. For this purpose, our work takes into account KLT corners as consolidated features to describe moving regions and track these features by considering optical flow method. To embed motion patterns, we develop and consider the distribution of all motion information in a patch as Gaussian distribution, and formulate parameters of Gaussian model as our motion pattern descriptor.