OpenRaiser/Intern-Atlas huggingface dataset:
Toward the Verification of a Simple Hypervisor
Venue: arXiv cs.LO 2011
Year: 2011

Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying virtual machine monitors (hypervisors). This paper describes an ongoing project to develop and verify MinVisor, a simple but functional Type-I x86 hypervisor, proving protection properties at the assembly level using ACL2. Originally based on an existing research hypervisor, MinVisor provides protection of its own memory from a malicious guest. Our long-term goal is to fully verify MinVisor, providing a vehicle to investigate the modeling and verification of hypervisors at the implementation level, and also a basis for further systems research. Functional segments of the MinVisor C code base are translated into Y86 assembly, and verified with respect to the Y86 model. The inductive assertions (also known as "compositional cutpoints") methodology is used to prove the correctness of the code. The proof of the code that sets up the nested page tables is described. We compare this project to related efforts in systems code verification and outline some useful steps forward.
How Can I Do That with ACL2? Recent Enhancements to ACL2
Venue: arXiv cs.MS 2011
Year: 2011

The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancements introduced after the release of Version 3.5 (in May, 2009, at about the time of the 2009 ACL2 workshop) up through the release of Version 4.3 in July, 2011, roughly a couple of years later. Many of these features are not particularly well known yet, but most ACL2 users could take advantage of at least some of them. Some of the changes could affect existing proof efforts, such as a change that treats pairs of functions such as 'member' and 'member-equal' as the same function.
A Generalized Arc-Consistency Algorithm for a Class of Counting Constraints: Revised Edition that Incorporates One Correction
Venue: arXiv cs.AI 2011
Year: 2011

This paper introduces the SEQ BIN meta-constraint with a polytime algorithm achieving general- ized arc-consistency according to some properties. SEQ BIN can be used for encoding counting con- straints such as CHANGE, SMOOTH or INCREAS- ING NVALUE. For some of these constraints and some of their variants GAC can be enforced with a time and space complexity linear in the sum of domain sizes, which improves or equals the best known results of the literature.
Improvement Of Barreto-Voloch Algorithm For Computing $r$th Roots Over Finite Fields
Venue: arXiv cs.SC 2011
Year: 2011

Root extraction is a classical problem in computers algebra. It plays an essential role in cryptosystems based on elliptic curves. In 2006, Barreto and Voloch proposed an algorithm to compute $r$th roots in ${F}_{q^m} $ for certain choices of $m$ and $q$. If $r\,||\,q-1$ and $ (m, r)=1, $ they proved that the complexity of their method is $\widetilde{\mathcal {O}}(r(\log m+\log\log q)m\log q) $. In this paper, we extend the Barreto-Voloch algorithm to the general case that $r\,||\,q^m-1$, without the restrictions $r\,||\,q-1$ and $(m, r)=1 $. We also specify the conditions that the Barreto-Voloch algorithm can be preferably applied.
Cameleon language Part 1: Processor
Venue: arXiv cs.PL 2011
Year: 2011

Emergence is the way complex systems arise out of a multiplicity of relatively simple interactions between primitives. Since programming problems become more and more complexes and transverses, our vision is that application development should be process at two scales: micro- and macro-programming where at the micro-level the paradigm is step-by-step and at macro-level the paradigm is emergence. For micro-programming, which focuses on how things happen, popular languages, Java, C++, Python, are imperative writing languages where the code is a sequence of sentences executed by the computer. For macro-programming, which focuses on how things connect, popular languages, labVIEW, Blender, Simulink, are graphical data flow languages such that the program is a composition of operators, a unit-process consuming input data and producing output data, and connectors, a data-flow between an output data and an input data of two operators. However, despite their fruitful applications, these macro-languages are not transversal since different data-structures of native data-structures cannot be integrated in their framework easily. Cameleon language is a graphical data flow language following a two-scale paradigm. It allows an easy up-scale that is the integration of any library writing in C++ in the data flow language. Cameleon language aims to democratize macro-programming by an intuitive interaction between the human and the computer where building an application based on a data-process and a GUI is a simple task to learn and to do. Cameleon language allows conditional execution and repetition to solve complex macro-problems. In this paper we introduce a new model based on the extension of the petri net model for the description of how the Cameleon language executes a composition.
Leveraging User Diversity to Harvest Knowledge on the Social Web
Venue: arXiv cs.IR 2011
Year: 2011

Social web users are a very diverse group with varying interests, levels of expertise, enthusiasm, and expressiveness. As a result, the quality of content and annotations they create to organize content is also highly variable. While several approaches have been proposed to mine social annotations, for example, to learn folksonomies that reflect how people relate narrower concepts to broader ones, these methods treat all users and the annotations they create uniformly. We propose a framework to automatically identify experts, i.e., knowledgeable users who create high quality annotations, and use their knowledge to guide folksonomy learning. We evaluate the approach on a large body of social annotations extracted from the photosharing site Flickr. We show that using expert knowledge leads to more detailed and accurate folksonomies. Moreover, we show that including annotations from non-expert, or novice, users leads to more comprehensive folksonomies than experts' knowledge alone.
Wikipedia Edit Number Prediction based on Temporal Dynamics Only
Venue: arXiv cs.LG 2011
Year: 2011

In this paper, we describe our approach to the Wikipedia Participation Challenge which aims to predict the number of edits a Wikipedia editor will make in the next 5 months. The best submission from our team, "zeditor", achieved 41.7% improvement over WMF's baseline predictive model and the final rank of 3rd place among 96 teams. An interesting characteristic of our approach is that only temporal dynamics features (i.e., how the number of edits changes in recent periods, etc.) are used in a self-supervised learning framework, which makes it easy to be generalised to other application domains.
Quels formalismes temporels pour représenter des connaissances extraites de textes de recettes de cuisine ?
Venue: arXiv cs.AI 2011
Year: 2011

The Taaable projet goal is to create a case-based reasoning system for retrieval and adaptation of cooking recipes. Within this framework, we are discussing the temporal aspects of recipes and the means of representing those in order to adapt their text.
Fluctuation-induced traffic congestion in heterogeneous networks
Venue: arXiv cs.NI 2011
Year: 2011

In studies of complex heterogeneous networks, particularly of the Internet, significant attention was paid to analyzing network failures caused by hardware faults or overload, where the network reaction was modeled as rerouting of traffic away from failed or congested elements. Here we model another type of the network reaction to congestion -- a sharp reduction of the input traffic rate through congested routes which occurs on much shorter time scales. We consider the onset of congestion in the Internet where local mismatch between demand and capacity results in traffic losses and show that it can be described as a phase transition characterized by strong non-Gaussian loss fluctuations at a mesoscopic time scale. The fluctuations, caused by noise in input traffic, are exacerbated by the heterogeneous nature of the network manifested in a scale-free load distribution. They result in the network strongly overreacting to the first signs of congestion by significantly reducing input traffic along the communication paths where congestion is utterly negligible.
Categorical interpretations of some key agreement protocols
Venue: arXiv cs.CR 2011
Year: 2011

We give interpretations of some known key agreement protocols in the framework of category theory and in this way we give a method of constructing of many new key agreement protocols.
Computing a Longest Common Palindromic Subsequence
Venue: arXiv cs.DS 2011
Year: 2011

The {\em longest common subsequence (LCS)} problem is a classic and well-studied problem in computer science. Palindrome is a word which reads the same forward as it does backward. The {\em longest common palindromic subsequence (LCPS)} problem is an interesting variant of the classic LCS problem which finds the longest common subsequence between two given strings such that the computed subsequence is also a palindrome. In this paper, we study the LCPS problem and give efficient algorithms to solve this problem. To the best of our knowledge, this is the first attempt to study and solve this interesting problem.
MyZone: A Next-Generation Online Social Network
Venue: arXiv cs.SI 2011
Year: 2011

This technical report considers the design of a social network that would address the shortcomings of the current ones, and identifies user privacy, security, and service availability as strong motivations that push the architecture of the proposed design to be distributed. We describe our design in detail and identify the property of resiliency as a key objective for the overall design philosophy. We define the system goals, threat model, and trust model as part of the system model, and discuss the challenges in adapting such distributed frameworks to become highly available and highly resilient in potentially hostile environments. We propose a distributed solution to address these challenges based on a trust-based friendship model for replicating user profiles and disseminating messages, and examine how this approach builds upon prior work in distributed Peer-to-Peer (P2P) networks.
Hand Tracking based on Hierarchical Clustering of Range Data
Venue: arXiv cs.CV 2011
Year: 2011

Fast and robust hand segmentation and tracking is an essential basis for gesture recognition and thus an important component for contact-less human-computer interaction (HCI). Hand gesture recognition based on 2D video data has been intensively investigated. However, in practical scenarios purely intensity based approaches suffer from uncontrollable environmental conditions like cluttered background colors. In this paper we present a real-time hand segmentation and tracking algorithm using Time-of-Flight (ToF) range cameras and intensity data. The intensity and range information is fused into one pixel value, representing its combined intensity-depth homogeneity. The scene is hierarchically clustered using a GPU based parallel merging algorithm, allowing a robust identification of both hands even for inhomogeneous backgrounds. After the detection, both hands are tracked on the CPU. Our tracking algorithm can cope with the situation that one hand is temporarily covered by the other hand.
Subspace Evasive Sets
Venue: arXiv cs.CC 2011
Year: 2011

In this work we describe an explicit, simple, construction of large subsets of F^n, where F is a finite field, that have small intersection with every k-dimensional affine subspace. Interest in the explicit construction of such sets, termed subspace-evasive sets, started in the work of Pudlak and Rodl (2004) who showed how such constructions over the binary field can be used to construct explicit Ramsey graphs. More recently, Guruswami (2011) showed that, over large finite fields (of size polynomial in n), subspace evasive sets can be used to obtain explicit list-decodable codes with optimal rate and constant list-size. In this work we construct subspace evasive sets over large fields and use them to reduce the list size of folded Reed-Solomon codes form poly(n) to a constant.
Universal and efficient compressed sensing by spread spectrum and application to realistic Fourier imaging techniques
Venue: arXiv cs.IT 2011
Year: 2011

We advocate a compressed sensing strategy that consists of multiplying the signal of interest by a wide bandwidth modulation before projection onto randomly selected vectors of an orthonormal basis. Firstly, in a digital setting with random modulation, considering a whole class of sensing bases including the Fourier basis, we prove that the technique is universal in the sense that the required number of measurements for accurate recovery is optimal and independent of the sparsity basis. This universality stems from a drastic decrease of coherence between the sparsity and the sensing bases, which for a Fourier sensing basis relates to a spread of the original signal spectrum by the modulation (hence the name "spread spectrum"). The approach is also efficient as sensing matrices with fast matrix multiplication algorithms can be used, in particular in the case of Fourier measurements. Secondly, these results are confirmed by a numerical analysis of the phase transition of the l1- minimization problem. Finally, we show that the spread spectrum technique remains effective in an analog setting with chirp modulation for application to realistic Fourier imaging. We illustrate these findings in the context of radio interferometry and magnetic resonance imaging.
User preference extraction using dynamic query sliders in conjunction with UPS-EMO algorithm
Venue: arXiv cs.NE 2011
Year: 2011

One drawback of evolutionary multiobjective optimization algorithms (EMOA) has traditionally been high computational cost to create an approximation of the Pareto front: number of required objective function evaluations usually grows high. On the other hand, for the decision maker (DM) it may be difficult to select one of the many produced solutions as the final one, especially in the case of more than two objectives. To overcome the above mentioned drawbacks number of EMOA's incorporating the decision makers preference information have been proposed. In this case, it is possible to save objective function evaluations by generating only the part of the front the DM is interested in, thus also narrowing down the pool of possible selections for the final solution. Unfortunately, most of the current EMO approaches utilizing preferences are not very intuitive to use, i.e. they may require tweaking of unintuitive parameters, and it is not always clear what kind of results one can get with given set of parameters. In this study we propose a new approach to visually inspect produced solutions, and to extract preference information from the DM to further guide the search. Our approach is based on intuitive use of dynamic query sliders, which serve as a means to extract preference information and are part of the graphical user interface implemented for the efficient UPS-EMO algorithm.
Generation of Test Vectors for Sequential Cell Verification
Venue: arXiv cs.OH 2011
Year: 2011

For Application Specific Integrated Circuits (ASIC) and System-on-Chip (SOC) designs, Cell - Based Design (CBD) is the most prevalent practice as it guarantees a shorter design cycle, minimizes errors and is easier to maintain. In modern ASIC design, standard cell methodology is practiced with sizable libraries of cells, each containing multiple implementations of the same logic functionality, in order to give the designer differing options based on area, speed or power consumption. For such library cells, thorough verification of functionality and timing is crucial for the overall success of the chip, as even a small error can prove fatal due to the repeated use of the cell in the design. Both formal and simulation based methods are being used in the industry for cell verification. We propose a method using the latter approach that generates an optimized set of test vectors for verification of sequential cells, which are guaranteed to give complete Single Input Change transition coverage with minimal redundancy. Knowledge of the cell functionality by means of the State Table is the only prerequisite of this procedure.
Enhancing Binary Images of Non-Binary LDPC Codes
Venue: arXiv cs.IT 2011
Year: 2011

We investigate the reasons behind the superior performance of belief propagation decoding of non-binary LDPC codes over their binary images when the transmission occurs over the binary erasure channel. We show that although decoding over the binary image has lower complexity, it has worse performance owing to its larger number of stopping sets relative to the original non-binary code. We propose a method to find redundant parity-checks of the binary image that eliminate these additional stopping sets, so that we achieve performance comparable to that of the original non-binary LDPC code with lower decoding complexity.
Parallel implematation of flow and matching algorithms
Venue: arXiv cs.DC 2011
Year: 2011

In our work we present two parallel algorithms and their lock-free implementations using a popular GPU environment Nvidia CUDA. The first algorithm is the push-relabel method for the flow problem in grid graphs. The second is the cost scaling algorithm for the assignment problem in complete bipartite graphs.
An empirical analysis of the relationship between web usage and academic performance in undergraduate students
Venue: arXiv cs.SI 2011
Year: 2011

The use of the internet, and in particular web browsing, offers many potential advantages for educational institutions as students have access to a wide range of information previously not available. However, there are potential negative effects due to factors such as time-wasting and asocial behaviour. In this study, we conducted an empirical investigation of the academic performance and the web-usage pattern of 2153 undergraduate students. Data from university proxy logs allows us to examine usage patterns and we compared this data to the students' academic performance. The results show that there is a small but significant (both statistically and educationally) association between heavier web browsing and poorer academic results (lower average mark, higher failure rates). In addition, among good students, the proportion of students who are relatively light users of the internet is significantly greater than would be expected by chance.
Implications for compressed sensing of a new sampling theorem on the sphere
Venue: arXiv cs.IT 2011
Year: 2011

A sampling theorem on the sphere has been developed recently, requiring half as many samples as alternative equiangular sampling theorems on the sphere. A reduction by a factor of two in the number of samples required to represent a band-limited signal on the sphere exactly has important implications for compressed sensing, both in terms of the dimensionality and sparsity of signals. We illustrate the impact of this property with an inpainting problem on the sphere, where we show the superior reconstruction performance when adopting the new sampling theorem compared to the alternative.
View Selection in Semantic Web Databases
Venue: arXiv cs.DB 2011
Year: 2011

We consider the setting of a Semantic Web database, containing both explicit data encoded in RDF triples, and implicit data, implied by the RDF semantics. Based on a query workload, we address the problem of selecting a set of views to be materialized in the database, minimizing a combination of query processing, view storage, and view maintenance costs. Starting from an existing relational view selection method, we devise new algorithms for recommending view sets, and show that they scale significantly beyond the existing relational ones when adapted to the RDF context. To account for implicit triples in query answers, we propose a novel RDF query reformulation algorithm and an innovative way of incorporating it into view selection in order to avoid a combinatorial explosion in the complexity of the selection process. The interest of our techniques is demonstrated through a set of experiments.
High-order finite volume schemes for layered atmospheric models
Venue: arXiv cs.NA 2011
Year: 2011

We present a numerical scheme for the solution of a class of atmospheric models where high horizontal resolution is required while a coarser vertical structure is allowed. The proposed scheme considers a layering procedure for the original set of equations, and the use of high-order ADER finite volume schemes for the solution of the system of balance laws arising from the dimensional reduction procedure. We present several types of layering based upon Galerkin discretizations of the vertical structure, and we study the effect of incrementing the order of horizontal approximation. Numerical experiments for the computational validation of the convergence of the scheme together with the study of physical phenomena are performed over 2D linear advective models, including a set of equations for an isothermal atmosphere.
Proof-irrelevant model of CC with predicative induction and judgmental equality
Venue: arXiv cs.LO 2011
Year: 2011

We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.
On Optimum Causal Cognitive Spectrum Reutilization Strategy
Venue: arXiv cs.IT 2011
Year: 2011

In this paper we study opportunistic transmission strategies for cognitive radios (CR) in which causal noisy observation from a primary user(s) (PU) state is available. PU is assumed to be operating in a slotted manner, according to a two-state Markov model. The objective is to maximize utilization ratio (UR), i.e., relative number of the PU-idle slots that are used by CR, subject to interference ratio (IR), i.e., relative number of the PU-active slots that are used by CR, below a certain level. We introduce an a-posteriori LLR-based cognitive transmission strategy and show that this strategy is optimum in the sense of maximizing UR given a certain maximum allowed IR. Two methods for calculating threshold for this strategy in practical situations are presented. One of them performs well in higher SNRs but might have too large IR at low SNRs and low PU activity levels, and the other is proven to never violate the allowed IR at the price of a reduced UR. In addition, an upper-bound for the UR of any CR strategy operating in the presence of Markovian PU is presented. Simulation results have shown a more than 116% improvement in UR at SNR of -3dB and IR level of 10% with PU state estimation. Thus, this opportunistic CR mechanism possesses a high potential in practical scenarios in which there exists no information about true states of PU.
Construction of an NP Problem with an Exponential Lower Bound
Venue: arXiv cs.CC 2011
Year: 2011

In this paper we present a Hashed-Path Traveling Salesperson Problem (HPTSP), a new type of problem which has the interesting property of having no polynomial time solutions. Next we show that HPTSP is in the class NP by demonstrating that local information about sub-routes is insufficient to compute the complete value of each route. As a consequence, via Ladner's theorem, we show that the class NPI is non-empty.