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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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 条记录，以下是131-140 订阅

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

详细简洁

排序：

Context Generation from Formal Specifications for C Analysis Tools 27th

Context Generation from Formal Specifications for C Analysis...

引用

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

作者： Alberti, Michele Signoles, Julien TrustInSoft Paris France CEA LIST Software Reliabil & Secur Lab F-91191 Gif Sur Yvette France

ISBN: (纸本)9783319944609;9783319944593

Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. this may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible. this paper presents a way to systematically generate such a context from a formal specification of a C function. this is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. the idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting.

关键词： Formal specification Code generation transformation Code analysis Frama-C ACSL

来源：评论

学校读者我要写书评

暂无评论

Functional and Constraint logic programming 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： Herbert Kuchen

ISBN: (数字)9783642225314

ISBN: (纸本)9783642225307

this book constitutes the refereed conference proceedings of the 20th international Workshop on Functional and Constraint logic programming, WFLP 2011, held in Odense, Denmark, in July 2011 as Part of the 13th international symposium on Principles and Practice of Declarative programming (PPDP 2011), the 22st international symposium on logic-based program synthesis and transformation (LOPSTR 2011), and the 4th international Workshop on Approaches and Applications of Inductive programming (AAIP 2011). From the 10 papers submitted, 9 were accepted for presentation the proceeding. the papers cover current research in all areas of functional and logic programming as well as the integration of constraint logic and object-oriented programming, and term rewriting.

关键词： logics and Meanings of programs Mathematical logic and Formal Languages programming Languages, Compilers, Interpreters Artificial Intelligence Symbolic and Algebraic Manipulation Computer Imaging, Vision, Pattern Recognition and Graphics

来源：评论

学校读者我要写书评

暂无评论

logic-based program synthesis and transformation 2009

引用

丛书名： Lecture Notes in Computer Science

2009年

作者： Michael Hanus

来源：评论

学校读者我要写书评

暂无评论

Static Analysis 1

引用

丛书名： Lecture Notes in Computer Science

1000年

ISBN: (数字)9783540691662

ISBN: (纸本)9783540691631

this book constitutes the refereed proceedings of the 15th international symposium on Static Analysis, SAS 2008, held in Valencia, Spain in July 2008 - co-located with LOPSTR 2008, the international symposium on logic-based program synthesis and transformation, PPDP 2008, the international ACM SIGPLAN symposium on Principles and Practice of Declarative programming, and PLID 2008, the international Workshop on programming Language Interference and Dependence. the 22 revised full papers presented together with two invited lectures were carefully reviewed and selected from 63 submissions. the papers address all aspects of static analysis including abstract domains, abstract interpretation, abstract testing, compiler optimizations, control flow analysis, data flow analysis, model checking, program specialization, security analysis, theoretical analysis frameworks, type based analysis, and verification systems.

关键词： Software Engineering/programming and Operating Systems programming Languages, Compilers, Interpreters logics and Meanings of programs Software Engineering Mathematical logic and Formal Languages programming Techniques

来源：评论

学校读者我要写书评

暂无评论

logic based program synthesis and transformation 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： Maurice Bruynooghe

ISBN: (数字)9783540259381

ISBN: (纸本)9783540221746

this volume contains selected papers from LOPSTR 2003, the 13th Inter- tional symposium on logic-based program synthesis and transformation. the LOPSTR series is devoted to research in logic-based program development. P- ticular topics of interest are speci?cation, synthesis, veri?cation, transformation, specialization, analysis, optimization, composition, reuse, component-based so- ware development, agent-based software development, software architectures, design patterns and frameworks, program re?nement and logics for re?nement, proofs as programs, and applications and tools. LOPSTR 2003 took place at the University of Uppsala from August 25 to August 27 as part of PLI 2003 (Principles, logics, and Implementations of High- Level programming Languages). PLI was an ACM-organized confederation of conferences and workshops with ICFP 2003 (ACM-SIGPLAN international C- ference on Functional programming) and PPDP 2003 (ACM-SIGPLAN Inter- tional Conference on Principles and Practice of Declarative programming) as the main events. the LOPSTR community pro?ted from the shared lectures of the invited speakers, and the active scienti?c discussions enabled by the co-location. LOPSTR 2003 was the thirteenth in a series of events. Past events were held in Manchester, UK (1991, 1992, 1998), Louvain-la-Neuve, Belgium (1993), Pisa, Italy (1994), Arnhem, the Netherlands (1995), Stockholm, Sweden (1996), L- ven, Belgium (1997), Venice, Italy (1999), London, UK (2000), Paphos, Cyprus (2001), and Madrid, Spain (2002).

关键词： Software Engineering/programming and Operating Systems logics and Meanings of programs programming Techniques Mathematical logic and Formal Languages Artificial Intelligence

来源：评论

学校读者我要写书评

暂无评论

Slicing Concurrent Constraint programs 26th

Slicing Concurrent Constraint Programs

引用

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

作者： Falaschi, Moreno Gabbrielli, Maurizio Olarte, Carlos Palamidessi, Catuscia Univ Siena Dipartimento Ingn Informaz & Sci Matemat Siena Italy Univ Bologna Dipartimento Informat Sci & Ingn Bologna Italy Univ Fed Rio Grande do Norte ECT Natal RN Brazil Ecole Polytech INRIA Palaiseau France Ecole Polytech LIX Palaiseau France

ISBN: (纸本)9783319631394;9783319631387

Concurrent Constraint programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to timed variants of CCP. We also develop a prototypical implementation freely available for making experiments.

关键词： Concurrent Constraint programming program slicing Debugging

来源：评论

学校读者我要写书评

暂无评论

Incremental Analysis of logic programs with Assertions and Open Predicates 29th

Incremental Analysis of Logic Programs with Assertions and O...

引用

29th international Conference 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: (纸本)9783030452599;9783030452605

Generic components are a further abstraction over the concept of modules, introducing dependencies on other (not necessarily available) components implementing specified interfaces. they have become a key concept in large and complex software applications. Despite undeniable advantages, generic code is also anti-modular. Precise analysis (e.g., for detecting bugs or optimizing code) requires such code to be instantiated with concrete implementations, potentially leading to expensive combinatorial explosion. In this paper we claim that incremental, whole program analysis can be very beneficial in this context, and alleviate the anti-modularity nature of generic code. We propose a simple Horn-clause encoding of generic programs, using open predicates and assertions, and we introduce a new incremental, multivariant analysis algorithm that reacts incrementally not only to changes in program clauses, but also to changes in the assertions, upon which large parts of the analysis graph may depend. We also discuss the application of the proposed techniques in a number of practical use cases. In addition, as a realistic case study, we apply the proposed techniques in the analysis of the LPdoc documentation system. We argue that the proposed traits are a convenient and elegant abstraction for modular generic programming, and that our preliminary results support our thesis that the new incrementality-related features added to the analysis bring promising advantages in this context.

关键词： Incremental static analysis Verification Assertions Generic code Specifications Abstract interpretation Horn clauses logic programs

来源：评论

学校读者我要写书评

暂无评论

the next 700 synthesis calculi 11

The next 700 synthesis calculi

引用

11th international symposium of Formal Methods Europe, FME 2002

作者： Basin, David Universität Freiburg Freiburg Germany

ISBN: (纸本)9783540439288

Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for program synthesis and transformation. these projects had different motivations and goals and differed too in the kinds of programs synthesized (e.g., functional programs, logic programs, and even circuit descriptions). However, despite their differences they were all based on three simple ideas. First, calculi can be formally derived in a rich enough logic (e.g., higher-order logic). Second, higher-order resolution is the central mechanism used to synthesize programs during proofs of their correctness. And third, synthesis proofs have a predictable form and can be partially or completely automated. In the talk I explain these ideas and illustrate the general methodology employed. © Springer-Verlag Berlin Heidelberg 2002.

关键词： Biomineralization

来源：评论

学校读者我要写书评

暂无评论

Latte: Locality Aware transformation for High-Level synthesis 26

Latte: Locality Aware Transformation for High-Level Synthesi...

引用

26th IEEE Annual international symposium on Field-programmable Custom Computing Machines (FCCM)

作者： Cong, Jason Wei, Peng Yu, Cody Hao Zhou, Peipei Univ Calif Los Angeles Comp Sci Los Angeles CA 90095 USA

ISBN: (纸本)9781538655221

In this paper we classify the timing degradation problems using four common collective communication and computation patterns in HLS-based accelerator design: scatter, gather, broadcast and reduce. these widely used patterns scale poorly in one-to-all or all-to-one data movements between off-chip communication interface and on-chip storage, or inside the computation logic. therefore, we propose the Latte microarchitecture featuring pipelined transfer controllers (PTC) along data paths in these patterns. Furthermore, we implement an automated framework to apply our Latte implementation in HLS with minimal user efforts. Our experiments show that Latte-optimized designs greatly improve the timing of baseline HLS designs by 1.50x with only 3.2% LUT overhead on average, and 2.66x with 2.7% overhead at maximum.

关键词： Microarchitecture Delays Wires System-on-chip Pipelines Layout Tools"

来源：评论

学校读者我要写书评

暂无评论

Inferring Energy Bounds via Static program Analysis and Evolutionary Modeling of Basic Blocks 27th

Inferring Energy Bounds via Static Program Analysis and Evol...

引用

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

作者： Liqat, Umer Bankovic, Zorana Lopez-Garcia, Pedro Hermenegildo, Manuel, V IMDEA Software Inst Madrid Spain Spanish Council Sci Res CSIC Madrid Spain Univ Politecn Madrid Madrid Spain

ISBN: (纸本)9783319944609;9783319944593

the ever increasing number and complexity of energy-bound devices (such as the ones used in Internet of things applications, smart phones, and mission critical systems) pose an important challenge on techniques to optimize their energy consumption and to verify that they will perform their function within the available energy budget. In this work we address this challenge from the software point of view and propose a novel approach to estimating accurate parametric bounds on the energy consumed by program executions that are practical for their application to energy verification and optimization. Our approach divides a program into basic (branchless) blocks and performs a best effort modeling to estimate upper and lower bounds on the energy consumption for each block using an evolutionary algorithm. then it combines the obtained values according to the program control flow, using a safe static analysis, to infer functions that give both upper and lower bounds on the energy consumption of the whole program and its procedures as functions on input data sizes. We have tested our approach on (C-like) embedded programs running on the XMOS hardware platform. However, our method is general enough to be applied to other microprocessor architectures and programming languages. the bounds obtained by our prototype implementation on a set of benchmarks were always safe and quite accurate. this supports our hypothesis that our approach offers a good compromise between safety and accuracy, and can be applied in practice for energy verification and optimization.

关键词： Energy modeling Evolutionary algorithms Static analysis Energy consumption analysis and verification Resource analysis and verification

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：