OpenRaiser/Intern-Atlas huggingface dataset:
Formal Methods and CyberSecurity
Venue: arXiv cs.CR 2019
Year: 2019

Formal methods have been largely thought of in the context of safety-critical systems, where they have achieved major acceptance. Tens of millions of people trust their lives every day to such systems, based on formal proofs rather than ``we haven't found a bug'' (yet!). Why is ``we haven't found a bug'' an acceptable basis for systems trusted with hundreds of millions of people's personal data? This paper looks at some of the issues in CyberSecurity, and the extent to which formal methods, ranging from ``fully verified'' to better tool support, could help. Alas The Royal Society (2016) only recommended formal methods in the limited context of ``safety critical applications'': we suggest this is too limited.
Unlimited Budget Analysis of Randomised Search Heuristics
Venue: arXiv cs.NE 2019
Year: 2019

Performance analysis of all kinds of randomised search heuristics is a rapidly growing and developing field. Run time and solution quality are two popular measures of the performance of these algorithms. The focus of this paper is on the solution quality an optimisation heuristic achieves, not on the time it takes to reach this goal, setting it far apart from runtime analysis. We contribute to its further development by introducing a novel analytical framework, called unlimited budget analysis, to derive the expected fitness value after arbitrary computational steps. It has its roots in the very recently introduced approximation error analysis and bears some similarity to fixed budget analysis. We present the framework, apply it to simple mutation-based algorithms, covering both, local and global search. We provide analytical results for a number of pseudo-Boolean functions for unlimited budget analysis and compare them to results derived within the fixed budget framework for the same algorithms and functions. There are also results of experiments to compare bounds obtained in the two different frameworks with the actual observed performance. The study show that unlimited budget analysis may lead to the same or more general estimation beyond fixed budget.
Elastic Remote Methods
Venue: arXiv cs.DC 2019
Year: 2019

For distributed applications to take full advantage of cloud computing systems, we need middleware systems that allow developers to build elasticity management components right into the applications. This paper describes the design and implementation of ElasticRMI, a middleware system that (1) enables application developers to dynamically change the number of (server) objects available to handle remote method invocations with respect to the application's workload, without requiring major changes to clients (invokers) of remote methods, (2) enables flexible elastic scaling by allowing developers to use a combination of resource utilization metrics and fine-grained application-specific information like the properties of internal data structures to drive scaling decisions, (3) provides a high-level programming framework that handles elasticity at the level of classes and objects, masking low-level platform specific tasks (like provisioning VM images) from the developer, and (4) increases the portability of ElasticRMI applications across different private data centers/IaaS clouds through Apache Mesos.
Deformable Models for Surgical Simulation: A Survey
Venue: arXiv cs.CE 2019
Year: 2019

This paper presents a survey of the state-of-the-art deformable models studied in the literature concerning soft tissue deformable modeling for interactive surgical simulation. It first introduces the challenges of surgical simulation, followed by discussions and analyses on the deformable models, which are classified into three categories: the heuristic modeling methodology, continuum-mechanical methodology, and other methodologies. It also examines linear and nonlinear deformable modeling, model internal forces, and numerical time integrations, together with modeling of soft tissue anisotropy, viscoelasticity, and compressibility. Finally, various issues in the existing deformable models are discussed to outline the remaining challenges of deformable models in surgical simulation.
Multi-group connectivity structures and their implications
Venue: arXiv cs.SI 2019
Year: 2019

We investigate the implications of different forms of multi-group connectivity. Four multi-group connectivity modalities are considered: co-memberships, edge bundles, bridges, and liaison hierarchies. We propose generative models to generate these four modalities. Our models are variants of planted partition or stochastic block models conditioned under certain topological constraints. We report findings of a comparative analysis in which we evaluate these structures, controlling for their edge densities and sizes, on mean rates of information propagation, convergence times to consensus, and steady state deviations from the consensus value in the presence of noise as network size increases.
Consensus in Equilibrium: Can One Against All Decide Fairly?
Venue: arXiv cs.DC 2019
Year: 2019

Is there an equilibrium for distributed consensus when all agents except one collude to steer the decision value towards their preference? If an equilibrium exists, then an $n-1$ size coalition cannot do better by deviating from the algorithm, even if it prefers a different decision value. We show that an equilibrium exists under this condition only if the number of agents in the network is odd and the decision is binary (among two possible input values). That is, in this framework we provide a separation between binary and multi-valued consensus. Moreover, the input and output distribution must be uniform, regardless of the communication model (synchronous or asynchronous). Furthermore, we define a new problem - Resilient Input Sharing (RIS), and use it to find an {\em iff} condition for the $(n-1)$-resilient equilibrium for deterministic binary consensus, essentially showing that an equilibrium for deterministic consensus is equivalent to each agent learning all the other inputs in some strong sense. Finally, we note that $(n-2)$-resilient equilibrium for binary consensus is possible for any $n$. The case of $(n-2)$-resilient equilibrium for \emph{multi-valued} consensus is left open.
Learning Geometrically Consistent Mesh Corrections
Venue: arXiv cs.CV 2019
Year: 2019

Building good 3D maps is a challenging and expensive task, which requires high-quality sensors and careful, time-consuming scanning. We seek to reduce the cost of building good reconstructions by correcting views of existing low-quality ones in a post-hoc fashion using learnt priors over surfaces and appearance. We train a CNN model to predict the difference in inverse-depth from varying viewpoints of two meshes -- one of low quality that we wish to correct, and one of high-quality that we use as a reference. In contrast to previous work, we pay attention to the problem of excessive smoothing in corrected meshes. We address this with a suitable network architecture, and introduce a loss-weighting mechanism that emphasises edges in the prediction. Furthermore, smooth predictions result in geometrical inconsistencies. To deal with this issue, we present a loss function which penalises re-projection differences that are not due to occlusions. Our model reduces gross errors by 45.3%--77.5%, up to five times more than previous work.
An Architectural Style for Self-Adaptive Multi-Agent Systems
Venue: arXiv cs.MA 2019
Year: 2019

Modern distributed software systems often operate in dynamic environments in which operation conditions change continuously and subsystems may come and go at will, e.g. intelligent traffic management and multi-robot systems. To manage these dynamics, these systems have to self-adapt their structures and behaviors dynamically. While we have witnessed significant progress over the past decade in the manner in which such systems are designed, persistent challenges remain. In particular, dealing with distribution and decentralized control remains one of the major challenges in self-adaptive systems. This report presents an architecture style that supports software architects with designing architectures for a family of decentralized self-adaptive systems. The architecture style structures the software in a number of interacting autonomous entities (agents) that cooperatively realize the system tasks. Multi-agent systems derived from the architectural style realize flexibility (agents adapt their behavior and interactions to variable operating conditions) and openness (agents cope autonomously with other agents that enter and leave the system). The architectural style consists of five related patterns that distill domain-specific architectural knowledge derived from extensive experiences with developing various multi-agent systems. The architectural patterns are specified using pi-ADL, a formal architectural description language supporting specification of dynamic architectures. This specification provides architects with a rigorous description of the architecture elements of the patterns, their interactions and behavior. We illustrate how we have applied the architectural style with excerpts of two cases from our practice: an experimental system for anticipatory traffic routing and an industrial logistic system for automated transportation in warehouse environments.
Cross Domain Image Matching in Presence of Outliers
Venue: arXiv cs.CV 2019
Year: 2019

Cross domain image matching between image collections from different source and target domains is challenging in times of deep learning due to i) limited variation of image conditions in a training set, ii) lack of paired-image labels during training, iii) the existing of outliers that makes image matching domains not fully overlap. To this end, we propose an end-to-end architecture that can match cross domain images without labels in the target domain and handle non-overlapping domains by outlier detection. We leverage domain adaptation and triplet constraints for training a network capable of learning domain invariant and identity distinguishable representations, and iteratively detecting the outliers with an entropy loss and our proposed weighted MK-MMD. Extensive experimental evidence on Office [17] dataset and our proposed datasets Shape, Pitts-CycleGAN shows that the proposed approach yields state-of-the-art cross domain image matching and outlier detection performance on different benchmarks. The code will be made publicly available.
What You See Is What You Get? The Impact of Representation Criteria on Human Bias in Hiring
Venue: arXiv cs.HC 2019
Year: 2019

Although systematic biases in decision-making are widely documented, the ways in which they emerge from different sources is less understood. We present a controlled experimental platform to study gender bias in hiring by decoupling the effect of world distribution (the gender breakdown of candidates in a specific profession) from bias in human decision-making. We explore the effectiveness of \textit{representation criteria}, fixed proportional display of candidates, as an intervention strategy for mitigation of gender bias by conducting experiments measuring human decision-makers' rankings for who they would recommend as potential hires. Experiments across professions with varying gender proportions show that balancing gender representation in candidate slates can correct biases for some professions where the world distribution is skewed, although doing so has no impact on other professions where human persistent preferences are at play. We show that the gender of the decision-maker, complexity of the decision-making task and over- and under-representation of genders in the candidate slate can all impact the final decision. By decoupling sources of bias, we can better isolate strategies for bias mitigation in human-in-the-loop systems.
Learning to Sample: an Active Learning Framework
Venue: arXiv cs.LG 2019
Year: 2019

Meta-learning algorithms for active learning are emerging as a promising paradigm for learning the ``best'' active learning strategy. However, current learning-based active learning approaches still require sufficient training data so as to generalize meta-learning models for active learning. This is contrary to the nature of active learning which typically starts with a small number of labeled samples. The unavailability of large amounts of labeled samples for training meta-learning models would inevitably lead to poor performance (e.g., instabilities and overfitting). In our paper, we tackle these issues by proposing a novel learning-based active learning framework, called Learning To Sample (LTS). This framework has two key components: a sampling model and a boosting model, which can mutually learn from each other in iterations to improve the performance of each other. Within this framework, the sampling model incorporates uncertainty sampling and diversity sampling into a unified process for optimization, enabling us to actively select the most representative and informative samples based on an optimized integration of uncertainty and diversity. To evaluate the effectiveness of the LTS framework, we have conducted extensive experiments on three different classification tasks: image classification, salary level prediction, and entity resolution. The experimental results show that our LTS framework significantly outperforms all the baselines when the label budget is limited, especially for datasets with highly imbalanced classes. In addition to this, our LTS framework can effectively tackle the cold start problem occurring in many existing active learning approaches.
Weakly Supervised Localization Using Background Images
Venue: arXiv cs.CV 2019
Year: 2019

Weakly Supervised Object Localization (WSOL) methodsusually rely on fully convolutional networks in order to ob-tain class activation maps(CAMs) of targeted labels. How-ever, these networks always highlight the most discriminativeparts to perform the task, the located areas are much smallerthan entire targeted objects. In this work, we propose a novelend-to-end model to enlarge CAMs generated from classifi-cation models, which can localize targeted objects more pre-cisely. In detail, we add an additional module in traditionalclassification networks to extract foreground object propos-als from images without classifying them into specific cate-gories. Then we set these normalized regions as unrestrictedpixel-level mask supervision for the following classificationtask. We collect a set of images defined as Background ImageSet from the Internet. The number of them is much smallerthan the targeted dataset but surprisingly well supports themethod to extract foreground regions from different pictures.The region extracted is independent from classification task,where the extracted region in each image covers almost en-tire object rather than just a significant part. Therefore, theseregions can serve as masks to supervise the response mapgenerated from classification models to become larger andmore precise. The method achieves state-of-the-art results onCUB-200-2011 in terms of Top-1 and Top-5 localization er-ror while has a competitive result on ILSVRC2016 comparedwith other approaches.
Information Gathering in Ad-Hoc Radio Networks
Venue: arXiv cs.DS 2019
Year: 2019

In the ad-hoc radio network model, nodes communicate with their neighbors via radio signals, without knowing the topology of the graph. We study the information gathering problem, where each node has a piece of information called a rumor, and the objective is to transmit all rumors to a designated target node. We provide an O(n^1.5*polylog(n)) deteministic protocol for information gathering in ad-hoc radio networks, significantly improving the trivial bound of O(n^2).
Saliency based Semi-supervised Learning for Orbiting Satellite Tracking
Venue: arXiv cs.CV 2019
Year: 2019

The trajectory and boundary of an orbiting satellite are fundamental information for on-orbit repairing and manipulation by space robots. This task, however, is challenging owing to the freely and rapidly motion of on-orbiting satellites, the quickly varying background and the sudden change in illumination conditions. Traditional tracking usually relies on a single bounding box of the target object, however, more detailed information should be provided by visual tracking such as binary mask. In this paper, we proposed a SSLT (Saliency-based Semi-supervised Learning for Tracking) algorithm that provides both the bounding box and segmentation binary mask of target satellites at 12 frame per second without requirement of annotated data. Our method, SSLT, improves the segmentation performance by generating a saliency map based semi-supervised on-line learning approach within the initial bounding box estimated by tracking. Once a customized segmentation model has been trained, the bounding box and satellite trajectory will be refined using the binary segmentation result. Experiment using real on-orbit rendezvous and docking video from NASA (Nation Aeronautics and Space Administration), simulated satellite animation sequence from ESA (European Space Agency) and image sequences of 3D printed satellite model took in our laboratory demonstrate the robustness, versatility and fast speed of our method compared to state-of-the-art tracking and segmentation methods. Our dataset will be released for academic use in future.
Trunk Pitch Oscillations for Joint Load Redistribution in Humans and Humanoid Robots
Venue: arXiv cs.RO 2019
Year: 2019

Creating natural-looking running gaits for humanoid robots is a complex task due to the underactuated degree of freedom in the trunk, which makes the motion planning and control difficult. The research on trunk movements in human locomotion is insufficient, and no formalism is known to transfer human motion patterns onto robots. Related work mostly focuses on the lower extremities, and simplifies the problem by stabilizing the trunk at a fixed angle. In contrast, humans display significant trunk motions that follow the natural dynamics of the gait. In this work, we use a spring-loaded inverted pendulum model with a trunk (TSLIP) together with a virtual point (VP) target to create trunk oscillations and investigate the impact of these movements. We analyze how the VP location and forward speed determine the direction and magnitude of the trunk oscillations. We show that positioning the VP below the center of mass (CoM) can explain the forward trunk pitching observed in human running. The VP below the CoM leads to a synergistic work between the hip and leg, reducing the leg loading. However, it comes at the cost of increased peak hip torque. Our results provide insights for leveraging the trunk motion to redistribute joint loads and potentially improve the energy efficiency in humanoid robots.
Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical Report
Venue: arXiv cs.LO 2019
Year: 2019

I/O conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several real-time extensions of ioco, usually called tioco, have been proposed, further taking into account permitted delays between actions. In this paper, we propose an improved version of tioco, called live timed ioco (ltioco), tackling various weaknesses of existing definitions. Here, a reasonable adaptation of quiescence (i.e., observable absence of any outputs) to real-time behaviors has to be done with care: ltioco therefore distinguishes safe outputs being allowed to happen, from live outputs being enforced to happen within a certain time period thus inducing two different facets of quiescence. Furthermore, tioco is frequently defined on Timed I/O Labeled Transition Systems (TIOLTS), a semantic model of Timed I/O Automata (TIOA) which is infinitely branching and thus infeasible for practical testing tools. Instead, we extend the theory of zone graphs to enable ltioco testing on a finite semantic model of TIOA. Finally, we investigate compositionality of ltioco with respect to parallel composition including a proper treatment of silent transitions.
Self-supervised Scale Equivariant Network for Weakly Supervised Semantic Segmentation
Venue: arXiv cs.CV 2019
Year: 2019

Weakly supervised semantic segmentation has attracted much research interest in recent years considering its advantage of low labeling cost. Most of the advanced algorithms follow the design principle that expands and constrains the seed regions from class activation maps (CAM). As well-known, conventional CAM tends to be incomplete or over-activated due to weak supervision. Fortunately, we find that semantic segmentation has a characteristic of spatial transformation equivariance, which can form a few self-supervisions to help weakly supervised learning. This work mainly explores the advantages of scale equivariant constrains for CAM generation, formulated as a self-supervised scale equivariant network (SSENet). Specifically, a novel scale equivariant regularization is elaborately designed to ensure consistency of CAMs from the same input image with different resolutions. This novel scale equivariant regularization can guide the whole network to learn more accurate class activation. This regularized CAM can be embedded in most recent advanced weakly supervised semantic segmentation framework. Extensive experiments on PASCAL VOC 2012 datasets demonstrate that our method achieves the state-of-the-art performance both quantitatively and qualitatively for weakly supervised semantic segmentation. Code has been made available.
CISE3: Verificação de aplicações com consistência fraca em Why3
Venue: arXiv cs.PL 2019
Year: 2019

In this article we present a tool for the verification of programs built on top replicated databases. The tool evaluates a sequential specification and deduces which operations need to be synchronized for the program to function properly in a distributed environment. Our prototype is built over the deductive verification platform Why3. The Why3 Framework provides a sophisticated user experience, the possibility to scale to realistic case studies, as well as a high degree of automation. A case study is presented and discussed, with the purpose of experimentally validating our approach.
Juxtaposing Controlled Empirical Studies in Visualization with Topic Developments in Psychology
Venue: arXiv cs.HC 2019
Year: 2019

Empirical studies form an integral part of visualization research. Not only can they facilitate the evaluation of various designs, techniques, systems, and practices in visualization, but they can also enable the discovery of the causalities explaining why and how visualization works. This state-of-the-art report focuses on controlled and semi-controlled empirical studies conducted in laboratories and crowd-sourcing environments. In particular, the survey provides a taxonomic analysis of over 129 empirical studies in the visualization literature. It juxtaposes these studies with topic developments between 1978 and 2017 in psychology, where controlled empirical studies have played a predominant role in research. To help appreciate this broad context, the paper provides two case studies in detail, where specific visualization-related topics were examined in the discipline of psychology as well as the field of visualization. Following a brief discussion on some latest developments in psychology, it outlines challenges and opportunities in making new discoveries about visualization through empirical studies.