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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

58 篇 期刊文献
29 篇 会议
16 册 图书

馆藏范围

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

日期分布

学科分类号

72 篇 工学
- 54 篇 计算机科学与技术...
- 37 篇 软件工程
- 7 篇 电气工程
- 2 篇 材料科学与工程（可...
- 2 篇 交通运输工程
- 1 篇 信息与通信工程
- 1 篇 控制科学与工程
- 1 篇 生物医学工程（可授...
15 篇 理学
- 13 篇 数学
- 2 篇 生物学
8 篇 医学
- 2 篇 基础医学(可授医学...
- 2 篇 临床医学
- 1 篇 公共卫生与预防医...
- 1 篇 中西医结合
- 1 篇 护理学（可授医学、...
7 篇 管理学
- 7 篇 公共管理
3 篇 法学
- 3 篇 社会学
3 篇 教育学
- 2 篇 心理学(可授教育学...
- 1 篇 教育学

主题

103 篇 program logic
14 篇 program
11 篇 system
11 篇 verification
10 篇 ibm
10 篇 separation logic
10 篇 data
10 篇 concurrency
9 篇 logic
9 篇 logic manual
8 篇 program verifica...
8 篇 operating system
7 篇 disk operating
7 篇 manual
7 篇 bibliography
6 篇 manual program
6 篇 operating
5 篇 system manual
5 篇 safety
5 篇 publication

机构

4 篇 carnegie mellon ...
3 篇 aarhus univ dept...
2 篇 univ sci & techn...
2 篇 univ sci & techn...
2 篇 kyoto univ grad ...
2 篇 department of co...
2 篇 school of comput...
2 篇 max planck inst ...
2 篇 yale univ new ha...
2 篇 state key labora...
2 篇 aarhus univ aarh...
2 篇 swiss fed inst t...
2 篇 univ turin dipar...
2 篇 univ london impe...
1 篇 aarhus univ abog...
1 篇 univ politecn ma...
1 篇 alan turing inst...
1 篇 sokendai hayama ...
1 篇 univ calif river...
1 篇 katholieke univ ...

作者

6 篇 birkedal lars
5 篇 vafeiadis viktor
5 篇 hasuo ichiro
4 篇 suenaga kohei
3 篇 eberhart clovis
3 篇 liang hongjin
3 篇 shao zhong
3 篇 feng xinyu
3 篇 dreyer derek
3 篇 georges aina lin...
3 篇 sato tetsuya
3 篇 berger martin
2 篇 vale arthur oliv...
2 篇 qin shengchao
2 篇 pym david
2 篇 he mengda
2 篇 metcalfe sylvia ...
2 篇 fernandez ls
2 篇 docherty simon
2 篇 yamada akihisa

语言

98 篇 英文
5 篇 其他

检索条件"主题词=Program Logic"

共 103 条记录，以下是71-80 订阅

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

详细简洁

排序：

PCFIRE: Towards Provable Preventative Control-Flow Integrity Enforcement for Realistic Embedded Software 13

PCFIRE: Towards Provable Preventative Control-Flow Integrity...

引用

16th International Conference on Embedded Software (EMSOFT)

作者： Tan, Jiaqi Tay, Hui Jun Drolia, Utsav Gandhi, Rajeev Narasimhan, Priya Carnegie Mellon Univ Dept ECE Pittsburgh PA 15213 USA

ISBN: (纸本)9781450344852

Control-Flow Integrity (CFI) is an important safety property of software, particularly in embedded and safety-critical systems, where CFI violations have led to patient deaths and can render cars remotely controllable by attackers. Previous techniques for CFI may reduce the robustness of embedded and safety-critical systems, as they handle CFI violations by stopping programs. In this work, we present PCFIRE, a preventative approach to CFI that prevents the root-causes of CFI violations to allow recovery, and enables programmers to specify robust recovery actions by providing CFI via source-code safety-checks. PCFIRE's CFI can be formally proved automatically, and supports realistic features of embedded software such as hardware and I/O access. We showcase PCFIRE by providing, and automatically proving, CFI for: benchmark programs, text utilities containing I/O, and embedded programs with sensor inputs and hardware outputs on the Raspberry Pi single-board computer.

关键词： Control-Flow Integrity program logic Proof Assistant Interactive Theorem Proving ARM Executables HOL

来源：评论

学校读者我要写书评

暂无评论

GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation 14

GPS: Navigating Weak Memory with Ghosts, Protocols, and Sepa...

引用

2014 ACM International Conference on Object-Oriented-programming-Systems-Languages-and-Applications (OOPSLA 14)

作者： Turon, Aaron Vafeiadis, Viktor Dreyer, Derek Max Planck Inst Software Syst MPI SWS Kaiserslautern Germany

ISBN: (纸本)9781450325851

Weak memory models formalize the inconsistent behaviors that one can expect to observe in multithreaded programs running on modern hardware. In so doing, however, they complicate the already-difficult task of reasoning about correctness of concurrent code. Worse, they render impotent the sophisticated formal methods that have been developed to tame concurrency, which almost universally assume a strong (i.e., sequentially consistent) memory model. This paper introduces GPS, the first program logic to provide a full-fledged suite of modern verification techniques including ghost state, protocols, and separation logic for high-level, structured reasoning about weak memory. We demonstrate the effectiveness of GPS by applying it to challenging examples drawn from the Linux kernel as well as lock-free data structures. We also define the semantics of GPS and prove in Coq that it is sound with respect to the axiomatic C11 weak memory model.

关键词： Concurrency Weak memory models C/C plus program logic Separation logic

来源：评论

学校读者我要写书评

暂无评论

logical equivalence for subtyping object and recursive types

Logical equivalence for subtyping object and recursive types

引用

9th Italian Conference on Theoretical Computer Science (ICTCS 2005)

作者： van Bakel, Steffen de'Liguoro, Ugo Univ Turin Dipartimento Informat I-10149 Turin Italy Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2BZ England

Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order zeta-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.

关键词： object calculi type theory program logic

来源：评论

学校读者我要写书评

暂无评论

Abstraction for Conflict-Free Replicated Data Types 2021

Abstraction for Conflict-Free Replicated Data Types

引用

42nd ACM SIGPLAN International Conference on programming Language Design and Implementation (PLDI)

作者： Liang, Hongjin Feng, Xinyu Nanjing Univ State Key Lab Novel Software Technol Nanjing Jiangsu Peoples R China

ISBN: (纸本)9781450383912

Strong eventual consistency (SEC) has been used as a classic notion of correctness for Conflict-Free Replicated Data Types (CRDTs). However, it does not give proper abstractions of functionality, thus is not helpful for modular verification of client programs using CRDTs. We propose a new correctness formulation for CRDTs, called Abstract Converging Consistency (ACC), to specify both data consistency and functional correctness. ACC gives abstract atomic specifications (as an abstraction) to CRDT operations, and establishes consistency between the concrete execution traces and the execution using the abstract atomic operations. The abstraction allows us to verify the CRDT implementation and its client programs separately, resulting in more modular and elegant proofs than monolithic approaches for whole program verification. We give a generic proof method to verify ACC of CRDT implementations, and a rely-guarantee style program logic to verify client programs. Our Abstraction theorem shows that ACC is equivalent to contextual refinement, linking the verification of CRDT implementations and clients together to derive functional correctness of whole programs.

关键词： Replicated Data Types Eventual Consistency Contextual Refinement program logic Modular Verification

来源：评论

学校读者我要写书评

暂无评论

Formal Reasoning about the C11 Weak Memory Model 15

Formal Reasoning about the C11 Weak Memory Model

引用

ACM SIGPLAN Conference on Certified programs and Proofs (CPP)

作者： Vafeiadis, Viktor Max Planck Inst Software Syst MPI SWS Saarbrucken Germany

This abstract introduces the C11 weak memory model, summarises known verification results, and discusses some open problems.

ISBN: (纸本)9781450332965

This abstract introduces the C11 weak memory model, summarises known verification results, and discusses some open problems.

关键词： Concurrency Weak Memory Models program logic

来源：评论

学校读者我要写书评

暂无评论

Formal Reasoning about Concurrent Assembly Code with Reentrant Locks

Formal Reasoning about Concurrent Assembly Code with Reentra...

引用

3rd International Symposium on Theoretical Aspects of Software Engineering

作者： Fu, Ming Zhang, Yu Li, Yong Univ Sci & Technol China Dept Comp Sci & Technol Hefei 230027 Peoples R China

ISBN: (纸本)9780769537573

This paper focuses on the problem of reasoning about concurrent assembly code with reentrant locks. Our verification technique is based on concurrent separation logic (CSL). In CSL, locks are treated as non-reentrant locks and each lock is associated with a resource invariant, the lock-protected resources are obtained and released through acquiring and releasing the lock respectively. In order to accommodate for reentrancy, we introduce some additional notions into our specification language to describe reentrant level for each acquiring and releasing lock operation. Keeping track of the reentrant level for each lock in the pre- and post-conditions enables the program logic to ensure that resources are not re-acquired upon reentrancy, thus resources owned by a thread are prevented from reintroducing in the postcondition. Our framework is full), mechanized. Its soundness has been verified using the Coq proof assistant. We demonstrate the usage of our framework through giving a safety proof of a simple program.

关键词： reentrant locks concurrent separation logic safety program logic

来源：评论

学校读者我要写书评

暂无评论

Automated Software Verification of Hyperliveness 30th

Automated Software Verification of Hyperliveness

引用

30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Held as Part of the 27th European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Beutner, Raven CISPA Helmholtz Ctr Informat Secur Saarbrucken Germany

ISBN: (纸本)9783031572487;9783031572494

Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of k-safety properties, i.e., properties that state that all k-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider for all(k)there exists(l) properties, which state that for all k executions, there exist l executions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of for all(k)there exists(l) properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.

关键词： Hyperproperties program logic Hoare logic Symbolic Execution Constraint-based Verification Predicate Transformer Refinement Strongest Postcondition Underapproximation.

来源：评论

学校读者我要写书评

暂无评论

Relational proofs for quantum programs

Relational proofs for quantum programs

引用

Proceedings of the ACM on programming Languages

作者： Barthe, Gilles Hsu, Justin Ying, Mingsheng Yu, Nengkun Zhou, Li Max Planck Institute for Security and Privacy Germany IMDEA Software Institute Spain Department of Computer Sciences University of Wisconsins Madison United States Centre for Quantum Software and Information University of Technology Sydney Australia State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Tsinghua University China Department of Computer Science and Technology Tsinghua University China

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks. © 2020 Copyright held by the owner/author(s).