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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

分类表

所选分类

>> <<

限定检索结果

标题

标题
作者
主题词
出版物名称
出版社
机构
学科分类号
摘要
ISBN
ISSN
基金资助
索书号

作者

作者
标题
主题词
出版物名称
出版社
机构
学科分类号
摘要
ISBN
ISSN
基金资助
索书号

文献类型

159 篇 会议
2 册 图书
2 篇 期刊文献

馆藏范围

163 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

89 篇 工学
- 73 篇 计算机科学与技术...
- 59 篇 软件工程
- 11 篇 建筑学
- 10 篇 机械工程
- 9 篇 土木工程
- 8 篇 电子科学与技术（可...
- 7 篇 光学工程
- 6 篇 信息与通信工程
- 5 篇 仪器科学与技术
- 5 篇 控制科学与工程
- 4 篇 农业工程
- 3 篇 材料科学与工程（可...
- 3 篇 生物医学工程（可授...
- 3 篇 生物工程
- 3 篇 安全科学与工程
- 2 篇 力学（可授工学、理...
- 2 篇 动力工程及工程热...
- 2 篇 电气工程
- 2 篇 航空宇航科学与技...
48 篇 理学
- 32 篇 数学
- 13 篇 物理学
- 4 篇 系统科学
- 4 篇 统计学（可授理学、...
- 3 篇 生物学
- 2 篇 地球物理学
12 篇 管理学
- 6 篇 管理科学与工程(可...
- 4 篇 图书情报与档案管...
10 篇 艺术学
- 9 篇 设计学（可授艺术学...
- 4 篇 美术学
4 篇 农学
- 4 篇 作物学
2 篇 医学
1 篇 法学

主题

18 篇 solid modeling
17 篇 computer aided d...
16 篇 rendering (compu...
13 篇 graphics process...
13 篇 three dimensiona...
10 篇 design automatio...
10 篇 mathematical mod...
9 篇 equations
8 篇 computational mo...
8 篇 visualization
8 篇 algorithm design...
7 篇 optimization
7 篇 image color anal...
7 篇 shape
7 篇 geometry
6 篇 interpolation
5 篇 model checking
5 篇 vectors
5 篇 computer graphic...
4 篇 buildings

机构

12 篇 tsinghua nationa...
11 篇 department of co...
11 篇 school of softwa...
9 篇 state key labora...
9 篇 key laboratory f...
7 篇 state key lab. o...
4 篇 state key labora...
3 篇 college of scien...
3 篇 school of comput...
3 篇 program of compu...
3 篇 school of comput...
2 篇 institute of mat...
2 篇 state key labora...
2 篇 liama/nlpr insti...
2 篇 school of comput...
2 篇 school of comput...
2 篇 college of compu...
2 篇 department of co...
2 篇 school of softwa...
2 篇 school of comput...

作者

6 篇 qunsheng peng
5 篇 peng qunsheng
3 篇 wang bin
3 篇 hai lin
3 篇 xueying qin
3 篇 junhai yong
3 篇 zhang hui
3 篇 qin xueying
2 篇 bin wang
2 篇 hoyano akira
2 篇 vardi moshe y.
2 篇 tao tao
2 篇 chen xiaowu
2 篇 bin pan
2 篇 li zongmin
2 篇 li chen
2 篇 pratt kevin b.
2 篇 he fazhi
2 篇 chen li
2 篇 meng xiangxu

语言

162 篇 英文
1 篇 中文

检索条件"任意字段=12th International Conference on Computer-Aided Design and Computer Graphics, CAD/Graphics 2011"

共 163 条记录，以下是151-160 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

A discrete strategy improvement algorithm for solving parity games 12th

A discrete strategy improvement algorithm for solving parity...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Vöge, Jens Jurdziński, Marcin Lehrstuhl für Informatik VII RWTH Aachen AachenD-52056 Germany BRICS Department of Computer Science University of Århus Ny Munkegade Bldg. 540 Arhus CDK-8000 Denmark

ISBN: (纸本)3540677704

A discrete strategy improvement algorithm is given for constructing winning strategies in parity games, thereby providing also a new solution of the model-checking problem for the modal μ-calculus. Known strategy improvement algorithms, as proposed for stochastic games by Hoffman and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these dificulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. the long standing problem whether parity games can be solved in polynomial time remains open. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Linear programming

来源：评论

学校读者我要写书评

暂无评论

Verifying advanced microarchitectures that support speculation and exceptions 12th

Verifying advanced microarchitectures that support speculati...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Hosabettu, Ravi Gopalakrishnan, Ganesh Srivas, Mandayam Department of Computer Science University of Utah Salt Lake CityUT84112 United States Computer Science Laboratory SRI International Menlo ParkCA94025 United States

ISBN: (纸本)3540677704

In this paper, we discuss the verification of a microprocessor involving a reorder buffer, a store buffer, speculative execution and exceptions at the microarchitectural level. We extend the earlier proposed Completion Functions Approach [HSG98] in a uniform manner to handle the verification of such microarchitectures. the key extension to our previous work was in systematically extending the abstraction map to accommodate the possibility of all the pending instructions being squashed. An interesting detail that arises in doing so is how the commutativity obligation for the program counter is proved despite the program counter being updated by both the instruction fetch stage (when a speculative branch may be entertained) and the retirement stage (when the speculation may be discovered to be incorrect). Another interesting detail pertains to how store buffers are handled. We highlight a new type of invariant in this work-one which keeps correspondence between store buffer pointers and reorder buffer pointers. All these results, taken together with the features handled using the completion functions approach in our earlier published work [HSG98,HSG99,HGS99], demonstrates that the approach is uniformly applicable to a wide variety of pipelined designs. © Springer-Verlag Berlin Heidelberg 2000.

关键词： computer architecture

来源：评论

学校读者我要写书评

暂无评论

Model checking continuous-Time Markov chains by transient analysis 12th

Model checking continuous-Time Markov chains by transient an...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Baier, Christel Haverkort, Boudewijn Hermanns, Holger Katoen, Joost-Pieter Institut für Informatik I University of Bonn Römerstraße 164 BonnD-53117 Germany Dept.of Computer Science RWTH Aachen Ahornstraße 55 AachenD-52056 Germany Dept.of Computer Science University of Twente P.O. Box 217 Enschede7500 AE Netherlands

ISBN: (纸本)3540677704

the verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branchingtime temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form P(image found)p(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator (image found), probability p, and real interval I. the main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. this allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Transient analysis

来源：评论

学校读者我要写书评

暂无评论

Binary reachability analysis of discrete pushdown timed automata 12th

Binary reachability analysis of discrete pushdown timed auto...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Dang, Zhe Ibarra, Oscar H. Bultan, Tevfik Kemmerer, Richard A. Su, Jianwen Department of Computer Science University of California Santa BarbaraCA93106 United States

ISBN: (纸本)3540677704

We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A configuration of a discrete pushdown timed automaton includes a control state, finitely many clock values and a stack word. Using a pure automata-theoretic approach, we show that the binary reachability (i.e., the set of all pairs of configurations (α, β), encoded as strings, such that α can reach β through 0 or more transitions) can be accepted by a nondeterministic pushdown machine augmented with reversal-bounded counters (NPCM). Since discrete timed automata with integer-valued clocks can be treated as discrete pushdown timed automata without the pushdown stack, we can show that the binary reachability of a discrete timed automaton can be accepted by a nondeterministic reversal-bounded multi-counter machine. thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversal- bounded NPCMs, the results can be used to verify a number of properties that cannot be expressed by timed temporal logics for discrete timed automata and CTL* for pushdown systems. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Clocks

来源：评论

学校读者我要写书评

暂无评论

Prioritized traversal: Efficient reachability analysis for verification and falsification 12th

Prioritized traversal: Efficient reachability analysis for v...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Fraer, Ranan Kamhi, Gila Ziv, Barukh Vardi, Moshe Y. Fix, Limor Logic and Validation Technology Intel Corporation Haifa Israel Dept. of Computer Science Rice University United States

ISBN: (纸本)3540677704

Our experience with semi-exhaustive verification shows a severe degradation in usability for the corner-case bugs, where the tuning effort becomes much higher and recovery from dead-ends is more and more difficult. Moreover, when there are no bugs at all, shifting semi-exhaustive traversal to exhaustive traversal is very expensive, if not impossible. this makes the output of semi-exhaustive verification on non-buggy designs very ambiguous. Furthermore, since after the design fixes each falsification task needs to converge to full verification, there is a strong need for an algorithm that can handle efficiently both verification and falsification. We address these shortcomings with an enhanced reachability algorithm that is more robust in detecting corner-case bugs and that can potentially converge to exhaustive reachability. Our approach is similar to that of Cabodi et al. in partitioning the frontiers during the traversal, but differs in two respects. First, our partitioning algorithm trades quality for time resulting in a significantly faster traversal. Second, the subfrontiers are processed according to some priority function resulting in a mixed BFS/DFS traversal. It is this last feature that makes our algorithm suitable for both falsification and verification. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Edge detection

来源：评论

学校读者我要写书评

暂无评论

Detecting errors before reaching them 12th

Detecting errors before reaching them

引用

12th international conference on computer aided Verification, CAV 2000

作者： De Alfaro, Luca Henzinger, thomas A. Mang, Freddy Y. C. Department of Electrical Engineering and Computer Sciences University of California at Berkeley CA94720-1770 United States

ISBN: (纸本)3540677704

Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rat- her than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs;for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated. the key observation is that "unpreventability" is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of "unpreventability," including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Achieving scalability in parallel reachability analysis of very large circuits 12th

Achieving scalability in parallel reachability analysis of v...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Heyman, Tamir Geist, Danny Grumberg, Orna Schuster, Assaf Computer Science Department Technion Haifa Israel IBM Haifa Research Laboratories Haifa Israel

ISBN: (纸本)3540677704

this paper presents a scalable method for parallel symbolic reachability analysis on a distributed-memory environment of workstations. Our method makes use of an adaptive partitioning algorithm which achieves high reduction of space requirements. the memory balance is maintained by dynamically repartitioning the state space throughout the computation. A compact BDD representation allows coordination by shipping BDDs from one machine to another, where different variable orders are allowed. the algorithm uses a distributed termination protocol with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk;rather, we make use of the network which is much faster. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Our initial performance evaluation using several large circuits shows that our method can handle models that are too large to fit in the memory of a single node. the efficiency of the partitioning algorithm is linear in the number of workstations employed, with a 40-60% efficiency. A corresponding decrease of space requirements is measured throughout the reachability analysis. Our results show that the relatively-slow network does not become a bottleneck, and that computation time is kept reasonably small. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Efficiency

来源：评论

学校读者我要写书评

暂无评论

Efficient detection of global properties in distributed systems using partial-order methods

Efficient detection of global properties in distributed syst...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Stoller, Scott D. Unnikrishnan, Leena Liu, Yanhong A. Computer Science Dept Indiana University BloomingtonIN47405-7104 United States

ISBN: (纸本)3540677704

A new approach is presented for detecting whether a particular computation of an asynchronous distributed system satisfies Poss ɸ (read "possibly ɸ"), meaning the system could have passed through a global state satisfying predicate ɸ, or Def ɸ (read "definitely ɸ"), meaning the system definitely passed through a global state satisfying ɸ. Detection can be done easily by straightforward state-space search;this is essentially what Cooper and Marzullo proposed. We show that the persistent-set technique, a well-known partial-order method for optimizing state-space search, provides efficient detection. this approach achieves the same worst-case asymptotic time complexity as two special- purpose detection algorithms of Garg and Waldecker that detect Poss ɸ and Def ɸ for a restricted but important class of predicates. For Poss ɸ, our approach applies to arbitrary predicates and thus is more general than Garg and Waldecker’s algorithm. We apply our algorithm for Poss ɸ to two examples, achieving a speedup of over 700 in one example and over 70 in the other, compared to unoptimized state-space search. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Distributed computer systems

来源：评论

学校读者我要写书评

暂无评论

Boolean satisfiability with transitivity constraints 12th

Boolean satisfiability with transitivity constraints

引用

12th international conference on computer aided Verification, CAV 2000

作者： Bryant, Randal E. Velev, Miroslav N. Computer Science Carnegie Mellon University PittsburghPA United States Electrical and Computer Engineering Carnegie Mellon University PittsburghPA United States

ISBN: (纸本)3540677704

We consider a variant of the Boolean satisfiability problem where a subset Ε of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, ei,j, for 1 ≤ i i andj. the task is to either find a satisfying assignment to Fsat that also satisfies all transitivity constraints over the relational variables (e.g., e1,2 ^ e2,3 ⇒ e1,3), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. this procedure forms the core of our tool for verifying pipelined microprocessors. To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing Fsat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables. To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets Ε, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of Fsat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Problem solving

来源：评论

学校读者我要写书评

暂无评论

Combining decision diagrams and SAT procedures for efficient symbolic model checking 12th

Combining decision diagrams and SAT procedures for efficient...

引用

12th international conference on computer aided Verification, CAV 2000

作者： Williams, Poul F. Biere, Armin Clarke, Edmund M. Gupta, Anubhav Department of Information Technology Technical University of Denmark LyngbyDK-2800 Denmark Department of Computer Science Institute of Computer Systems ETH Zentrum Zürich8092 Switzerland School of Computer Science Carnegie Mellon University PittsburghPA15213 United States

ISBN: (纸本)3540677704

In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. the method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a liveness property of a 256 bit shift-and-add multiplier and we are able to find a previously undetected bug in the specification of a 16 bit multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice. Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). the basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of basic steps. In particular the optimization rule of quantification-by-substitution turned out to be very useful: Ǝx: g ^ (x ⇔ f) ≡ g[f / x]. the rule is used (1) during fixed point iterations, (2) for deciding whether an initial set of states is a subset of another set of states, and finally (3) for iterative squaring. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Binary decision diagrams

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共17页 << < 8 9 10 11 12 13 14 15 16 17 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：