检索结果-南通市图书馆

Conditional Congruence Closure over Uninterpreted and Interpreted Symbols

在线全文

学校读者我要写书评

暂无评论

Journal of Systems Science & Complexity 2019年第1期32卷 317-355页

作者： kapur deepak Department of Computer Science University of New Mexico

A framework for generating congruence closure and conditional congruence closure of ground terms over uninterpreted as well as interpreted symbols satisfying various properties is proposed. It is based on some of the key concepts from kapur's congruence closure algorithm(RTA97)for ground equations based on introducing new symbols for all nonconstant subterms appearing in the equation set and using ground completion on uninterpreted constants and puri?ed equalities over interpreted symbols belonging to different theories. In the original signature, the resulting rewrite systems may be nonterminating but they still generate canonical forms. A byproduct of this framework is a constant Horn completion algorithm using which ground canonical Horn rewrite systems can be generated for conditional ground *** effcient algorithms for generating congruence closure of conditional and unconditional equations on ground terms over uninterpreted symbols are presented. The complexity of the conditional congruence closure is shown to be O(n*log(n)), which is the same as for unconditional ground *** proposed algorithm is motivated by our attempts to generate effcient and succinct interpolants for the quanti?er-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and need additional simpli?cation. A completion algorithm to generate a canonical conditional rewrite system from ground conditional equations is also presented. The framework is general and ?exible and is used later to develop congruence closure algorithms for cases when function symbols satisfy simple properties such as commutativity, nilpotency, idempotency and identity as well as their combinations. Interesting outcomes include algorithms for canonical rewrite systems for ground equational and conditional theories on uninterpreted and interpreted symbols leading to generation of canonical forms for ground terms, constrained terms and Horn equat

关键词： Completion congruence closure conditional congruence closure intepreted symbols rewrit-ing uninterpreted symbols

ON INVARIANT CHECKING

在线全文

学校读者我要写书评

暂无评论

Journal of Systems Science & Complexity 2013年第3期26卷 470-482页

作者： ZHANG Zhihai kapur deepak School of Mathematical Sciences Peking University Department of Computer Science University of New Mexico

Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable *** is especially the case if the given formula is not an inductive loop invariant,as most automated techniques can only check or generate inductive loop *** this paper,conditions are identified on simple loops and formulas when this check can be performed automatically.A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a *** a byproduct of this analysis,a new kind of loop invariant inside the loop body,called inside-loop invariant,is *** an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program *** use of such invariants for program debugging is explored;it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow,accessing array/collection data structures outside the range,divide by zero,etc.

关键词： Assertion Floyd-Hoare logic invariant invariant generation.

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

在线全文

学校读者我要写书评

暂无评论

Journal of Systems Science & Complexity 2006年第3期19卷 307-330页

作者： deepak kapur Department of Computer Science University of New MexicoAlbuquerqueUSA

A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.

关键词： Automated software analysis and verification inductive assertion loop invariant quantifier elimination.

在线全文

学校读者我要写书评

暂无评论

结膜黏液表皮样癌：透明细胞变异型

美国医学会眼科杂志（中文版） 2006年第4期18卷 237-239,209页

作者： Rashmi kapur Joel Sugar deepak P.Edward 冯云（译）赵光喜（校）

结膜黏液表皮样癌是一种罕见的结膜新生物,是唾液腺的常见恶性肿瘤.在结膜上它往往类似于鳞状细胞癌.肿瘤的组织学起源被认为是多能造血母细胞，还可能有黏液分秘成分，因此肿瘤由黏液分泌细胞组成其间混合表皮细胞。

关键词：黏液表皮样癌透明细胞变异型恶性肿瘤混合表皮细胞造血母细胞鳞状细胞癌

Bimatoprost引起眼部周围皮肤色素沉着组织病理学研究

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

美国医学会眼科杂志（中文版） 2006年第4期18卷 210-215页

作者： Rashmi kapur Smajo Osmanovic Sami Toyran deepak P. Edward 陆遥（译）赵光喜（校） Department of Ophthalmology and Visual Sciences University of Illinois Chicago Department of Ophthalmology and Visual Sciences Arlington Eye Physicians Arlington Heights Ⅲ 不详

目的：研究卢美根引起眼部周围皮肤色素沉着的光镜和超微结构的改变。方法：取使用卢美根后患者和对照患者的眼睑组织活检标本．进行光镜和透射电镜关。利用图形分析器。在Fontana-Masson-染色切片上计数黑色素颗粒。抗S100和CD3抗体进... 详细信息

目的：研究卢美根引起眼部周围皮肤色素沉着的光镜和超微结构的改变。方法：取使用卢美根后患者和对照患者的眼睑组织活检标本．进行光镜和透射电镜关。利用图形分析器。在Fontana-Masson-染色切片上计数黑色素颗粒。抗S100和CD3抗体进行免疫组化分析。计数阳性标记的细胞。结果：在光镜下。黑色素颗粒数量在使用卢美根后患者的眼睑标本中明显增加。电镜下显示皮肤的黑色素细胞具有明显的粗面内质网和丰富的正常大小的色素颗粒。与正常标本相比处于不同的成熟阶段。使用卢美根后眼睑标本的角化细胞与正常对照相比显示丰富的成熟色素颗粒。此外值得注意的是。两种标本中都没有非典型的色素细胞。S100-阳性的黑色素细胞在使用卢美根和对照组眼睑标本的数量相当。两组中几乎没有CD-3和CD-68阳性的细胞。结论：Bimatoprost引起的眼周色素沉着是由黑色素生成增加所致。在观察的标本上没有证据显示黑色素细胞增殖或前列腺素诱导的炎症反应发生。

关键词：皮肤色素沉着组织病理学周围眼部 Bi 黑色素颗粒黑色素细胞活检标本