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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

144 篇 会议
13 册 图书

馆藏范围

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

日期分布

学科分类号

127 篇 工学
- 126 篇 计算机科学与技术...
- 75 篇 软件工程
- 6 篇 电气工程
- 3 篇 信息与通信工程
- 3 篇 控制科学与工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 生物医学工程（可授...
38 篇 理学
- 37 篇 数学
- 1 篇 生物学
4 篇 管理学
- 3 篇 图书情报与档案管...
- 1 篇 管理科学与工程(可...
- 1 篇 工商管理
1 篇 医学
- 1 篇 基础医学(可授医学...
- 1 篇 临床医学
- 1 篇 药学(可授医学、理...

主题

38 篇 logic programmin...
11 篇 program transfor...
10 篇 logics and meani...
9 篇 computer circuit...
8 篇 semantics
8 篇 artificial intel...
7 篇 mathematical log...
6 篇 software enginee...
6 篇 programming tech...
5 篇 software enginee...
5 篇 program analysis
5 篇 programming lang...
4 篇 program synthesi...
4 篇 constraint handl...
3 篇 source-to-source...
2 篇 program debuggin...
2 篇 floating-point n...
2 篇 concurrent const...
2 篇 types
2 篇 program slicing

机构

4 篇 univ politecn va...
3 篇 katholieke univ ...
3 篇 nagoya inst tech...
3 篇 imdea software i...
2 篇 univ politecn ma...
2 篇 univ fed rio gra...
2 篇 univ politecn va...
2 篇 katholieke univ ...
2 篇 univ southern de...
2 篇 rhein westfal th...
2 篇 imdea software
2 篇 rhein westfal th...
2 篇 univ complutense...
2 篇 univ north texas...
2 篇 tech u madrid sc...
2 篇 michigan state u...
2 篇 univ new mexico ...
2 篇 univ new mexico ...
2 篇 ecole polytech l...
2 篇 univ ulm d-89069...

作者

6 篇 vidal german
4 篇 schneider-kamp p...
4 篇 silva josep
4 篇 falaschi moreno
4 篇 seki hirohisa
4 篇 abdennadher slim
4 篇 giesl juergen
3 篇 proietti maurizi...
3 篇 hermenegildo man...
3 篇 carro manuel
3 篇 hermenegildo m
3 篇 morales jose f.
3 篇 de schreye danny
3 篇 leuschel michael
3 篇 lucas salvador
3 篇 meseguer jose
2 篇 puebla german
2 篇 bruynooghe mauri...
2 篇 senni valerio
2 篇 michael hanus

语言

154 篇 英文
3 篇 中文

检索条件"任意字段=16th International Symposium on Logic-Based Program Synthesis and Transformation"

共 157 条记录，以下是101-110 订阅

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

详细简洁

排序：

Analyzing Array Manipulating programs by program transformation 24th

Analyzing Array Manipulating Programs by Program Transformat...

引用

24th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Cornish, J. Robert M. Gange, Graeme Navas, Jorge A. Schachte, Peter Sondergaard, Harald Stuckey, Peter J. Univ Melbourne Dept Comp & Informat Syst Melbourne Vic 3010 Australia NASA Ames Res Ctr Moffett Field Mountain View CA 94035 USA

ISBN: (纸本)9783319178226;9783319178219

We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as "every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j]." We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.

关键词： Machinery

来源：评论

学校读者我要写书评

暂无评论

On the Completeness of Selective Unification in Concolic Testing of logic programs 26th

On the Completeness of Selective Unification in Concolic Tes...

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Mesnard, Fred Payet, Etienne Vidal, German Univ Reunion LIM St Denis Reunion France Univ Politecn Valencia DSIC MiST Valencia Spain

ISBN: (纸本)9783319631394;9783319631387

Concolic testing is a popular dynamic validation technique that can be used for both model checking and automatic test case generation. We have recently introduced concolic testing in the context of logic programming. In contrast to previous approaches, the key ingredient in this setting is a technique to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. this is called "selective" unification. In this paper, we show that the existing algorithm is not complete and explore different alternatives in order to have a sound and complete algorithm for selective unification.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Symbolic Abstract Contract synthesis in a Rewriting Framework 26th

Symbolic Abstract Contract Synthesis in a Rewriting Framewor...

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Alpuente, Maria Pardo, Daniel Villanueva, Alicia Univ Politecn Valencia DSIC Camino Vera S-N E-46022 Valencia Spain

ISBN: (纸本)9783319631394;9783319631387

We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K framework, we enrich the symbolic execution facilities recently provided by C with novel capabilities for assertion synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.0, which generates logical axioms that define the precise input/ output behavior of the C routines.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Multivariant Assertion-based Guidance in Abstract Interpretation 28th

Multivariant Assertion-Based Guidance in Abstract Interpreta...

引用

28th international symposium on logic-based program synthesis and transformation (LOPSTR(

作者： Garcia-Contreras, Isabel Morales, Jose F. Hermenegildo, Manuel, V IMDEA Software Inst Madrid Spain Univ Politecn Madrid UPM Madrid Spain

ISBN: (纸本)9783030138387;9783030138370

Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent precision loss, typically at the expense of larger resource consumption. In both cases (i.e., when analysis produces inaccurate results and when resource consumption is too high), it is necessary to have some means for users to provide information to guide analysis and thus improve precision and/or performance. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance/context-sensitivity, and can handle different run-time semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating analysis. We also provide some formal results on the effects of such assertions on the analysis results.

关键词： program analysis Multivariance Context sensitivity Abstract interpretation Assertions Static analysis User guidance

来源：评论

学校读者我要写书评

暂无评论

Correctness of Context-Moving transformations for Term Rewriting Systems 25th

Correctness of Context-Moving Transformations for Term Rewri...

引用

25th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Sato, Koichi Kikuchi, Kentaro Aoto, Takahito Toyama, Yoshihito Tohoku Univ RIEC Aoba Ku 2-1-1 Katahira Sendai Miyagi 9808577 Japan

ISBN: (纸本)9783319274362;9783319274355

Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. the conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.

关键词： Tail-recursion program transformation Term rewriting system Inductive theorem proving

来源：评论

学校读者我要写书评

暂无评论

Analysis of Air Traffic Track Data with the AutoBayes synthesis System

引用

20th international symposium on logic-based program synthesis and transformation, LOPSTR 2010

作者： Schumann, Johann Cate, Karen Lee, Alan SGT Inc NASA Ames Moffett Field CA 94035 USA NASA Ames Res Ctr Moffett Field CA 94035 USA

ISBN: (纸本)9783642205507

the Next Generation Air Traffic System (NGATS) is aiming to provide substantial computer support for the air traffic controller. Algorithms for the accurate prediction of aircraft movements are of central importance for such software systems but trajectory prediction has to work reliably in the presence of unknown parameters and uncertainties. We are using the AutoBayes program synthesis system to generate customized data analysis algorithms that process large sets of aircraft radar track data in order to estimate parameters and uncertainties. In this paper, we present, how the tasks of finding structure in track data, estimation of important parameters in climb trajectories, and detection of continuous descent approaches (CDA) can be supported by code generated from compact AUTOBAYES specifications. We present an overview of the AutoBayes architecture and describe, how its schema-based approach generates customized analysis algorithms, documented C/C++ code, and detailed mathematical derivations. Results of experiments with actual air traffic control data are discussed.

关键词： Air traffic control

来源：评论

学校读者我要写书评

暂无评论

Annotation algorithms for unrestricted independent and-parallelism in logic programs

引用

17th international symposium on logic-based program synthesis and transformation

作者： Casas, Amadeo Carro, Manuel Hermenegildo, Manuel V. Univ New Mexico Dept Comp Sci & Elect Albuquerque NM 87131 USA Univ Politecn Madrid Sch Comp Sci Madrid Spain

ISBN: (纸本)9783540787686

We present two new algorithms which perform automatic parallelization via source-to-source transformations. the objective is to exploit goal-level, unrestricted independent and-parallelism. the proposed algorithms use as targets new parallel execution primitives which are simpler and more flexible than the well-known &/2 parallel operator. this makes it possible to generate better parallel expressions by exposing more potential parallelism among the literals of a clause than is possible with &/2. the difference between the two algorithms stems from whether the order of the solutions obtained is preserved or not. We also report on a preliminary evaluation of an implementation of our approach. We compare the performance obtained to that of previous annotation algorithms and show that relevant improvements can be obtained.

关键词： logic programming automatic parallelization and-parallelism program transformation

来源：评论

学校读者我要写书评

暂无评论

Intuitionistic logic programming for SQL 26th

Intuitionistic Logic Programming for SQL

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Saenz-Perez, Fernando Univ Complutense Madrid Declarat Programming Grp Dept Ingn Software & Inteligencia Artificial Madrid Spain

ISBN: (纸本)9783319631394;9783319631387

Intuitionistic logic programming provides the notion of embedded implication in rule bodies, which can be used to reason about a current database modified by the antecedent. this can be applied to a system that translates SQL to Datalog to solve SQL WIth queries, for which relations are locally defined and can therefore be understood as locally added to the current database. In addition, assumptions in SQL queries as either adding or removing data can be modelled in this way as well, which is an interesting feature for decision-support scenarios. this work suggests a way to apply intuitionistic logic programming to SQL, and provides a pointer to a working system implementing this idea.

关键词： Intuitionistic logic programming SQL Datalog Extended relational algebra

来源：评论

学校读者我要写书评

暂无评论

Determinacy analysis for logic programs using mode and type information

引用

14th international symposium on logic based program synthesis and transformation

作者： López-García, P Bueno, F Hermenegildo, M Tech Univ Madrid UPM Sch Comp Sci Madrid Spain Univ New Mexico Dept Comp Sci Albuquerque NM 87131 USA Univ New Mexico Dept Elect & Comp Engn Albuquerque NM 87131 USA

ISBN: (纸本)3540266550

We propose an analysis for detecting procedures and goals that are deterministic (i.e. that produce at most one solution), or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic (because they call other predicates that can produce more than one solution). Applications of such determinacy information include detecting programming errors, performing certain high-level program transformations for improving search efficiency, optimizing low level code generation and parallel execution, and estimating tighter upper bounds on the computational costs of goals and data sizes, which can be used for program debugging, resource consumption and granularity control, etc. We have implemented the analysis and integrated it in the CiaoPP system, which also infers automatically the mode and type information that our analysis takes as input. Experiments performed on this implementation show that the analysis is fairly accurate and efficient.

关键词： determinacy inference program analysis modes types

来源：评论

学校读者我要写书评

暂无评论

Proof Checking and logic programming 25th

Proof Checking and Logic Programming

引用

25th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Miller, Dale Ecole Polytech Inria Palaiseau France Ecole Polytech LIX Palaiseau France

ISBN: (纸本)9783319274362;9783319274355

In a world where trusting software systems is increasingly important, formal methods and formal proof can help provide trustable foundations. Proof checking can help to reduce the size of the trusted base since we do not need to trust an entire theorem prover if we can check the proofs they produce by a trusted (and smaller) checker. Many approaches to building proof checkers require embedding within them a full programming language. In most many modern proof checkers and theorem provers, that programming language is a functional programming language, often a variant of ML. In fact, parts of ML (e.g., strong typing, abstract datatypes, and higher-order programming) were designed to make ML into a trustworthy "meta-language" for checking proofs. While there is considerable overlap in the foundations of logic programming and proof checking (both benefit from unification, backtracking search, efficient term structures, etc.), the discipline of logic programming has, in fact, played a minor role in the history of proof checking. I will argue that logic programming can have a major role in the future of this important topic.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：