The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.

The notion of meta-variable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of meta-variables in textbooks, we propose two formal systems that have the notion of meta-variable.In both calculi, each variable is given a level (non-negative integer), which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a meta-level function operating on the metameta-level. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a meta-variable, free object-level variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as meta-level functions on object-level terms, hence uses capture-avoiding substitution.We show that both calculi enjoy a number of properties including Church-Rosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.

N?-labeled calculus is a generalization of N-labeled calculus so as to describe time-concerned recognition, knowledge, belief and decision of humans or computer programs together with related external physical or logical phenomena. N-labeled calculus is the smallest formal system applicable to verification and analysis of cooperative real-timing systems on natural number time introduced as an adaptation of tense arithmetic (TA). A merging problem of vehicles with misunderstanding or incorrect recognition is discussed as an example of cooperating systems controlling continuously changing objects including human factor. Euler’s approximation is introduced in order to represent the continuously changing objects. Through this example, relationship among artificial intelligence, external environment and human factors is investigated.

The aim of this paper is to extend the probabilistic choice in probabilistic programs to sub-probabilistic choice, i.e., of the form References | Related Articles | Metrics

We present a computing environment for origami on the web. The environment consists of the computational origami engine Eos for origami construction, visualization, and geometrical reasoning, WebEos for providing web interface to the functionalities of Eos, and web service system Scorum for symbolic computing web services. WebEos is developed using Web2.0 technologies, and provides a graphical interactive web interface for origami construction and proving. In Scorum, we are preparing web services for a wide range of symbolic computing systems, and are using these services in our origami environment. We explain the functionalities of this environment, and discuss its architectural and technological features.

We discuss the verification of mathematical software solving polynomial systems symbolically by way of triangular decomposition. Standard verification techniques are highly resource consuming and apply only to polynomial systems which are easy to solve. We exhibit a new approach which manipulates constructible sets represented by regular systems. We provide comparative benchmarks of different verification procedures applied to four solvers on a large set of well-known polynomial systems. Our experimental results illustrate the high efficiency of our new approach. In particular, we are able to verify triangular decompositions of polynomial systems which are not easy to solve.

Gaussian elimination and LU factoring have been greatly studied from the algorithmic point of view, but much less from the point view of the best output format. In this paper, we give new output formats for fraction free LU factoring and for QR factoring. The formats and the algorithms used to obtain them are valid for any matrix system in which the entries are taken from an integral domain, not just for integer matrix systems. After discussing the new output format of LU factoring, the complexity analysis for the fraction free algorithm and fraction free output is given. Our new output format contains smaller entries than previously suggested forms, and it avoids the gcd computations required by some other partially fraction free computations. As applications of our fraction free algorithm and format, we demonstrate how to construct a fraction free QR factorization and how to solve linear systems within a given domain.

Clustering high dimensional data has become a challenge in data mining due to the curse of dimensionality. To solve this problem, subspace clustering has been defined as an extension of traditional clustering that seeks to find clusters in subspaces spanned by different combinations of dimensions within a dataset. This paper presents a new subspace clustering algorithm that calculates the local feature weights automatically in an EM-based clustering process. In the algorithm, the features are locally weighted by using a new unsupervised weighting method, as a means to minimize a proposed clustering criterion that takes into account both the average intra-clusters compactness and the average inter-clusters separation for subspace clustering. For the purposes of capturing accurate subspace information, an additional outlier detection process is presented to identify the possible local outliers of subspace clusters, and is embedded between the E-step and M-step of the algorithm. The method has been evaluated in clustering real-world gene expression data and high dimensional artificial data with outliers, and the experimental results have shown its effectiveness.

The topic of super-resolution image reconstruction has recently received considerable attention among the research community. Super-resolution image reconstruction methods attempt to create a single high-resolution image from a number of low-resolution images (or a video sequence). The method of projections onto convex sets (POCS) for super-resolution image reconstruction attracts many researchers’ attention. In this paper, we propose an improvement to reduce the amount of Gibbs artifacts presenting on the edges of the high-resolution image reconstructed by the POCS method. The proposed method weights the blur PSF centered at an edge pixel with an exponential function, and consequently decreases the coefficients of the PSF in the direction orthogonal to the edge. Experiment results show that the modification reduces effectively the visibility of Gibbs artifacts on edges and improves obviously the quality of the reconstructed high-resolution image.

Expertise Oriented Search (EOS) aims at providing comprehensive expertise analysis on data from distributed sources. It is useful in many application domains, for example, finding experts on a given topic, detecting the confliction of interest between researchers, and assigning reviewers to proposals. In this paper, we present the design and implementation of our expertise oriented search system, Arnetminer (http://www.arnetminer.net). Arnetminer has gathered and integrated information about a half-million computer science researchers from the Web, including their profiles and publications. Moreover, Arnetminer constructs a social network among these researchers through their co-authorship, and utilizes this network information as well as the individual profiles to facilitate expertise oriented search tasks. In particular, the co-authorship information is used both in ranking the expertise of individual researchers for a given topic and in searching for associations between researchers. We have conducted initial experiments on Arnetminer. Our results demonstrate that the proposed relevancy propagation expert finding method outperforms the method that only uses person local information, and the proposed two-stage association search on a large-scale social network is order of magnitude faster than the baseline method.

Deniable ring authentication allows a member of an ad-hoc sunset of participants to authenticate a message without revealing which member has issued the signature, and the verifier cannot transfer the signature to any third party. It is an important cryptographic primitive for privacy and anonymous communication. Unfortunately, the size of the signature of the proposed deniable ring authentication is dependent on the size of the ring. It is inefficient especially when the size of the ring is large. In this paper, we propose an ID-based version of deniable ring authentication. We present a generic construction which uses dynamic accumulators to construct ID-based deniable ring authentication with constant-size signature. We also give an ID-based deniable ring authentication based on bilinear pairings, which is proved to be secure in the random oracle model.