首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   5篇
  完全免费   2篇
  自动化技术   7篇
  2019年   1篇
  2015年   1篇
  2013年   1篇
  2005年   1篇
  2004年   2篇
  2001年   1篇
排序方式: 共有7条查询结果,搜索用时 140 毫秒
1
1.
The desired security properties of electronic voting protocols include verifiability, accuracy, democracy and fairness. In this paper we use a static program analysis tool to validate these properties for one of the classical voting protocols under appropriate assumptions. The protocol is formalised in an extension of the LySa process calculus with blinding signatures. The analysis, which is fully automatic, pinpoints previously undiscovered flaws related to verifiability and accuracy and we suggest modifications of the protocol needed for validating these properties.  相似文献
2.
In a typical COBOL program, the data division consists of 50% of the lines of code. Automatic type inference can help to understand the large collections of variable declarations contained therein, showing how variables are related based on their actual usage. The most problematic aspect of type inference is pollution, the phenomenon that types become too large, and contain variables that intuitively should not belong to the same type. The aim of the paper is to provide empirical evidence for the hypothesis that the use of subtyping is an effective way for dealing with pollution. The main results include a tool set to carry out type inference experiments, a suite of metrics characterizing type inference outcomes, and the experimental observation that only one instance of pollution occurs in the case study conducted.  相似文献
3.
In this paper we design abstract domains for power analysis. These domains are conceived to discover properties of the following type: The variable X at a given program point is the power of c with the exponent having a given property , where c and are automatically determined. This construction is general and includes different algebraic entities, such as numerical and polynomial (with rational coefficients), as bases. Several families of domains are presented, some of these consider that the exponent can be any natural or integer value, the others also include the analysis of properties of the exponent set. Relevant lattice-theoretic properties of these domains are proved such as the absence of infinite ascending chain and the structure of their meet-irreducible elements. The numerical domains are applied in the analysis of integer powers of imperative programs and in the analysis of probabilistic concurrent programming, with probabilistic non-deterministic choice. Moreover we use the numerical power domains in order to analyze the factorization of integer variables, i.e., invariant properties of factors and of their exponents. In this way we are able to statically detect information hidden in prime factorization, which can be used in software watermarking.  相似文献
4.
We present a method for analyzing assembly programs obtained by compilation and checking safety properties on compiled programs. It proceeds by analyzing the source program, translating the invariant obtained at the source level, and then checking the soundness of the translated invariant with respect to the assembly program. This process is especially adapted to the certification of assembly or other machine-level kinds of programs. Furthermore, the success of invariant checking enhances the level of confidence in the results of both the compilation and the static analysis. From a practical point of view, our method is generic in the choice of an abstract domain for representing sets of stores, and the process does not interact with the compilation itself. Hence a certification tool can be interfaced with an existing analyzer and designed so as to work with a class of compilers that do not need to be modified. Finally, a prototype was implemented to validate the approach.  相似文献
5.
Traversal strategies à la Stratego (also à la Strafunski and ‘Scrap Your Boilerplate’) provide an exceptionally versatile and uniform means of querying and transforming deeply nested and heterogeneously structured data including terms in functional programming and rewriting, objects in OO programming, and XML documents in XML programming.  相似文献
6.
对称多处理器的飞速发展和近年来提出的动态异构处理器(DHMP)为性能优化提供了新的机遇。一个机遇是找出程序每个阶段的性能瓶颈,提出了静态程序阶段分析方法,即通过分析结构参数和计算相似度矩阵来找出程序每个阶段的资源瓶颈;另一个机遇是给出动态异构处理器重构的时间节点,提出了DPDA和HTPD两种动态阶段检测算法,检测出阶段的变化能够为动态可重构处理器提供重构的时间节点。DPDA算法效果很好且软硬件实现代价小,而HTPD算法是目前为止第一个使用统计学方法进行动态检测阶段的算法。实验表明,与BBV相比,DPDA和HTPD能避免BBV离线、动态算法需添加额外硬件、结果与编译器相关等限制,并且阶段划分的稳定性和正确率与BBV相当。DPDA和HTPD算法由于本身不依赖额外硬件,因此都能直接在主流处理器和动态异构处理器(DHMP)中使用。  相似文献
7.
金芝  刘芳  李戈 《软件学报》2019,30(1):110-126
程序理解是软件工程中的关键活动,在软件开发、维护、重用等任务中发挥着重要的作用.程序理解自软件工程出现以来,就一直是该领域的研究热点.随着软件应用的日益复杂和不断普及,程序理解研究的需求发生了新的变化,程序的自理解或自认知逐渐成为新的关注点,有必要对程序理解进行重新审视.从工程、学习和认知以及方法和技术这3个角度定位程序理解任务;随后,通过文献分析展示其研究布局,进而分别从认知过程、理解技术以及软件工程任务中的应用这3个方面,综合论述程序理解研究的发展脉络和研究进展.  相似文献
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号