OpenRaiser/Intern-Atlas huggingface dataset:
Domain Types: Selecting Abstractions Based on Variable Usage
Venue: arXiv cs.SE 2013
Year: 2013

The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.
Drawing the double circle on a grid of minimum size
Venue: arXiv cs.CG 2013
Year: 2013

In 1926, Jarník introduced the problem of drawing a convex $n$-gon with vertices having integer coordinates. He constructed such a drawing in the grid $[1,c\cdot n^{3/2}]^2$ for some constant $c>0$, and showed that this grid size is optimal up to a constant factor. We consider the analogous problem for drawing the double circle, and prove that it can be done within the same grid size. Moreover, we give an O(n)-time algorithm to construct such a point set.
On the Concept of Variable Roles and its Use in Software Analysis
Venue: arXiv cs.PL 2013
Year: 2013

Human written source code in imperative programming languages exhibits typical patterns for variable use such as flags, loop iterators, counters, indices, bitvectors etc. Although it is widely understood by practitioners that these variable roles are important for automated software analysis tools, they are not systematically studied by the formal methods community, and not well documented in the research literature. In this paper, we study the notion of variable roles on the example of basic types (int, float, char) in C. We propose a classification of the variables in a program by variable roles, and demonstrate that classical data flow analysis lends itself naturally both as a specification formalism and an analysis paradigm for this classification problem. We demonstrate the practical applicability of our method by predicting membership of source files to the different categories of the software verification competition SVCOMP 2013.
Auto-similarity in rational base number systems
Venue: arXiv cs.FL 2013
Year: 2013

This work is a contribution to the study of set of the representations of integers in a rational base number system. This prefix-closed subset of the free monoid is naturally represented as a highly non regular tree whose nodes are the integers and whose subtrees are all distinct. With every node of that tree is then associated a minimal infinite word. The main result is that a sequential transducer which computes for all n the minimal word associated with n+1 from the one associated with n, has essentially the same underlying graph as the tree itself. These infinite words are then interpreted as representations of real numbers; the difference between the numbers represented by these two consecutive minimal words is the called the span of a node of the tree. The preceding construction allows to characterise the topological closure of the set of spans.
Modèle multi-échelles pour les services dans les VANET
Venue: arXiv cs.NI 2013
Year: 2013

Service deployment, integration and interactions in VANET are fast expanding. They are now focusing only on driver security. In the future, with in-car application deployments, the car will be considered as a user extension - in the same way as smartphones actually. We propose a multi-level graph model to challenge this VANET / Application / User integration.
An adaptive time integration strategy based on displacement history curvature
Venue: arXiv cs.NA 2013
Year: 2013

This work introduces a time-adaptive strategy that uses a refinement estimator based on the first Frenet curvature. In dynamics, a time-adaptive strategy is a mechanism that interactively proposes changes to the time step used in iterative methods of solution. These changes aim to improve the relation between quality of response and computational cost. The method here proposed is suitable for a variety of numerical time integration problems, e.g., in the study of bodies subjected to dynamical loads. The motion equation in its space-discrete form is used as reference to derive the formulation presented in this paper. Our method is contrasted with other ones based on local error estimator and apparent frequencies. We check the performance of our proposal when employed with the central difference, the explicit generalized-alpha and the Chung-Lee integration methods. The proposed refinement estimator demands low computational resources, being easily applied to several direct integration methods.
Design and Realization of a Scalable Simulator of Magnetic Resonance Tomography
Venue: arXiv cs.DC 2013
Year: 2013

In research activities regarding Magnetic Resonance Imaging in medicine, simulation tools with a universal approach are rare. Usually, simulators are developed and used which tend to be restricted to a particular, small range of applications. This led to the design and implementation of a new simulator PARSPIN, the subject of this thesis. In medical applications, the Bloch equation is a well-suited mathematical model of the underlying physics with a wide scope. In this thesis, it is shown how analytical solutions of the Bloch equation can be found, which promise substantial execution time advantages over numerical solution methods. From these analytical solutions of the Bloch equation, a new formalism for the description and the analysis of complex imaging experiments is derived, the K-t formalism. It is shown that modern imaging methods can be better explained by the K-t formalism than by observing and analysing the magnetization of each spin of a spin ensemble. Various approaches for a numerical simulation of Magnetic Resonance imaging are discussed. It is shown that a simulation tool based on the K-t formalism promises a substantial gain in execution time. Proper spatial discretization according to the sampling theorem, a topic rarely discussed in literature, is universally derived from the K-t formalism in this thesis. A spin-based simulator is an application with high demands to computing facilities even on modern hardware. In this thesis, two approaches for a parallelized software architecture are designed, analysed and evaluated with regard to a reduction of execution time. A number of possible applications in research and education are demonstrated. For a choice of imaging experiments, results produced both experimentally and by simulation are compared.
Resolution-aware network coded storage
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we show that coding can be used in storage area networks (SANs) to improve various quality of service metrics under normal SAN operating conditions, without requiring additional storage space. For our analysis, we develop a model which captures modern characteristics such as constrained I/O access bandwidth limitations. Using this model, we consider two important cases: single-resolution (SR) and multi-resolution (MR) systems. For SR systems, we use blocking probability as the quality of service metric and propose the network coded storage (NCS) scheme as a way to reduce blocking probability. The NCS scheme codes across file chunks in time, exploiting file striping and file duplication. Under our assumptions, we illustrate cases where SR NCS provides an order of magnitude savings in blocking probability. For MR systems, we introduce saturation probability as a quality of service metric to manage multiple user types, and we propose the uncoded resolution- aware storage (URS) and coded resolution-aware storage (CRS) schemes as ways to reduce saturation probability. In MR URS, we align our MR layout strategy with traffic requirements. In MR CRS, we code videos across MR layers. Under our assumptions, we illustrate that URS can in some cases provide an order of magnitude gain in saturation probability over classic non-resolution aware systems. Further, we illustrate that CRS provides additional saturation probability savings over URS.
Coexistence and Interference Mitigation for Wireless Body Area Networks: Improvements using On-Body Opportunistic Relaying
Venue: arXiv cs.NI 2013
Year: 2013

Coexistence, and hence interference mitigation, across multiple wireless body area networks (WBANs) is an important problem as WBANs become more pervasive. Here, two-hop relay-assisted cooperative communications using opportunistic relaying (OR) is proposed for enhancement of coexistence for WBANs. Suitable time division multiple access (TDMA) schemes are employed for both intra-WBAN and inter-WBANs access protocols. To emulate actual conditions of WBAN use, extensive on-body and inter-body "everyday" channel measurements are employed. In addition, a realistic inter-WBAN channel model is simulated to investigate the effect of body shadowing and hub location on WBAN performance in enabling coexistence. When compared with single-link communications, it is found that opportunistic relaying can provide significant improvement, in terms of signal-to-interference+noise ratio (SINR), to outage probability and level crossing rate (LCR) into outages. However, average outage duration (AOD) is not affected. In addition a lognormal distribution shows a better fit to received SINR when the channel coherence time is small, and a Nakagami-m distribution is a more common fit when the channel is more stable. According to the estimated SINR distributions, theoretical outage probability, LCR and AOD are shown to match the empirical results well.
Predicting the Severity of Breast Masses with Data Mining Methods
Venue: arXiv cs.LG 2013
Year: 2013

Mammography is the most effective and available tool for breast cancer screening. However, the low positive predictive value of breast biopsy resulting from mammogram interpretation leads to approximately 70% unnecessary biopsies with benign outcomes. Data mining algorithms could be used to help physicians in their decisions to perform a breast biopsy on a suspicious lesion seen in a mammogram image or to perform a short term follow-up examination instead. In this research paper data mining classification algorithms; Decision Tree (DT), Artificial Neural Network (ANN), and Support Vector Machine (SVM) are analyzed on mammographic masses data set. The purpose of this study is to increase the ability of physicians to determine the severity (benign or malignant) of a mammographic mass lesion from BI-RADS attributes and the patient,s age. The whole data set is divided for training the models and test them by the ratio of 70:30% respectively and the performances of classification algorithms are compared through three statistical measures; sensitivity, specificity, and classification accuracy. Accuracy of DT, ANN and SVM are 78.12%, 80.56% and 81.25% of test samples respectively. Our analysis shows that out of these three classification models SVM predicts severity of breast cancer with least error rate and highest accuracy.
Test cost and misclassification cost trade-off using reframing
Venue: arXiv cs.LG 2013
Year: 2013

Many solutions to cost-sensitive classification (and regression) rely on some or all of the following assumptions: we have complete knowledge about the cost context at training time, we can easily re-train whenever the cost context changes, and we have technique-specific methods (such as cost-sensitive decision trees) that can take advantage of that information. In this paper we address the problem of selecting models and minimising joint cost (integrating both misclassification cost and test costs) without any of the above assumptions. We introduce methods and plots (such as the so-called JROC plots) that can work with any off-the-shelf predictive technique, including ensembles, such that we reframe the model to use the appropriate subset of attributes (the feature configuration) during deployment time. In other words, models are trained with the available attributes (once and for all) and then deployed by setting missing values on the attributes that are deemed ineffective for reducing the joint cost. As the number of feature configuration combinations grows exponentially with the number of features we introduce quadratic methods that are able to approximate the optimal configuration and model choices, as shown by the experimental results.
Memory Implementations - Current Alternatives
Venue: arXiv cs.AI 2013
Year: 2013

Memory can be defined as the ability to retain and recall information in a diverse range of forms. It is a vital component of the way in which we as human beings operate on a day to day basis. Given a particular situation, decisions are made and actions undertaken in response to that situation based on our memory of related prior events and experiences. By utilising our memory we can anticipate the outcome of our chosen actions to avoid unexpected or unwanted events. In addition, as we subtly alter our actions and recognise altered outcomes we learn and create new memories, enabling us to improve the efficiency of our actions over time. However, as this process occurs so naturally in the subconscious its importance is often overlooked.
Immune System Approaches to Intrusion Detection - A Review (ICARIS)
Venue: arXiv cs.CR 2013
Year: 2013

The use of artificial immune systems in intrusion detection is an appealing concept for two reasons. Firstly, the human immune system provides the human body with a high level of protection from invading pathogens, in a robust, self-organised and distributed manner. Secondly, current techniques used in computer security are not able to cope with the dynamic and increasingly complex nature of computer systems and their security. It is hoped that biologically inspired approaches in this area, including the use of immune-based systems will be able to meet this challenge. Here we collate the algorithms used, the development of the systems and the outcome of their implementation. It provides an introduction and review of the key developments within this field, in addition to making suggestions for future research.
Investigating Mathematical Models of Immuno-Interactions with Early-Stage Cancer under an Agent-Based Modelling Perspective
Venue: arXiv cs.CE 2013
Year: 2013

Many advances in research regarding immuno-interactions with cancer were developed with the help of ordinary differential equation (ODE) models. These models, however, are not effectively capable of representing problems involving individual localisation, memory and emerging properties, which are common characteristics of cells and molecules of the immune system. Agent-based modelling and simulation is an alternative paradigm to ODE models that overcomes these limitations. In this paper we investigate the potential contribution of agent-based modelling and simulation when compared to ODE modelling and simulation. We seek answers to the following questions: Is it possible to obtain an equivalent agent-based model from the ODE formulation? Do the outcomes differ? Are there any benefits of using one method compared to the other? To answer these questions, we have considered three case studies using established mathematical models of immune interactions with early-stage cancer. These case studies were re-conceptualised under an agent-based perspective and the simulation results were then compared with those from the ODE models. Our results show that it is possible to obtain equivalent agent-based models (i.e. implementing the same mechanisms); the simulation output of both types of models however might differ depending on the attributes of the system to be modelled. In some cases, additional insight from using agent-based modelling was obtained. Overall, we can confirm that agent-based modelling is a useful addition to the tool set of immunologists, as it has extra features that allow for simulations with characteristics that are closer to the biological phenomena.
Draw a line on your PDA to authenticate
Venue: arXiv cs.CR 2013
Year: 2013

The trend toward a highly mobile workforce and the ubiquity of graphical interfaces (such as the stylus and touch-screen) has enabled the emergence of graphical authentications in Personal Digital Assistants (PDAs) [1]. However, most of the current graphical password schemes are vulnerable to shoulder-surfing [2,3], a known risk where an attacker can capture a password by direct observation or by recording the authentication session. Several approaches have been developed to deal with this problem, but they have significant usability drawbacks, usually in the time and effort to log in, making them less suitable for authentication [4, 8]. For example, it is time-consuming for users to log in CHC [4] and there are complex text memory requirements in scheme proposed by Hong [5]. With respect to the scheme proposed by Weinshall [6], not only is it intricate to log in, but also the main claim of resisting shoulder-surfing is proven false [7]. In this paper, we introduce a new graphical password scheme which provides a good resistance to shouldersurfing and preserves a desirable usability.
Analysis and Evaluation of the Link and Content Based Focused Treasure-Crawler
Venue: arXiv cs.IR 2013
Year: 2013

Indexing the Web is becoming a laborious task for search engines as the Web exponentially grows in size and distribution. Presently, the most effective known approach to overcome this problem is the use of focused crawlers. A focused crawler applies a proper algorithm in order to detect the pages on the Web that relate to its topic of interest. For this purpose we proposed a custom method that uses specific HTML elements of a page to predict the topical focus of all the pages that have an unvisited link within the current page. These recognized on-topic pages have to be sorted later based on their relevance to the main topic of the crawler for further actual downloads. In the Treasure-Crawler, we use a hierarchical structure called the T-Graph which is an exemplary guide to assign appropriate priority score to each unvisited link. These URLs will later be downloaded based on this priority. This paper outlines the architectural design and embodies the implementation, test results and performance evaluation of the Treasure-Crawler system. The Treasure-Crawler is evaluated in terms of information retrieval criteria such as recall and precision, both with values close to 0.5. Gaining such outcome asserts the significance of the proposed approach.
Analysis of Mismatched Estimation Errors Using Gradients of Partition Functions
Venue: arXiv cs.IT 2013
Year: 2013

We consider the problem of signal estimation (denoising) from a statistical-mechanical perspective, in continuation to a recent work on the analysis of mean-square error (MSE) estimation using a direct relationship between optimum estimation and certain partition functions. The paper consists of essentially two parts. In the first part, using the aforementioned relationship, we derive single-letter expressions of the mismatched MSE of a codeword (from a randomly selected code), corrupted by a Gaussian vector channel. In the second part, we provide several examples to demonstrate phase transitions in the behavior of the MSE. These examples enable us to understand more deeply and to gather intuition regarding the roles of the real and the mismatched probability measures in creating these phase transitions.
Dominant Frequency Extraction
Venue: arXiv cs.NA 2013
Year: 2013

Time series are collected and studied extensively for the knowledge about the data source characteristics such as the trend or the spectral landscape. Some peaks in the spectral landscape correspond to dominant frequencies. The approach here is empirical: all time series are discrete and finite. Contents: Introduction. 1 Examples of periodic phenomena. 2 Algorithms and libraries. 3 Time series analysis. 4 Dominant frequency in ladar data. Conclusion. References.
Lower Bounds for RAMs and Quantifier Elimination
Venue: arXiv cs.CC 2013
Year: 2013

We are considering RAMs $N_{n}$, with wordlength $n=2^{d}$, whose arithmetic instructions are the arithmetic operations multiplication and addition modulo $2^{n}$, the unary function $ \min\lbrace 2^{x}, 2^{n}-1\rbrace$, the binary functions $\lfloor x/y\rfloor $ (with $\lfloor x/0 \rfloor =0$), $\max(x,y)$, $\min(x,y)$, and the boolean vector operations $\wedge,\vee,\neg$ defined on $0,1$ sequences of length $n$. It also has the other RAM instructions. The size of the memory is restricted only by the address space, that is, it is $2^{n}$ words. The RAMs has a finite instruction set, each instruction is encoded by a fixed natural number independently of $n$. Therefore a program $P$ can run on each machine $N_{n}$, if $n=2^{d}$ is sufficiently large. We show that there exists an $ε>0$ and a program $P$, such that it satisfies the following two conditions. (i) For all sufficiently large $n=2^{d}$, if $P$ running on $N_{n}$ gets an input consisting of two words $a$ and $b$, then, in constant time, it gives a $0,1$ output $P_{n}(a,b)$. (ii) Suppose that $Q$ is a program such that for each sufficiently large $n=2^{d}$, if $Q$, running on $N_{n}$, gets a word $a$ of length $n$ as an input, then it decides whether there exists a word $b$ of length $n$ such that $P_{n}(a,b)=0$. Then, for infinitely many positive integers $d$, there exists a word $a$ of length $n=2^{d}$, such that the running time of $Q$ on $N_{n}$ at input $a$ is at least $ε(\log d)^{\frac{1}{2}} (\log \log d)^{-1}$.
Using a bag of Words for Automatic Medical Image Annotation with a Latent Semantic
Venue: arXiv cs.IR 2013
Year: 2013

We present in this paper a new approach for the automatic annotation of medical images, using the approach of "bag-of-words" to represent the visual content of the medical image combined with text descriptors based approach tf.idf and reduced by latent semantic to extract the co-occurrence between terms and visual terms. A medical report is composed of a text describing a medical image. First, we are interested to index the text and extract all relevant terms using a thesaurus containing MeSH medical concepts. In a second phase, the medical image is indexed while recovering areas of interest which are invariant to change in scale, light and tilt. To annotate a new medical image, we use the approach of "bagof-words" to recover the feature vector. Indeed, we use the vector space model to retrieve similar medical image from the database training. The calculation of the relevance value of an image to the query image is based on the cosine function. We conclude with an experiment carried out on five types of radiological imaging to evaluate the performance of our system of medical annotation. The results showed that our approach works better with more images from the radiology of the skull.