For stroke-order free online multi-stroke charac- ter recognition, stroke-to-stroke correspondence search be- tween an input pattern and a reference pattern plays an im- portant role to deal with the stroke-order vari...For stroke-order free online multi-stroke charac- ter recognition, stroke-to-stroke correspondence search be- tween an input pattern and a reference pattern plays an im- portant role to deal with the stroke-order variation. Although various methods of stroke correspondence have been pro- posed, no comparative study for clarifying the relative su- periority of those methods has been done before. In this pa- per, we firstly review the approaches for solving the stroke- order variation problem. Then, five representative methods of stroke correspondence proposed by different groups, includ- ing cube search （CS）, bipartite weighted matching （BWM）, individual correspondence decision （ICD）, stable marriage （SM）, and deviation-expansion model （DE）, are experimen- tally compared, mainly in regard of recognition accuracy and efficiency. The experimental results on an online Kanji char- acter dataset, showed that 99.17%, 99.17%, 96.37%, 98.54%, and 96.59% were attained by CS, BWM, ICD, SM, and DE, respectively as their recognition rates. Extensive discussions are made on their relative superiorities and practicalities.展开更多
Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, mode...Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related liter- atures published at reputed conferences, symposiums, workshops, and journals, and took a survey of （1） various model checking techniques that can be adapted to software development and their implementations, and （2） the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for soft- ware debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique（s） and/or tool（s） are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.展开更多
Multi-view dynamic three-dimensional reconstruction has typically required the use of custom shutter-synchronized camera rigs in order to capture scenes containing rapid movements or complex topology changes. In this ...Multi-view dynamic three-dimensional reconstruction has typically required the use of custom shutter-synchronized camera rigs in order to capture scenes containing rapid movements or complex topology changes. In this paper, we demonstrate that multiple unsynchronized low-cost RGB-D cameras can be used for the same purpose. To alleviate issues caused by unsynchronized shutters, we propose a novel depth frame interpolation technique that allows synchronized data capture from highly dynamic 3 D scenes. To manage the resulting huge number of input depth images, we also introduce an efficient moving least squares-based volumetric reconstruction method that generates triangle meshes of the scene. Our approach does not store the reconstruction volume in memory,making it memory-efficient and scalable to large scenes.Our implementation is completely GPU based and works in real time. The results shown herein, obtained with real data, demonstrate the effectiveness of our proposed method and its advantages compared to stateof-the-art approaches.展开更多
Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execu- tion exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researcher...Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execu- tion exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have par- alleled existing symbolic execution tools （e.g., KLEE）. In particular, Cloud9 is a widely used paralleled symbolic exe- cution tool, and researchers have used the tool to analyze real code. However, researchers criticize that tools such as Cloud9 still cannot analyze large scale code. In this paper, we con- duct a field study on Cloud9, in which we use KLEE and Cloud9 to analyze benchmarks in C. Our results confirm the criticism. Based on the results, we identify three bottlenecks that hinder the performance of Cloud9： the communication time gap, the job transfer policy, and the cache management of the solved constraints. To handle these problems, we tune the communication time gap with better parameters, modify the job transfer policy, and implement an approach for cache management of solved constraints. We conduct two evalua- tions on our benchmarks and a real application to understand our improvements. Our results show that our tuned Cloud9 reduces the execution time significantly, both on our bench- marks and the real application. Furthermore, our evaluation results show that our tuning techniques improve the effective- ness on all the devices, and the improvement can be achievedupto five times, depending upon a tuning value of our ap- proach and the behaviour of program under test.展开更多
文摘For stroke-order free online multi-stroke charac- ter recognition, stroke-to-stroke correspondence search be- tween an input pattern and a reference pattern plays an im- portant role to deal with the stroke-order variation. Although various methods of stroke correspondence have been pro- posed, no comparative study for clarifying the relative su- periority of those methods has been done before. In this pa- per, we firstly review the approaches for solving the stroke- order variation problem. Then, five representative methods of stroke correspondence proposed by different groups, includ- ing cube search （CS）, bipartite weighted matching （BWM）, individual correspondence decision （ICD）, stable marriage （SM）, and deviation-expansion model （DE）, are experimen- tally compared, mainly in regard of recognition accuracy and efficiency. The experimental results on an online Kanji char- acter dataset, showed that 99.17%, 99.17%, 96.37%, 98.54%, and 96.59% were attained by CS, BWM, ICD, SM, and DE, respectively as their recognition rates. Extensive discussions are made on their relative superiorities and practicalities.
文摘Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related liter- atures published at reputed conferences, symposiums, workshops, and journals, and took a survey of （1） various model checking techniques that can be adapted to software development and their implementations, and （2） the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for soft- ware debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique（s） and/or tool（s） are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.
文摘Multi-view dynamic three-dimensional reconstruction has typically required the use of custom shutter-synchronized camera rigs in order to capture scenes containing rapid movements or complex topology changes. In this paper, we demonstrate that multiple unsynchronized low-cost RGB-D cameras can be used for the same purpose. To alleviate issues caused by unsynchronized shutters, we propose a novel depth frame interpolation technique that allows synchronized data capture from highly dynamic 3 D scenes. To manage the resulting huge number of input depth images, we also introduce an efficient moving least squares-based volumetric reconstruction method that generates triangle meshes of the scene. Our approach does not store the reconstruction volume in memory,making it memory-efficient and scalable to large scenes.Our implementation is completely GPU based and works in real time. The results shown herein, obtained with real data, demonstrate the effectiveness of our proposed method and its advantages compared to stateof-the-art approaches.
文摘Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execu- tion exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have par- alleled existing symbolic execution tools （e.g., KLEE）. In particular, Cloud9 is a widely used paralleled symbolic exe- cution tool, and researchers have used the tool to analyze real code. However, researchers criticize that tools such as Cloud9 still cannot analyze large scale code. In this paper, we con- duct a field study on Cloud9, in which we use KLEE and Cloud9 to analyze benchmarks in C. Our results confirm the criticism. Based on the results, we identify three bottlenecks that hinder the performance of Cloud9： the communication time gap, the job transfer policy, and the cache management of the solved constraints. To handle these problems, we tune the communication time gap with better parameters, modify the job transfer policy, and implement an approach for cache management of solved constraints. We conduct two evalua- tions on our benchmarks and a real application to understand our improvements. Our results show that our tuned Cloud9 reduces the execution time significantly, both on our bench- marks and the real application. Furthermore, our evaluation results show that our tuning techniques improve the effective- ness on all the devices, and the improvement can be achievedupto five times, depending upon a tuning value of our ap- proach and the behaviour of program under test.
