检索结果-内蒙古大学图书馆

Slicing execution for model checking C programs

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING 2006年第5期16卷 747-768页

作者： Yi, Xiaodong Wang, Ji Yang, Xuejun Natl Lab Parallel & Distributed Proc Changsha Peoples R China

This paper presents a novel method, namely slicing execution, for model checking C programs with respect to temporal safety properties. The distinguished feature is that it shows a nice approach to the efficient reduction of state space by abstraction and symbolic representation. Slicing execution is founded on an over-approximated semantics of C programs by variable abstraction, and executes symbolically only the relevant statements under abstraction criteria to construct over-approximated finite models of programs, which may be model checked. The variable abstraction criterion begins with a proper initial set of program variables and may be iteratively refined according to spurious counterexamples generated during model checking. In general, the properties to be verified often involve only a few variables in practical programs. In these cases, significant state space reduction, as well as considerable improvement of the scalability, may be achieved. The presented method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c. The experiment results confirm that slicing execution is not only practical but also effective.

关键词： slicing execution variable abstraction paxtial strongest post-condition

来源：评论

学校读者我要写书评

暂无评论

Slicing Execution with Partial Weakest Precondition for Model Abstraction of C Programs

引用

COMPUTER JOURNAL 2010年第1期53卷 37-49页

作者： Yang, Xuejun Wang, Ji Yi, Xiaodong Natl Lab Parallel & Distributed Proc Changsha Hunan Peoples R China

Model abstraction plays an important role in model checking of source codes of programs. Slicing execution is a lightweight symbolic execution procedure to extract the models of C programs in an over-approximated way. In this paper, we present an approach to improving slicing execution with a novel concept called partial weakest precondition (PWP) to alleviate the space explosion problem. PWPs specify the corresponding weakest precondition conservatively by only considering part of program variables. We present how to integrate PWP with slicing execution, which leads to a compact model with much smaller state space compared with the one obtained by the original slicing execution. A new PWP implementation is also presented to avoid possible exponential PWP formula size and support pointers and aliases as well. The distinguished features of the implementation are that it does not need to translate the program to the passive form beforehand, and it supports loops very well. Comparing with slicing execution without PWP, the experimentation on SSL protocol based on the C source code openssl-0.9.6c shows that the state space may be reduced to only 1/10 after applying PWP.

关键词： partial weakest precondition model abstraction slicing execution

来源：评论

学校读者我要写书评

暂无评论

An Adversarial Feature Distillation Method for Audio Classification

引用

IEEE ACCESS 2019年 7卷 105319-105330页

作者： Gao, Liang Mi, Haibo Zhu, Boqing Feng, Dawei Li, Yicong Peng, Yuxing Natl Univ Def Technol Natl Key Lab Parallel & Distributed Proc Changsha 410073 Hunan Peoples R China

The audio classification task aims to discriminate between different audio signal types. In this task, deep neural networks have achieved better performance than the traditional shallow architecture-based machine-learning method. However, deep neural networks often require huge computational and storage requirements that hinder the deployment in embedded devices. In this paper, we proposed a distillation method which transfers knowledge from well-trained networks to a small network, and the method can compress model size while improving audio classification precision. The contributions of the proposed method are two folds: a multi-level feature distillation method was proposed and an adversarial learning strategy was employed to improve the knowledge transfer. The extensive experiments are conducted on three audio classification tasks, audio scene classification, general audio tagging, and speech command recognition. The experimental results demonstrate that: the small network can provide better performance while achieves the calculated amount of floating-point operations per second (FLOPS) compression ratio of 76:1 and parameters compression ratio of 3:1.

关键词： Convolutional neural networks audio tagging knowledge distillation model compression

来源：评论

学校读者我要写书评

暂无评论

FPGA implementation of an exact dot product and its application in variable-precision floating-point arithmetic

引用

JOURNAL OF SUPERCOMPUTING 2013年第2期64卷 580-605页

作者： Lei, Yuanwu Dou, Yong Dong, Yazhuo Zhou, Jie Xia, Fei NUDT Natl Lab Parallel & Distributed Proc Changsha Hunan Peoples R China

The current paper explores the capability and flexibility of field programmable gate-arrays (FPGAs) to implement variable-precision floating-point (VP) arithmetic. First, the VP exact dot product algorithm, which uses exact fixed-point operations to obtain an exact result, is presented. A VP multiplication and accumulation unit (VPMAC) on FPGA is then proposed. In the proposed design, the parallel multipliers generate the partial products of mantissa multiplication in parallel, which is the most time-consuming part in the VP multiplication and accumulation operation. This method fully utilizes DSP performance on FPGAs to enhance the performance of the VPMAC unit. Several other schemes, such as two-level RAM bank, carry-save accumulation, and partial summation, are used to achieve high frequency and pipeline throughput in the product accumulation stage. The typical algorithms in Basic Linear Algorithm Subprograms (i.e., vector dot product, general matrix vector product, and general matrix multiply product), LU decomposition, and Modified Gram-Schmidt QR decomposition, are used to evaluate the performance of the VPMAC unit. Two schemes, called the VPMAC coprocessor and matrix accelerator, are presented to implement these applications. Finally, prototypes of the VPMAC unit and the matrix accelerator based on the VPMAC unit are created on a Xilinx XC6VLX760 FPGA chip. Compared with a parallel software implementation based on OpenMP running on an Intel Xeon Quad-core E5620 CPU, the VPMAC coprocessor, equipped with one VPMAC unit, achieves a maximum acceleration factor of 18X. Moreover, the matrix accelerator, which mainly consists of a linear array of eight processing elements, achieves 12X-65X better performance.

关键词： Carry-save accumulation Exact dot produce FPGA MGS-QR decomposition LU decomposition Variable-precision floating-point (VP) arithmetic

来源：评论

学校读者我要写书评

暂无评论

Shape Analysis by Refining on Abstract Evaluation Path

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2008年第C期207卷 137-151页

作者： Ma, Xiaodong Wang, Ji Dong, Wei Natl Lab Parallel & Distributed Proc Beijing Peoples R China

This paper presents a novel method for shape analysis, which can deal with complex expressions in C language. It supports taking addresses of fields and stack variables. The concept of abstract evaluation path (AEP) is proposed, which is generated from the expression in the language. AEP is used to refine the abstract shape graph (ASG) to get a set of more precise ASGs, on which the semantics of the statement can be defined easily. The results can be used to determine "shape invariants" and detect memory leak conservatively. A prototype has been implemented and the results of the experiment are shown.

关键词： shape analysis memory leak AEP

来源：评论

学校读者我要写书评

暂无评论

Unsupervised Learning-Based Depth Estimation-Aided Visual SLAM Approach

引用

CIRCUITS SYSTEMS AND SIGNAL procESSING 2020年第2期39卷 543-570页

作者： Geng, Mingyang Shang, Suning Ding, Bo Wang, Huaimin Zhang, Pengfei Natl Univ Def Technol Coll Comp Natl Key Lab Parallel & Distributed Proc Changsha 410073 Peoples R China

Simultaneous localization and map construction (SLAM) tasks have been proven to benefit greatly from the depth information of the environment. In this paper, we first present an unsupervised end-to-end learning framework for the task of monocular depth and camera motion estimation from video sequences. The difference between our work and the existing unsupervised methods is that we not only use image reconstruction for supervising but also exploit the pose estimation method used in traditional SLAM approaches to enhance the supervised signal and add extra training constraints for the task of monocular depth and camera motion estimation. Furthermore, we successfully exploit our unsupervised learning framework to assist the traditional ORB-SLAM system when the initialization module of ORB-SLAM method could not match enough features. Qualitative and quantitative experiments have shown that our unsupervised learning framework performs the depth estimation task superior to the supervised methods and outperforms the previous state-of-the-art unsupervised approach by 13.5% on KITTI dataset. For the pose estimation task, our method performs comparably to the supervised methods that use ground-truth pose data for training. Besides, our unsupervised learning framework can significantly accelerate the initialization process of the traditional ORB-SLAM system and effectively improve the accuracy of environmental mapping in strong lighting and weak texture scenes.

关键词： Monocular depth estimation Pose estimation Unsupervised learning Visual SLAM system

来源：评论

学校读者我要写书评

暂无评论

Multi-representation knowledge distillation for audio classification

引用

MULTIMEDIA TOOLS AND APPLICATIONS 2022年第4期81卷 5089-5112页

作者： Gao, Liang Xu, Kele Wang, Huaimin Peng, Yuxing Natl Univ Def Technol Coll Comp Natl Key Lab Parallel & Distributed Proc Changsha 410073 Peoples R China

Audio classification aims to discriminate between different audio signal types, and it has received intensive attention due to its wide applications. In deep learning-based audio classification methods, researchers usually transform the raw signal of audios into different feature representations (such as Short Time Fourier Transform and Mel Frequency Cepstral Coefficients) as the inputs of networks. However, selecting the feature representation requires expert knowledge and extensive experimental verification. Besides, using a single type of feature representation may cause suboptimal results as the information implied in different kinds of feature representations may be complementary. Previous works show that ensembling the networks trained on different representations can greatly boost classification performance. However, making inferences using multiple networks is cumbersome and computation expensive. In this paper, we propose a novel end-to-end collaborative training framework for the audio classification task. The framework takes multiple representations as inputs to train the networks jointly with a knowledge distillation method. Consequently, our framework significantly promotes the performance of networks without increasing the computational overhead in the inference stage. Extensive experimental results demonstrate that the proposed approach improves classification performance and achieves competitive results on both acoustic scene classification tasks and general audio tagging tasks.

关键词： Neural networks Multiple representations Acoustic classification Knowledge distillation

来源：评论

学校读者我要写书评

暂无评论

A Push-Based Prefetching for Remote Caching RAM Grid

引用

INTERNATIONAL JOURNAL OF GRID AND HIGH PERFORMANCE COMPUTING 2009年第4期1卷 1-15页

作者： Chu, Rui Xiao, Nong Lu, Xicheng Natl Lab Parallel & Distributed Proc Xiamen Peoples R China

As an innovative grid computing technique for sharing the distributed memory resources in a high-speed wide-area network, RAM Grid exploits the distributed computing nodes, and provides remote memory for the user nodes which are short of memory. The performance of RAM Grid is constrained with the expensive network communication cost. In order to hide the latency of remote memory access and improve the performance, the authors proposed the push-based prefetching to enable the memory providers to push the potential useful pages to the user nodes. For each provider, it employs sequential pattern mining techniques, which adapts to the characteristics of memory page access sequences, on locating useful memory pages for prefetching. They have verified the effectiveness of the proposed method through trace-driven simulations.

关键词： Push-Based Prefetching RAM Grid Sequential Pattern Mining

来源：评论

学校读者我要写书评

暂无评论

Optimizing the Management of Reference Prediction Table for Prefetching and Prepromotion

引用

JOURNAL OF COMPUTERS 2010年第2期5卷 242-249页

作者： Wu, Junjie Yang, Xuejun Natl Lab Parallel & Distributed Proc Changsha Hunan Peoples R China

Prefetching and prepromotion are two important techniques for hiding the memory access latency. Reference prediction tables (RPT) plays a significant role in the process of prefetching or prepromoting data with linear memory access patterns. The traditional RPT management, LRU replacement algorithm, can not manage RPT efficiently. This leads to that large RPT has to be used for the considerable performance. The cost brought from the large capacity limits the usage of RPT in real processors. This paper uses bimodal insert policy (BIP) and proposed scalar filter policy (SFP) in the RPT management. Owing to matching the using characteristics of RPT, BIP can reduce the RPT thrashing and SFP can filter the useless scalar instructions in it. After testing 8 NPB benchmarks on a fullsystem simulator, we find that our approaches improve the RPT hit rate by 53.81% averagely, and increases prefetching and prepromotion operations by 18.85% and 53.55% averagely over the traditional LRU management.

关键词： reference prediction table prefetching prepromotion bimodal insert policy scalar filter policy cache memory

来源：评论

学校读者我要写书评

暂无评论

parallelizing skyline queries over uncertain data streams with sliding window partitioning and grid index

引用

KNOWLEDGE AND INFORMATION SYSTEMS 2014年第2期41卷 277-309页

作者： Li, Xiaoyong Wang, Yijie Li, Xiaoling Wang, Yuan Natl Univ Def Technol Coll Comp Natl Key Lab Parallel & Distributed Proc Changsha 410073 Hunan Peoples R China

Skyline query processing over uncertain data streams has attracted considerable attention in database community recently, due to its importance in helping users make intelligent decisions over complex data in many real applications. Although lots of recent efforts have been conducted to the skyline computation over data streams in a centralized environment typically with one processor, they cannot be well adapted to the skyline queries over complex uncertain streaming data, due to the computational complexity of the query and the limited processing capability. Furthermore, none of the existing studies on parallel skyline computation can effectively address the skyline query problem over uncertain data streams, as they are all developed to address the problem of parallel skyline queries over static certain data sets. In this paper, we formally define the parallel query problem over uncertain data streams with the sliding window streaming model. Particularly, for the first time, we propose an effective framework, named distributed parallel framework to address the problem based on the sliding window partitioning. Furthermore, we propose an efficient approach (parallel streaming skyline) to further optimize the parallel skyline computation with an optimized streaming item mapping strategy and the grid index. Extensive experiments with real deployment over synthetic and real data are conducted to demonstrate the effectiveness and efficiency of the proposed techniques.

关键词： Uncertain data Probabilistic skyline Data streams Skyline queries parallel queries Grid index

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：