共查询到20条相似文献,搜索用时 140 毫秒
1.
2.
定点DSPs的定标及其运算方法 总被引:5,自引:0,他引:5
分析了定点DSPs的定标问题,讨论了定点运算中的Qs值选择和解决数值超范围的方法,提出了定点DSPs加法的通用处理方法,并就定点运算程序设计中的一些具体问题进行了讨论。 相似文献
3.
4.
5.
网络拓扑发现中的路由器别名识别技术研究与实现 总被引:7,自引:0,他引:7
网络拓扑发现技术的关键问题之一就是研究路由器之间的连接关系。路由器别名问题是网络拓扑发现技术研究中的一个重要问题,它是指路由器具有多个不同的接口地址,在Internet上可以使用其中的任一地址来标识同一路由器。该文详细描述了路由器别名问题,及其对网络拓扑发现结果带来的影响;重点分析了RFC1122标准中有关路由器的通信规范,描述了别名探子方法的实现原理,并给出了不同应用条件下该方法的实现流程。试验发现,别名探子扫描结果的完整性与目标网络和其他网络连接关系的复杂性有很大关系。分析表明,别名探子方法还存在着种种局限,但在实际应用中,该方法仍不失为一种有效的方法。 相似文献
6.
7.
邮箱用户身份信息挖掘是数据挖掘研究的一个热点。当前相关研究大多仅从邮件头中抽取邮箱用户的别名,遗漏了邮件正文中潜藏的更能代表通信双方身份的别名信息。针对纯文本邮件正文中邮箱用户别名信息抽取问题,提出了基于统计和规则过滤的称呼块和签名块定位算法,该算法能高效准确地从邮件正文中提取出蕴涵邮箱用户别名的称呼块和签名块文本片段;进一步提出了基于别名边界词汇模板修正的别名抽取方法,从而提高了仅基于命名实体识别或词性标注工具识别别名的准确率。实验结果表明,提出的方法可以有效地抽取出邮件正文中邮箱用户的别名。 相似文献
8.
锁别名分析能够得到锁指针变量的指向信息,有效的锁别名分析可以更好地辅助数据竞争分析和死锁分析.现有锁别名分析往往采用保守的方式处理,进而影响分析结果的准确性.针对这一问题,提出了一种锁别名分析方法,该方法首先使用GCC插件获取SSA形式的中间代码,然后对中间代码进行预处理以获得与锁、函数指针操作相关的语句,最后对预处理后的程序使用本文提出的FP_LOCK算法进行准确的流敏感、上下文敏感分析.实验结果表明该方法能精确地确定锁别名,并且经过预处理后的FP_LOCK算法对分析大程序平均有9.95倍的加速比. 相似文献
9.
别名分析对于数据流分析、程序优化和分析工具的实现非常重要.文章提出了一种需求驱动,流非敏感的分析算法来解决指针别名问题.通过构造程序表达式图(PEG)把指针别名问题转化成判断两个指针节点是否是联通的问题,它不同于传统的别名分析方法,它不需要构造别名集合和对其求交集,所以提高了分析指针别名的效率. 相似文献
10.
别名分析的精度影响着很多其他编译优化的效果。在对展开后的循环体做指令调度的时候,不精确的别名分析结果会导致冗余数据依赖的产生,从而限制了调度。流敏感的别名分析因为代价过高而扩展性不好。在流不敏感别名信息的基础上,提出了一种需求驱动的流敏感别名检查方法,能够以流敏感的方式判断两个表达式在某程序点上是否为别名。该方法假设两个表达式之间具有别名关系,从而获取初始的数据流事实。用数据流分析技术计算逆向程序点上的数据流事实。如果在所有逆向路径上的数据流事实中都产生了矛盾,则认为别名关系不成立。实验结果表明,该方法能较好地提高别名分析的精度。 相似文献
11.
Yifeng Chen 《Formal Aspects of Computing》2013,25(1):89-106
This paper introduces a number of new techniques that support systematic manipulation of predicates, operators, healthiness conditions, laws and fixpoints of recursive programs. Necessary restrictions are imposed on the definition of each model so that the inheritance relation can be established by checking a few conditions on the healthiness conditions and the commands. In particular, we intend to identify the conditions that simplify the closure proof of the program operators and enable laws and fixpoints of a model to be inherited by its submodel without re-proof. A recursive program may correspond to different recursive functions in a model and its submodels, because the primitives such as abort and assignment statements are normally represented as different predicates in different models (although the original definition of each operator is unchanged). This paper studies meta-theory in this more general setting. A fixpoint theorem is discovered and applied to clarify the relationship between the partially correct relational model and the totally correct sequential model in UTP. It is shown that, although assignment statements are modified by the new healthiness conditions in the latter model, most laws (including many that are re-proved in UTP) and fixpoints can be inherited directly without re-proof, if the first argument of every sequential composition in each command tree corresponds to a terminating computation. This result also singles out a small number of laws and fixpoints that may no longer hold in the totally correct model. 相似文献
12.
We present a new model checking algorithm for verifying computation tree logic (CTL) properties. Our technique is based on
using language inference to learn the fixpoints necessary for checking a CTL formula instead of computing them iteratively
as is done in traditional model checking. This allows us to analyze infinite or large state-space systems where the traditional
iterations may not converge or may take too long to converge. We allow fairness constraints to be specified for verification
of various liveness properties. The main challenge in developing a learning based model checking algorithm for CTL is that
CTL properties express nested fixpoints. We overcome this challenge by developing a new characterization of CTL properties
in terms of functions that have unique fixpoints. We instantiate our technique to systems in which states are encoded as strings
and use a regular inference algorithm to learn the CTL fixpoints. We prove that if the fixpoints have a regular representation,
our procedure will always terminate with the correct answer. We have extended our Lever tool to use the technique presented
in this paper and demonstrate its effectiveness by verifying a number of parametric and integer systems.
A preliminary version of this work appeared in the proceedings of the twentieth IEEE/ACM International conference on Automated
Software Engineering, Long Beach, California, USA, 2005.
Part of the work was done when the first author was at the University of Illinois.
Supported in part by DARPA/AFOSR MURI Award F49620-02-1-0325 and NSF 04-29639. 相似文献
13.
Parallel algorithm for computing fixpoints of Galois connections 总被引:1,自引:0,他引:1
Petr Krajca Jan Outrata Vilem Vychodil 《Annals of Mathematics and Artificial Intelligence》2010,59(2):257-272
This paper presents a parallel algorithm for computing fixpoints of Galois connections induced by object-attribute relational
data. The algorithm results as a parallelization of CbO (Kuznetsov 1999) in which we process disjoint sets of fixpoints simultaneously. One of the distinctive features of the algorithm compared
to other parallel algorithms is that it avoids synchronization which has positive impacts on its speed and implementation.
We describe the parallel algorithm, prove its correctness, and analyze its asymptotic complexity. Furthermore, we focus on
implementation issues, scalability of the algorithm, and provide an evaluation of its efficiency on various data sets. 相似文献
14.
We present an algorithm for computing the uniquely determined least fixpoints of self-maps on \(\overline{\mathbb{R}}^{n}\) (with \(\overline{\mathbb{R}} = \mathbb{R} \cup\{ \pm\infty\}\)) that are point-wise maximums of finitely many monotone and order-concave self-maps. This natural problem occurs in the context of systems analysis and verification. As an example application we discuss how our method can be used to compute template-based quadratic invariants for linear systems with guards. The focus of this article, however, lies on the discussion of the underlying theory and the properties of the algorithm itself. 相似文献
15.
We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well-structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common. 相似文献
16.
In languages with unbounded demonic and angelic nondeterminacy, functions acquire a surprisingly rich set of fixpoints. We
show how to construct these fixpoints, and describe which ones are suitable for giving a meaning to recursively defined functions.
We present algebraic laws for reasoning about them at the language level, and construct a model to show that the laws are
sound. The model employs a new kind of power domain-like construct for accommodating arbitrary nondeterminacy. 相似文献
17.
Refining abstract interpretations 总被引:1,自引:0,他引:1
Bhargav S. Gulavani Supratik Chakraborty Sriram K. Rajamani 《Information Processing Letters》2010,110(16):666-671
Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present a dag-based abstraction refinement technique to automatically refine such abstract interpretations and reduce false errors. This technique refines precision loss due to widen operator by a new interpolated widen operator and refines precision loss due to join operator by disjunctions. We prove the soundness and progress properties of this abstraction refinement procedure. 相似文献
18.
Peter Höfner 《Theoretical computer science》2011,412(28):3303-3322
In computer science, fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However, there are situations where other ones are needed. In this paper, we study, on an algebraic base, a special fixpoint of the function f(x)=a⋅x that describes infinite iteration of an element a. We show that the greatest fixpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis. 相似文献
19.
Erik Sandewall 《Computational Intelligence》1985,1(1):80-87
Axiom sets and their extensions are viewed as functions from the set of formulas in the language to a set of four truth values, t, f, u for undefined, and k for contradiction. Such functions form a lattice with “contains less information” as the partial order ?, and “combination of several sources of knowledge” as the least-upper-bound operation ?. Inference rules are expressed as binary relations between such functions. We show that the usual criterium on fixpoints, namely, to be minimal, does not apply correctly in the case of non-monotonic inference rules. A stronger concept, approachable fixpoints, is introduced and proven to be sufficient for the existence of a derivation of the fixpoint. In addition, the usefulness of our approach is demonstrated by concise proofs for some previously known results about normal default rules. 相似文献
20.
《The Journal of Logic Programming》1995,22(3):211-222
Despite the frequent comment that there is no general agreement on the semantics of logic programs, this paper shows that a number of independently proposed extensions to the stable model semantics coincide: the regular model semantics proposed by You and Yuan, the partial stable model semantics by Saccà and Zaniolo, the preferential semantics by Dung, and a stronger version of the stable class semantics by Baral and Subrahmanian. We show that these equivalent semantics can be characterized simply as selecting a particular kind of stable classes, called normal alternating fixpoints. In addition, we indicate that almost all of the previously proposed semantic frameworks coincide with that of normal alternating fixpoints. Due to its simplicity and naturalness, the framework of normal alternating fixpoints offers great potential in the study of the semantics for various nonmonotonic systems. 相似文献