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

A Syntactic Proofof the Conservativity of λ_ω over λ_2

Journal of computer science & technology 1999年第2期14卷 129-134页

作者：宋方敏钱悦晨 Department of Computer Science and Technology State Key Laboratory for Novel Software Technology Nanjing University Nanjing P.R. China

In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.

关键词： calculus second order typed -calculus

来源：评论

学校读者我要写书评

暂无评论

An object-based model for cooperative computing

引用

science China(Technological sciences) 1998年第1期41卷 22-30页

作者：茅兵谢立 1. Department of Computer Science and Technology State Key Laboratory for Novel Software Technology Nanjing University 210093 Nanjing China

A cooperative computing model is presented to support the construction of CSCW systems. The model divides a cooperative system into layers and each layer is formed by component objects. A principal focus of the model is the provision of an object linking mechanism which links the relevant objects in the same layer of multiple users to realize multi-level collaboration which is independent of the application. In addition, multi-level collaboration obtains fine-grained collaboration and improves collaboration efficiency. The object-based method used ensures a structured collaboration and facilitates cooperative system development.

关键词： CSCW collaboration management multi-level cooperation object linking.

来源：评论

学校读者我要写书评

暂无评论

What is Discussed about COVID-19:A Multi-Modal Framework for Analyzing Microblogs from Sina Weibo without Human labeling

引用

computers, Materials & Continua 2020年第9期64卷 1453-1471页

作者： Hengyang Lu Yutong Lou Bin Jin Ming Xu School of Artificial Intelligence and Computer Science Jiangnan UniversityWuxi214122China National Key Laboratory for Novel Software Technology Department of Computer Science and TechnologyNanjing UniversityNanjing210023China

Starting from late 2019,the new coronavirus disease(COVID-19)has become a global *** the development of online social media,people prefer to express their opinions and discuss the latest news *** have witnessed the positive influence of online social media,which helped citizens and governments track the development of this pandemic in *** is necessary to apply artificial intelligence(AI)techniques to online social media and automatically discover and track public opinions posted *** this paper,we take Sina Weibo,the most widely used online social media in China,for analysis and *** collect multi-modal microblogs about COVID-19 from 2020/1/1 to 2020/3/31 with a web crawler,including texts and images posted by *** order to effectively discover what is being discussed about COVID-19 without human labeling,we propose a unified multi-modal framework,including an unsupervised short-text topic model to discover and track bursty topics,and a self-supervised model to learn image features so that we can retrieve related images about *** results have shown the effectiveness and superiority of the proposed models,and also have shown the considerable application prospects for analyzing and tracking public opinions about COVID-19.

关键词： COVID-19 public opinion microblog topic model self-supervised learning

来源：评论

学校读者我要写书评

暂无评论

Understanding and Detecting Inefficient Image Displaying Issues in Android Apps

引用

Journal of computer science & technology 2024年第2期39卷 434-459页

作者：李文杰马骏蒋炎岩许畅马晓星 State Key Laboratory of Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China

Mobile applications(apps for short)often need to display ***,inefficient image displaying(IID)issues are pervasive in mobile apps,and can severely impact app performance and user *** paper first establishes a descriptive framework for the image displaying procedures of IID *** on the descriptive framework,we conduct an empirical study of 216 real-world IID issues collected from 243 popular open-source Android apps to validate the presence and severity of IID issues,and then shed light on these issues’characteristics to support research on effective issue *** the findings of this study,we propose a static IID issue detection tool TAPIR and evaluate it with 243 real-world Android ***,49 and 64 previously-unknown IID issues in two different versions of 16 apps reported by TAPIR are manually confirmed as true positives,respectively,and 16 previously-unknown IID issues reported by TAPIR have been confirmed by developers and 13 have been ***,we further evaluate the performance impact of these detected IID issues and the performance improvement if they are *** results demonstrate that the IID issues detected by TAPIR indeed cause significant performance degradation,which further show the effectiveness and efficiency of TAPIR.

关键词： Android application(app) inefficient image displaying(IID) performance empirical study static analysis

来源：评论

学校读者我要写书评

暂无评论

On interleaving space exploration of multi-threaded programs

引用

Frontiers of computer science 2021年第4期15卷 17-28页

作者： Dongjie CHEN Yanyan JIANG Chang XU Xiaoxing MA State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China

Exploring the interleaving space of a multithreaded program to efficiently detect concurrency bugs is important but also difficult because of the astronomically many thread *** paper presents a novel framework to decompose a thread schedule generator that explores the interleaving space into the composition of a basic generator and its extension under the“small interleaving hypothesis”.Under this framework,we in-depth analyzed research work on interleaving space exploration,illustrated how to design an effective schedule generator,and shed light on future research opportunities.

关键词： survey testing concurrency bugs interleaving space

来源：评论

学校读者我要写书评

暂无评论

Detecting and Tracking Moving Targets on Omnidirectional Vision

引用

Transactions of Tianjin University 2009年第1期15卷 13-18页

作者：杨淑莹葛为民张成何丕廉 School of Computer Science and Technology Tianjin University Tianjin Key Lab of Intelligent Computing and Novel Software Technology Tianjin University of Technology

A method was presented to implement the detecting and tracking of moving targets through omnidirec-tional vision. The method combined optical flow with particle filter arithmetic, in which optical flow field was used to detect and locate moving targets and particle filter was used to track the detected moving objects. According to the circular image character of omnidirectional vision, the calculation equation of optical flow field and the tracking arithmetic of particle filter were improved based on the polar coordinates at the omnidirectional center. The edge of a randomly moving object could be detected by optical flow field and was surrounded by a reference region in the particle filter. A dynamic motion model was established to predict particle state. Histograms were used as the fea-tures in the reference region and candidate regions. The mutual information (MI) and Gaussian function were com-bined to calculate particle weights. Finally, the state of tracked object was computed by the total particle states with weights. Experiment results show that the proposed method could detect and track moving objects with better real-time performance and accuracy.

关键词： omnidirectional vision optical flow particle filter mutual information

来源：评论

学校读者我要写书评

暂无评论

AATT+: Effectively manifesting concurrency bugs in Android apps

引用

science of computer Programming 2018年 163卷 1-18页

作者： Wang, Jue Jiang, Yanyan Xu, Chang Li, Qiwei Gu, Tianxiao Ma, Jun Ma, Xiaoxing Lu, Jian State Key Lab for Novel Software Technology Nanjing University Nanjing China Department of Computer Science and Technology Nanjing University Nanjing China

Smartphones are indispensable in people's daily activities, and smartphone apps tend to be increasingly concurrent due to the wide use of multi-core devices and technologies. Due to this tendency, developers are increasingly unable to tackle the complexity of concurrent apps and to avoid subtle concurrency bugs. To better address this issue, we propose a novel approach to detecting concurrency bugs in Android apps based on the fact that one can generate simultaneous input events and their schedules for an app, which would easily trigger concurrency bugs in an app. We conduct systematic state space exploration to find potentially conflicting resource accesses in an Android app. The app is then automatically pressure-tested by guided event and schedule generation. We implemented our prototype tool named AATT+ and evaluated it with two sets of real-world Android apps. Benchmarking using 15 Android apps with previously known concurrency bugs, AATT+ and existing concurrency-unaware techniques detected 10 and 1 bugs, respectively. Evaluated with another set of 17 popular Android apps, AATT+ detected 11 concurrency bugs and 7 of them were previously unknown, achieving an over 80% higher detection rate than existing concurrency-unaware techniques. © 2018 Elsevier B.V.

关键词： Smartphones

来源：评论

学校读者我要写书评

暂无评论

A program logic for obstruction-freedom

引用

Frontiers of computer science 2024年第6期18卷 85-100页

作者： Zhao-Hui LI Xin-Yu FENG School of Computer Science and Technology University of Science and Technology of ChinaHefei 230026China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China

Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed ***,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same *** also propose informal principles to extend a logic for verifying linearizability to verifying *** this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and ***,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.

关键词： verification program logic progress properties obstruction-freedom concurrent objects

来源：评论

学校读者我要写书评

暂无评论

Quantum programming languages: A tentative study

引用

science in China(Series F) 2008年第6期51卷 623-637页

作者： XU JiaFu SONG FangMin State Key Laboratory for Novel Software Technology Department of Computer Science and TechnologyNanjing University Nanjing 210093 China

Starting with some simple representative quantum programming languages, this paper lays stress on quantum computation, language paradigm, program structure, input/output, exception facility, and especially the recent results of the quantum computation group at Nanjing University, namely the functional quantum programming language NDQFP. All primitive functions and combining forms in NDQFP are given in the appendix.

关键词： quantum programming languages language paradigm imperative programming language declarative programming language lexical analyzer syntactic analyzer assembler interpreter

来源：评论

学校读者我要写书评

暂无评论

STAR-RIS and UAV Combination in MEC Networks: Simultaneous Task Offloading and Communications

引用

IEEE Transactions on Communications 2025年

作者： Xiao, Han Hu, Xiaoyan Wang, Wenjie Su, Zhou Wong, Kai-Kit Yang, Kun Xi'an Jiaotong University School of Information and Communications Engineering Xi'an710049 China Southeast University National Mobile Communications Research Laboratory Nanjing210096 China Xi'an Jiaotong University School of Cyber Science and Engineering Xi'an710049 China University College London Department of Electronic and Electrical Engineering Torrington Place LondonWC1E 7JE United Kingdom Yonsei University Yonsei Frontier Lab Seoul Korea Republic of Nanjing University State Key Laboratory of Novel Software Technology Nanjing210008 China School of Intelligent Software and Engineering Suzhou215163 China University of Essex School of Computer Science and Electronic Engineering Essex United Kingdom

This paper explores a simultaneous tasks offloading and communications (STOC) scheme in mobile edge computing (MEC) networks, supported by the combination of simultaneously transmitting and reflecting reconfigurable intelligent surface (STAR-RIS) and the unmanned aerial vehicle (UAV). Different from the traditional MEC schemes, the proposed scheme concurrently considers the computation and communication capabilities of the MEC networks, which is actually more practical in reality. Specifically, an optimization problem is devised to maximize the weighted sum of the minimum computed task data and communication data, while ensuring the quality of service (QoS) constraints for STOC through joint design of time scheduling, resource allocation, active and passive beamforming, alongside with the UAV trajectory planning. This non-convex problem with strong couplings among variables is challenging to solve directly. Then, a novel alternating optimization method is proposed, leveraging the successive convex approximation (SCA) and semi-definite relaxation (SDR) techniques. We provide sufficient numerical results to validate the effectiveness of the proposed STOC scheme, which demonstrate that the proposed scheme supported by STAR-RIS and UAV outperforms five benchmark schemes in terms of performance gain. It is important to note that the proposed scheme offers a feasible and realistic way for the implementations of STOC in practical MEC networks. © 1972-2012 IEEE.

关键词： Convex optimization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：