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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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

分类表

所选分类

>> <<

限定检索结果

文献类型

143 篇 会议
15 册 图书

馆藏范围

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

日期分布

学科分类号

125 篇 工学
- 124 篇 计算机科学与技术...
- 69 篇 软件工程
- 6 篇 电气工程
- 5 篇 信息与通信工程
- 3 篇 控制科学与工程
- 1 篇 机械工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 生物医学工程（可授...
- 1 篇 网络空间安全
38 篇 理学
- 37 篇 数学
- 1 篇 生物学
4 篇 管理学
- 3 篇 图书情报与档案管...
- 1 篇 管理科学与工程(可...
- 1 篇 工商管理
1 篇 医学
- 1 篇 基础医学(可授医学...
- 1 篇 临床医学
- 1 篇 药学(可授医学、理...

主题

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

机构

4 篇 univ politecn va...
3 篇 katholieke univ ...
3 篇 nagoya inst tech...
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 篇 univ complutense...
2 篇 univ north texas...
2 篇 tech u madrid sc...
2 篇 imdea software i...
2 篇 univ new mexico ...
2 篇 univ new mexico ...
2 篇 ecole polytech l...
2 篇 univ ulm d-89069...
2 篇 ecole polytech i...
2 篇 german univ cair...
2 篇 nagoya institute...

作者

6 篇 vidal german
4 篇 proietti maurizi...
4 篇 schneider-kamp p...
4 篇 silva josep
4 篇 falaschi moreno
4 篇 seki hirohisa
4 篇 abdennadher slim
4 篇 giesl juergen
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
2 篇 gallagher john p...
2 篇 komendantskaya e...
2 篇 sharaf nada
2 篇 hermenegildo man...

语言

155 篇 英文
3 篇 中文

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

共 158 条记录，以下是11-20 订阅

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

详细简洁

排序：

OVERLAY 2021 - Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, logic, Automata, and synthesis, hosted by the 12th international symposium on Games, Automata, logics,and Formal Verification, GandALF 2021

OVERLAY 2021 - Proceedings of the 3rd Workshop on Artificial...

引用

3rd Workshop on Artificial Intelligence and Formal Verification, logic, Automata, and synthesis, OVERLAY 2021

the proceedings contain 19 papers. the topics discussed include: planning with global state constraints for urban traffic control;BLACK: a fast, flexible and reliable LTL satisfiability checker;automated planning through program verification;rule-based shield synthesis for partially observable Monte Carlo planning;dynamic attack trees;mining temporal networks: results and open problems;multi-frame modal symbolic learning;automated reasoning for reinforcement learning agents in structured environments;using directional arc consistency with asynchronous forward-bounding algorithm;and statistical model checking for the analysis of mission- and safety-critical cyber-physical system.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Design and Evaluation of a Synthesizable Standard-Cell-based Nonvolatile FPGA 50

Design and Evaluation of a Synthesizable Standard-Cell-Based...

引用

IEEE 50th international symposium on Multiple-Valued logic (ISMVL)

作者： Suzuki, Daisuke Hanyu, Takahiro Tohoku Univ Frontier Res Inst Interdisciplinary Sci Sendai Miyagi Japan Tohoku Univ Res Inst Elect Commun Sendai Miyagi Japan

ISBN: (纸本)9781728154060

A nonvolatile FPGA, where the circuit-configuration information still remains without power supply, offers a powerful solution against the standby power issue. In this paper, a synthesizable nonvolatile FPGA is proposed, where the circuit-configuration information is described in a hardware description language and is pushed through a standard ASIC tool flow with nonvolatile logic circuit IPs such as nonvolatile flip-flops. the use of the ASIC tool flow makes it possible to migrate any arbitrary process technology and to perform architecture-level simulation with physical information. As a typical design example under 55nm CMOS/100nm magnetic tunnel junction (MTJ) technologies, the performance of the proposed nonvolatile FPGA is evaluated in comparison with that of a CMOS-only volatile FPGA.

关键词： FPGA Nonvolatile logic logic synthesis hardware description language standard-cell-based design

来源：评论

学校读者我要写书评

暂无评论

synthesis of Human-Inspired Intelligent Fonts Using Conditional-DCGAN

Synthesis of Human-Inspired Intelligent Fonts Using Conditi...

引用

international Conference on Computer Vision and Machine Intelligence, CVMI 2022

作者： Kalingeri, Ranjith Kushwaha, Vandana Kala, Rahul Nandi, G.C. Center of Intelligent Robotics Indian Institute of Information Technology Allahabad UP Prayagraj211015 India

ISBN: (纸本)9789811978661

Despite numerous fonts already being designed and easily available online, the desire for new fonts seems to be endless. Previous methods focused on extracting style, shape, and stroke information from a large set of fonts, or transforming and interpolating existing fonts to create new fonts. the drawback of these methods is that generated fonts look-alike fonts of training data. As fonts are created from human handwriting documents, they have uncertainty and randomness incorporated into them, giving them a more authentic feel than standard fonts. Handwriting, like a fingerprint, is unique to each individual. In this paper, we have proposed GAN-based models that automate the entire font generation process, removing the labor involved in manually creating a new font. We extracted data from single-author handwritten documents and developed and trained class-conditioned DCGAN models to generate fonts that mimic the author’s handwriting style. © 2023, the Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

关键词： BCFID cGAN DCGAN FID Intelligent fonts Random fonts WCFID

来源：评论

学校读者我要写书评

暂无评论

transformational verification of quicksort 8

Transformational verification of quicksort

引用

8th international Workshop on Verification and program transformation, VPT 2020 and 7th Workshop on Horn Clauses for Verification and synthesis, HCVS 2020

作者： de Angelis, Emanuele Fioravanti, Fabio Proietti, Maurizio CNR IASI Via dei Taurini 19 Roma00185 Italy DEC University "G. d'Annunzio" of Chieti-Pescara Viale Pindaro 42 Pescara65127 Italy

Many transformation techniques developed for constraint logic programs, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work out a nontrivial case study through the transformation-based verification approach. We consider the familiar Quicksort program for sorting lists, written in a functional programming language, and we verify the pre/postconditions that specify the intended correctness properties of the functions defined in the program. We verify these properties by: (1) translating them into CHCs, (2) transforming the CHCs by removing all list occurrences, and (3) checking the satisfiability of the transformed CHCs by using the Eldarica solver over booleans and integers. the transformation mentioned at Point (2) requires an extension of the algorithms for the elimination of inductively defined data structures presented in previous work, because during one stage of the transformation we use as lemmas some properties that have been proved at previous stages. © E. De Angelis, F. Fioravanti & M. Proietti this work is licensed under the Creative Commons Attribution License.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Predicate Specialization for Definitional Higher-Order logic programs 28th

Predicate Specialization for Definitional Higher-Order Logic...

引用

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

作者： Troumpoukis, Antonis Charalambidis, Angelos Univ Athens Dept Informat & Telecommun Athens Greece NCSR Demokritos Inst Informat & Telecommun Athens Greece

ISBN: (纸本)9783030138387;9783030138370

Higher-order logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higher-order logic programs and can transform them into first-order programs without introducing additional data structures. the resulting first-order programs can be executed by conventional logic programming interpreters and benefit from other optimizations that might be available. We provide an implementation and experimental results that suggest the efficiency of the transformation.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

A Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear logic Inference 28th

A Pragmatic, Scalable Approach to Correct-by-Construction Pr...

引用

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

作者： Papapanagiotou, Petros Fleuriot, Jacques Univ Edinburgh Sch Informat 10 Crichton St Edinburgh EH8 9AB Midlothian Scotland

ISBN: (纸本)9783030138387;9783030138370

the need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear logic (CLL) for correct-by-construction resource-based process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting.

关键词： Process modelling Composition Correct by construction Workflow Linear logic

来源：评论

学校读者我要写书评

暂无评论

Eliminating Unstable Tests in Floating-Point programs 28th

Eliminating Unstable Tests in Floating-Point Programs

引用

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

作者： Titolo, Laura Munoz, Cesar A. Feliu, Marco A. Moscato, Mariano M. Natl Inst Aerosp Hampton VA 23666 USA NASA Langley Res Ctr Hampton VA 23665 USA

ISBN: (纸本)9783030138387;9783030138370

Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. this problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. the output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. the proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.

关键词： Floating-point numbers Round-off error program transformation Test instability Formal verification

来源：评论

学校读者我要写书评

暂无评论

Proving program Properties as First-Order Satisfiability 28th

Proving Program Properties as First-Order Satisfiability

引用

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

作者： Lucas, Salvador Univ Politecn Valencia DSIC Valencia Spain

ISBN: (纸本)9783030138387;9783030138370

program semantics can often be expressed as a (many-sorted) first-order theory S, and program properties as sentences phi which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties phi expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of S and the negation (sic)phi of phi. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theories. In this paper we extend our previous results to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property. by just finding a model of an appropriate theory (including S and possibly something else) and an appropriate first-order formula related to.. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.

关键词： First-order logic logical models program analysis

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

An Assertion Language for Slicing Constraint logic Languages 28th

An Assertion Language for Slicing Constraint Logic Languages

引用

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

作者： Falaschi, Moreno Olarte, Carlos Univ Siena Dept Informat Engn & Math Siena Italy Univ Fed Rio Grande do Norte ECT Natal RN Brazil

ISBN: (纸本)9783030138387;9783030138370

Constraint logic programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we developed a framework for dynamic slicing of CCP where the user first identifies that a (partial) computation is wrong. then, she marks (selects) some parts of the final state corresponding to the data (constraints) and processes that she wants to study more deeply. An automatic process of slicing begins, and the partial computation is "depurated" by removing irrelevant information. In this paper we give two major contributions. First, we extend the framework to CLP, thus generalizing the previous work. Second, we provide an assertion language suitable for both, CCP and CLP, which allows the user to specify some properties of the computations in her program. If a state in a computation does not satisfy an assertion then some "wrong" information is identified and an automatic slicing process can start. We thus make one step further towards automatizing the slicing process. We show that our framework can be integrated with the previous semi-automatic one, giving the user more choices and flexibility. We show by means of examples and experiments the usefulness of our approach.

关键词： Concurrent Constraint programming Constraint logic programming Dynamic slicing Debugging Assertion language

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共16页 << < 1 2 3 4 5 6 7 8 9 10 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：