OpenRaiser/Intern-Atlas huggingface dataset:
The Design and Implementation of Typed Scheme: From Scripts to Programs
Venue: arXiv cs.PL 2011
Year: 2011

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of explicit type annotations in typical scripting languages forces programmers to must (re)discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants. This paper presents Typed Scheme, an explicitly typed extension of PLT Scheme, an untyped scripting language. Its type system is based on the novel notion of occurrence typing, which we formalize and mechanically prove sound. The implementation of Typed Scheme additionally borrows elements from a range of approaches, including recursive types, true unions and subtyping, plus polymorphism combined with a modicum of local inference. The formulation of occurrence typing naturally leads to a simple and expressive version of predicates to describe refinement types. A Typed Scheme program can use these refinement types to keep track of arbitrary classes of values via the type system. Further, we show how the Typed Scheme type system, in conjunction with simple recursive types, is able to encode refinements of existing datatypes, thus expressing both proposed variations of refinement types.
Approximating the Closest Vector Problem Using an Approximate Shortest Vector Oracle
Venue: arXiv cs.DS 2011
Year: 2011

We give a polynomial time Turing reduction from the $γ^2\sqrt{n}$-approximate closest vector problem on a lattice of dimension $n$ to a $γ$-approximate oracle for the shortest vector problem. This is an improvement over a reduction by Kannan, which achieved $γ^2n^{3/2}$.
Using Bounded Model Checking to Focus Fixpoint Iterations
Venue: arXiv cs.PL 2011
Year: 2011

Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.
QIS-XML: An Extensible Markup Language for Quantum Information Science
Venue: arXiv cs.SE 2011
Year: 2011

This Master thesis examines issues of interoperability and integration between the Classic Information Science (CIS) and Quantum Information Science (QIS). It provides a short introduction to the Extensible Markup Language (XML) and proceeds to describe the development steps that have lead to a prototype XML specification for quantum computing (QIS-XML). QIS-XML is a proposed framework, based on the widely used standard (XML) to describe, visualize, exchange and process quantum gates and quantum circuits. It also provides a potential approach to a generic programming language for quantum computers through the concept of XML driven compilers. Examples are provided for the description of commonly used quantum gates and circuits, accompanied with tools to visualize them in standard web browsers. An algorithmic example is also presented, performing a simple addition operation with quantum circuits and running the program on a quantum computer simulator. Overall, this initial effort demonstrates how XML technologies could be at the core of the architecture for describing and programming quantum computers. By leveraging a widely accepted standard, QIS-XML also builds a bridge between classic and quantum IT, which could foster the acceptance of QIS by the ICT community and facilitate the understanding of quantum technology by IT experts. This would support the consolidation of Classic Information Science and Quantum Information Science into a Complete Information Science, a challenge that could be referred to as the "Information Science Grand Unification Challenge".
Generating Schemata of Resolution Proofs
Venue: arXiv cs.AI 2011
Year: 2011

Two distinct algorithms are presented to extract (schemata of) resolution proofs from closed tableaux for propositional schemata. The first one handles the most efficient version of the tableau calculus but generates very complex derivations (denoted by rather elaborate rewrite systems). The second one has the advantage that much simpler systems can be obtained, however the considered proof procedure is less efficient.
Power Management during Scan Based Sequential Circuit Testing
Venue: arXiv cs.CE 2011
Year: 2011

This paper shows that not every scan cell contributes equally to the power consumption during scan based test. The transitions at some scan cells cause more toggles at the internal signal lines of a circuit than the transitions at other scan cells. Hence the transitions at these scan cells have a larger impact on the power consumption during test application. These scan cells are called power sensitive scan cells.A verilog based approach is proposed to identify a set of power sensitive scan cells. Additional hardware is added to freeze the outputs of power sensitive scan cells during scan shifting in order to reduce the shift power consumption.when multiple scan chain is incorporated along with freezing the power sensitive scan cell,over all power during testing can be reduced to a larger extend.
Testing List H-Homomorphisms
Venue: arXiv cs.DS 2011
Year: 2011

Let $H$ be an undirected graph. In the List $H$-Homomorphism Problem, given an undirected graph $G$ with a list constraint $L(v) \subseteq V(H)$ for each variable $v \in V(G)$, the objective is to find a list $H$-homomorphism $f:V(G) \to V(H)$, that is, $f(v) \in L(v)$ for every $v \in V(G)$ and $(f(u),f(v)) \in E(H)$ whenever $(u,v) \in E(G)$. We consider the following problem: given a map $f:V(G) \to V(H)$ as an oracle access, the objective is to decide with high probability whether $f$ is a list $H$-homomorphism or \textit{far} from any list $H$-homomorphisms. The efficiency of an algorithm is measured by the number of accesses to $f$. In this paper, we classify graphs $H$ with respect to the query complexity for testing list $H$-homomorphisms and show the following trichotomy holds: (i) List $H$-homomorphisms are testable with a constant number of queries if and only if $H$ is a reflexive complete graph or an irreflexive complete bipartite graph. (ii) List $H$-homomorphisms are testable with a sublinear number of queries if and only if $H$ is a bi-arc graph. (iii) Testing list $H$-homomorphisms requires a linear number of queries if $H$ is not a bi-arc graph.
Confronting Intractability via Parameters
Venue: arXiv cs.CC 2011
Year: 2011

One approach to confronting computational hardness is to try to understand the contribution of various parameters to the running time of algorithms and the complexity of computational tasks. Almost no computational tasks in real life are specified by their size alone. It is not hard to imagine that some parameters contribute more intractability than others and it seems reasonable to develop a theory of computational complexity which seeks to exploit this fact. Such a theory should be able to address the needs of practicioners in algorithmics. The last twenty years have seen the development of such a theory. This theory has a large number of successes in terms of a rich collection of algorithmic techniques both practical and theoretical, and a fine-grained intractability theory. Whilst the theory has been widely used in a number of areas of applications including computational biology, linguistics, VLSI design, learning theory and many others, knowledge of the area is highly varied. We hope that this article will show both the basic theory and point at the wide array of techniques available. Naturally the treatment is condensed, and the reader who wants more should go to the texts, Downey and Fellows, Flum and Grohe, Niedermeier, and the upcoming undergraduate text Downey and Fellows.
The restricted isometry property for time-frequency structured random matrices
Venue: arXiv cs.IT 2011
Year: 2011

We establish the restricted isometry property for finite dimensional Gabor systems, that is, for families of time--frequency shifts of a randomly chosen window function. We show that the $s$-th order restricted isometry constant of the associated $n \times n^2$ Gabor synthesis matrix is small provided $s \leq c \, n^{2/3} / \log^2 n$. This improves on previous estimates that exhibit quadratic scaling of $n$ in $s$. Our proof develops bounds for a corresponding chaos process.
ReProCS: A Missing Link between Recursive Robust PCA and Recursive Sparse Recovery in Large but Correlated Noise
Venue: arXiv cs.IT 2011
Year: 2011

This work studies the recursive robust principal components' analysis (PCA) problem. Here, "robust" refers to robustness to both independent and correlated sparse outliers, although we focus on the latter. A key application where this problem occurs is in video surveillance where the goal is to separate a slowly changing background from moving foreground objects on-the-fly. The background sequence is well modeled as lying in a low dimensional subspace, that can gradually change over time, while the moving foreground objects constitute the correlated sparse outliers. In this and many other applications, the foreground is an outlier for PCA but is actually the "signal of interest" for the application; where as the background is the corruption or noise. Thus our problem can also be interpreted as one of recursively recovering a time sequence of sparse signals in the presence of large but spatially correlated noise. This work has two key contributions. First, we provide a new way of looking at this problem and show how a key part of our solution strategy involves solving a noisy compressive sensing (CS) problem. Second, we show how we can utilize the correlation of the outliers to our advantage in order to even deal with very large support sized outliers. The main idea is as follows. The correlation model applied to the previous support estimate helps predict the current support. This prediction serves as "partial support knowledge" for solving the modified-CS problem instead of CS. The support estimate of the modified-CS reconstruction is, in turn, used to update the correlation model parameters using a Kalman filter (or any adaptive filter). We call the resulting approach "support-predicted modified-CS".
Evaluation of Fiji National University Campus Information Systems
Venue: arXiv cs.HC 2011
Year: 2011

Fiji National University (FNU) has been encountering many difficulties with its current campus administrative systems. These difficulties include accessibility, scalability, performance, flexibility and integration. In order to address these difficulties, we developed a thin client web based campus information system. The newly designed system allows the students, academic and administration staff of the university to handle their day to day affairs with the university online. In this paper we describe three types of evaluation carried out to determine the suitability of newly developed system for FNU environment. User interface evaluation was carried out to assess user interface on a set of usability principles, usability evaluation to see the ease at which users can use the system and finally performance evaluation to verify and validate user response time required to complete various tasks. The result of each of these evaluations were analysed and the system was rectified as part of iterative design process.
Decoding finger movements from ECoG signals using switching linear models
Venue: arXiv cs.LG 2011
Year: 2011

One of the major challenges of ECoG-based Brain-Machine Interfaces is the movement prediction of a human subject. Several methods exist to predict an arm 2-D trajectory. The fourth BCI Competition gives a dataset in which the aim is to predict individual finger movements (5-D trajectory). The difficulty lies in the fact that there is no simple relation between ECoG signals and finger movement. We propose in this paper to decode finger flexions using switching models. This method permits to simplify the system as it is now described as an ensemble of linear models depending on an internal state. We show that an interesting accuracy prediction can be obtained by such a model.
High Performance Human Face Recognition using Independent High Intensity Gabor Wavelet Responses: A Statistical Approach
Venue: arXiv cs.CV 2011
Year: 2011

In this paper, we present a technique by which high-intensity feature vectors extracted from the Gabor wavelet transformation of frontal face images, is combined together with Independent Component Analysis (ICA) for enhanced face recognition. Firstly, the high-intensity feature vectors are automatically extracted using the local characteristics of each individual face from the Gabor transformed images. Then ICA is applied on these locally extracted high-intensity feature vectors of the facial images to obtain the independent high intensity feature (IHIF) vectors. These IHIF forms the basis of the work. Finally, the image classification is done using these IHIF vectors, which are considered as representatives of the images. The importance behind implementing ICA along with the high-intensity features of Gabor wavelet transformation is twofold. On the one hand, selecting peaks of the Gabor transformed face images exhibit strong characteristics of spatial locality, scale, and orientation selectivity. Thus these images produce salient local features that are most suitable for face recognition. On the other hand, as the ICA employs locally salient features from the high informative facial parts, it reduces redundancy and represents independent features explicitly. These independent features are most useful for subsequent facial discrimination and associative recall. The efficiency of IHIF method is demonstrated by the experiment on frontal facial images dataset, selected from the FERET, FRAV2D, and the ORL database.
On the expressive power of unit resolution
Venue: arXiv cs.AI 2011
Year: 2011

This preliminary report addresses the expressive power of unit resolution regarding input data encoded with partial truth assignments of propositional variables. A characterization of the functions that are computable in this way, which we propose to call propagatable functions, is given. By establishing that propagatable functions can also be computed using monotone circuits, we show that there exist polynomial time complexity propagable functions requiring an exponential amount of clauses to be computed using unit resolution. These results shed new light on studying CNF encodings of NP-complete problems in order to solve them using propositional satisfiability algorithms.
DWT Based Fingerprint Recognition using Non Minutiae Features
Venue: arXiv cs.CV 2011
Year: 2011

Forensic applications like criminal investigations, terrorist identification and National security issues require a strong fingerprint data base and efficient identification system. In this paper we propose DWT based Fingerprint Recognition using Non Minutiae (DWTFR) algorithm. Fingerprint image is decomposed into multi resolution sub bands of LL, LH, HL and HH by applying 3 level DWT. The Dominant local orientation angle θ and Coherence are computed on LL band only. The Centre Area Features and Edge Parameters are determined on each DWT level by considering all four sub bands. The comparison of test fingerprint with database fingerprint is decided based on the Euclidean Distance of all the features. It is observed that the values of FAR, FRR and TSR are improved compared to the existing algorithm.
Cryptographic Hardening of d-Sequences
Venue: arXiv cs.CR 2011
Year: 2011

This paper shows how a one-way mapping using majority information on adjacent bits will improve the randomness of d-sequences. Supporting experimental results are presented. It is shown that the behavior of d-sequences is different from that of other RNG sequences.
A time-parallel algorithm for almost integrable Hamiltonian systems
Venue: arXiv cs.NA 2011
Year: 2011

We introduce a time-parallel algorithm for solving numerically almost integrable Hamiltonian systems in action-angle coordinates. This algorithm is a refinement of that introduced by Saha, Stadel and Tremaine in 1997 (SST97) for the same type of problems. Our refined algorithm has a better convergence obtained from the use of derivatives of the perturbing term not considered in the original SST97 algorithm. An advantage of this algorithm is its independence of the step-size for the parallelized procedures which can be consider as a particular case of the parareal scheme.
Attack Interference in Non-Collaborative Scenarios for Security Protocol Analysis [Extended Version]
Venue: arXiv cs.CR 2011
Year: 2011

In security protocol analysis, the traditional choice to consider a single Dolev-Yao attacker is supported by the fact that models with multiple collaborating Dolev-Yao attackers have been shown to be reducible to models with one Dolev-Yao attacker. In this paper, we take a fundamentally different approach and investigate the case of multiple non-collaborating attackers. After formalizing the framework for multi-attacker scenarios, we show with a case study that concurrent competitive attacks can interfere with each other. We then present a new strategy to defend security protocols, based on active exploitation of attack interference. The paper can be seen as providing two proof-of-concept results: (i) it is possible to exploit interference to mitigate protocol vulnerabilities, thus providing a form of protection to protocols; (ii) the search for defense strategies requires scenarios with at least two attackers.
Intelligent Self-Repairable Web Wrappers
Venue: arXiv cs.AI 2011
Year: 2011

The amount of information available on the Web grows at an incredible high rate. Systems and procedures devised to extract these data from Web sources already exist, and different approaches and techniques have been investigated during the last years. On the one hand, reliable solutions should provide robust algorithms of Web data mining which could automatically face possible malfunctioning or failures. On the other, in literature there is a lack of solutions about the maintenance of these systems. Procedures that extract Web data may be strictly interconnected with the structure of the data source itself; thus, malfunctioning or acquisition of corrupted data could be caused, for example, by structural modifications of data sources brought by their owners. Nowadays, verification of data integrity and maintenance are mostly manually managed, in order to ensure that these systems work correctly and reliably. In this paper we propose a novel approach to create procedures able to extract data from Web sources -- the so called Web wrappers -- which can face possible malfunctioning caused by modifications of the structure of the data source, and can automatically repair themselves.
Models, Calculation and Optimization of Gas Networks, Equipment and Contracts for Design, Operation, Booking and Accounting
Venue: arXiv cs.CE 2011
Year: 2011

There are proposed models of contracts, technological equipment and gas networks and methods of their optimization. The flow in network undergoes restrictions of contracts and equipment to be operated. The values of sources and sinks are provided by contracts. The contract models represent (sub-) networks. The simplest contracts represent either nodes or edges. Equipment is modeled by edges. More sophisticated equipment is represented by sub-networks. Examples of such equipment are multi-poles and compressor stations with many entries and exits. The edges can be of different types corresponding to equipment and contracts. On such edges, there are given systems of equation and inequalities simulating the contracts and equipment. On this base, the methods proposed that allow: calculation and control of contract values for booking on future days and for accounting of sales and purchases; simulation and optimization of design and of operation of gas networks. These models and methods are implemented in software systems ACCORD and Graphicord as well as in the distributed control system used by Wingas, Germany. As numerical example, the industrial computations are presented.
Algorithmic Programming Language Identification
Venue: arXiv cs.LG 2011
Year: 2011

Motivated by the amount of code that goes unidentified on the web, we introduce a practical method for algorithmically identifying the programming language of source code. Our work is based on supervised learning and intelligent statistical features. We also explored, but abandoned, a grammatical approach. In testing, our implementation greatly outperforms that of an existing tool that relies on a Bayesian classifier. Code is written in Python and available under an MIT license.
Kernel Bounds for Path and Cycle Problems
Venue: arXiv cs.DS 2011
Year: 2011

Connectivity problems like k-Path and k-Disjoint Paths relate to many important milestones in parameterized complexity, namely the Graph Minors Project, color coding, and the recent development of techniques for obtaining kernelization lower bounds. This work explores the existence of polynomial kernels for various path and cycle problems, by considering nonstandard parameterizations. We show polynomial kernels when the parameters are a given vertex cover, a modulator to a cluster graph, or a (promised) max leaf number. We obtain lower bounds via cross-composition, e.g., for Hamiltonian Cycle and related problems when parameterized by a modulator to an outerplanar graph.
Faire levier sur les architectures logicielles pour guider et vérifier le développement d'applications SCC
Venue: arXiv cs.PL 2011
Year: 2011

A software architecture describes the structure of a computing system by specifying software components and their interactions. Mapping a software architecture to an implementation is a well known challenge. A key element of this mapping is the architecture's description of the data and control-flow interactions between components. The characterization of these interactions can be rather abstract or very concrete, providing more or less implementation guidance, programming support, and static verification. In this paper, we explore one point in the design space between abstract and concrete component interaction specifications. We introduce a notion of interaction contract that expresses allowed interactions between components, describing both data and control-flow constraints. This declaration is part of the architecture description, allows generation of extensive programming support, and enables various verifications. We instantiate our approach in an architecture description language for Sense/Compute/Control applications, and describe associated compilation and verification strategies.
On the gap between ess(f) and cnf_size(f)
Venue: arXiv cs.DM 2011
Year: 2011

Given a Boolean function f, the quantity ess(f) denotes the largest set of assignments that falsify f, no two of which falsify a common implicate of f. Although ess(f)$ is clearly a lower bound on cnf_size(f) (the minimum number of clauses in a CNF formula for f), Cepek et al. showed that it is not, in general, a tight lower bound. They gave examples of functions f for which there is a small gap between ess(f) and cnf_size(f). We demonstrate significantly larger gaps. We show that the gap can be exponential in n for arbitrary Boolean functions, and Theta(sqrt{n}) for Horn functions, where n is the number of variables of f. We also introduce a natural extension of the quantity ess(f), which we call ess_k(f), which is the largest set of assignments, no k of which falsify a common implicate of f.