In recent years we have witnessed a large interest in surface deformation techniques. This has been a reaction that can be attributed to the ability to develop techniques which are detail-preserving. Space deformation techniques, on the other hand, received less attention, but nevertheless they have many advantages over surface-based techniques. This paper explores the potential of these two approaches to deformation and discusses the opportunities that the fusion of the two may lead to.

This survey reviews the recent development of gradient domain mesh deformation method. Different to other deformation methods, the gradient domain deformation method is a surface-based, variational optimization method. It directly encodes the geometric details in differential coordinates, which are also called Laplacian coordinates in literature. By preserving the Laplacian coordinates, the mesh details can be well preserved during deformation. Due to the locality of the Laplacian coordinates, the variational optimization problem can be casted into a sparse linear system. Fast sparse linear solver can be adopted to generate deformation result interactively, or even in real-time. The nonlinear nature of gradient domain mesh deformation leads to the development of two categories of deformation methods: linearization methods and nonlinear optimization methods. Basically, the linearization methods only need to solve the linear least-squares system once. They are fast, easy to understand and control, while the deformation result might be suboptimal. Nonlinear optimization methods can reach optimal solution of deformation energy function by iterative updating. Since the computation of nonlinear methods is expensive, reduced deformable models should be adopted to achieve interactive performance. The nonlinear optimization methods avoid the user burden to input transformation at deformation handles, and they can be extended to incorporate various nonlinear constraints, like volume constraint, skeleton constraint, and so on. We review representative methods and related approaches of each category comparatively and hope to help the user understand the motivation behind the algorithms. Finally, we discuss the relation between physical simulation and gradient domain mesh deformation to reveal why it can achieve physically plausible deformation result.

Polygonal models are popular representations of 3D objects. The use of polygonal models in computational applications often requires a model to properly bound a 3D solid. That is, the polygonal model needs to be closed, manifold, and free of self-intersections. This paper surveys a sizeable literature for repairing models that do not satisfy this criteria, focusing on categorizing them by their methodology and capability. We hope to offer pointers to further readings for researchers and practitioners, and suggestions of promising directions for future research endeavors.

We present some new methods for parameterizing the triangle mesh surface (TMS) which result from the Marching Cubes (MC) algorithm. The methods apply to surfaces of genus zero and the parameter domain is a unit sphere. We take advantage of some special properties of the TMS resulting from the MC algorithm to obtain simple, computational efficient representations of the nearest neighbor coordinates and utilize these coordinates in the characterization of the parameterization by means of systems of equations which are solved iteratively. Examples and comparisons are presented.

A new method for constructing interpolating Loop subdivision surfaces is presented. The new method is an extension of the progressive interpolation technique for B-splines. Given a triangular mesh $M$, the idea is to iteratively upgrade the vertices of $M$ to generate a new control mesh $\ov{M}$ such that limit surface of $\ov{M}$ would interpolate $M$. It can be shown that the iterative process is convergent for Loop subdivision surfaces. Hence, the method is well-defined. The new method has the advantages of both a local method and a global method, i.e., it can handle meshes of any size and any topology while generating smooth interpolating subdivision surfaces that faithfully resemble the shape of the given meshes. The meshes considered here can be open or closed.

It is a challenging problem of surface-based deformation to avoid apparent volumetric distortions around largely deformed areas. In this paper, we propose a new rigidity constraint for gradient domain mesh deformation to address this problem. Intuitively the proposed constraint can be regarded as several small cubes defined by the mesh vertices through mean value coordinates. The user interactively specifies the cubes in the regions which are prone to volumetric distortions, and the rigidity constraints could make the mesh behave like a solid object during deformation. The experimental results demonstrate that our constraint is intuitive, easy to use and very effective.

A simple robust "strut algorithm" is presented which, when given a graph embedded in 3D space, thickens its edges into solid struts. Various applications, crystallographic and sculptural, are shown in which smooth high-genus forms are the output. A toolbox of algorithmic techniques allow for a variety of novel, visually engaging forms that express a mathematical aesthetic. In sculptural examples, hyperbolic tessellations in the Poincar\'e plane are transformed in several ways to three-dimensional networks of edges embodied within a plausibly organic organization. By the use of different transformations and adjustable parameters in the algorithms, a variety of attractive forms result. The techniques produce watertight boundary representations that can be built with solid freeform fabrication equipment. The final physical output satisfies the "coolness criterion," that passers by will pick them up and say "Wow, that's cool!"

This paper gives a method of quantifying small visual differences between 3D mesh models with conforming topology, based on the theory of strain fields. Strain field is a geometric quantity in elasticity which is used to describe the deformation of elastomer. In this paper we consider the 3D models as objects with elasticity. The further demonstrations are provided: the first is intended to give the reader a visual impression of how our measure works in practice; and the second is to give readers a visual impression of how our measure works in evaluating filter algorithms. Our experiments show that our difference estimates are well correlated with human perception of differences. This work has applications in the evaluation of 3D mesh watermarking, 3D mesh compression reconstruction, and 3D mesh filtering.

In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG reachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.

SAT-based bounded model checking (BMC) has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere {\it et al.} in checking linear temporal logic (LTL) formulae and then also adapted to check formulae of the universal fragment of computation tree logic (ACTL) by W. Penczek {\it et al}. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek's method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the $k$-model by distinguishing the temporal operator {\it EX} from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the $k$-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shows the advantages of the improved approach with respect to the efficiency of model checking.

Transactional memory (TM) is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code (PCC) system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness.

In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi (higher-order Calculus of Communicating Systems (CCS) and higher-order $\pi$-calculus, respectively) and the encoding from and to first-order $\pi$-calculus. However a fully abstract encoding of first-order $\pi$-calculus with higher-order CCS is not available up-today. This is what we intend to settle in this paper. We follow the encoding strategy, first proposed by Thomsen, of translating first-order $\pi$-calculus into Plain CHOCS. We show that the encoding strategy is fully abstract with respect to early bisimilarity (first-order $\pi$-calculus) and wired bisimilarity (Plain CHOCS) (which is a bisimulation defined on wired processes only sending and receiving wires), that is the core of the encoding strategy. Moreover from the fact that the wired bisimilarity is contained by the well-established context bisimilarity, we secure the soundness of the encoding, with respect to early bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results of this paper. Finally, we make some discussion on our work and suggest some future work.

Although two-party password-authenticated key exchange (PAKE) protocols have been intensively studied in recent years, group PAKE protocols have received little attention. In this paper, we propose a tree-based group PAKE protocol --- $n$PAKE$^+$ protocol under the setting where each party shares an {\em independent} password with a trusted server. The $n$PAKE$^+$ protocol is a novel combination of the hierarchical key tree structure and the password-based Diffie-Hellman exchange, and hence it achieves substantial gain in computation efficiency. In particular, the computation cost for each client in our protocol is only $O(\log n)$. Additionally, the hierarchical feature of $n$PAKE$^+$ enables every subgroup to obtain its own subgroup key in the end. We also prove the security of our protocol under the random oracle model and the ideal cipher model.

Stream Register File (SRF) is a large on-chip memory of the stream processor and its efficient management is essential for good performance. Current stream programming languages expose the management of SRF to the programmer, incurring heavy burden on the programmer and bringing difficulties to inheriting the legacy codes. SF95 is the language developed for FT64 which is the first 64-bit stream processor designed for scientific applications. SF95 conceals SRF from the programmer and leaves the management of SRF to its compiler. In this paper, we present a compiler approach named SRF Coloring to manage SRF automatically. The novelties of this paper are: first, it is the first time to use the graph coloring-based algorithm for the SRF management; second, an algorithm framework for SRF Coloring that is well suited to the FT64 architecture is proposed --- this framework is based on a well-understood graph coloring algorithm for register allocation, together with some modifications to deal with the unusual aspects of SRF problem; third, the SRF Coloring algorithm is implemented in SF95Compiler, a compiler designed for FT64 and SF95. The experimental results show that our approach represents a practical and promising solution to SRF allocation.

In the Semantic Web, vocabularies are defined and shared among knowledge workers to describe linked data for scientific, industrial or daily life usage. With the rapid growth of online vocabularies, there is an emergent need for approaches helping users understand vocabularies quickly. In this paper, we study the summarization of vocabularies to help users understand vocabularies. Vocabulary summarization is based on the structural analysis and pragmatics statistics in the global Semantic Web. Local Bipartite Model and Expanded Bipartite Model of a vocabulary are proposed to characterize the structure in a vocabulary and links between vocabularies. A structural importance for each RDF sentence in the vocabulary is assessed using link analysis. Meanwhile, pragmatics importance of each RDF sentence is assessed using the statistics of instantiation of its terms in the Semantic Web. Summaries are produced by extracting important RDF sentences in vocabularies under a re-ranking strategy. Preliminary experiments show that it is feasible to help users understand a vocabulary through its summary.

Various methods have been proposed for off-line permutation packet routing on a mesh. One of the methods is known as multistage routing, in which the first stage is crucial. For the first stage of routing, the previous study normally converts it to a problem of graph theory and proves the existence of solutions. However, there is a lack of simple algorithms to the first stage of routing. This article presents an explicit and simple approach for the first stage of routing based on elementary mathematics.