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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

301 篇 会议
8 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

150 篇 工学
- 130 篇 计算机科学与技术...
- 118 篇 软件工程
- 22 篇 电气工程
- 16 篇 机械工程
- 13 篇 建筑学
- 12 篇 控制科学与工程
- 7 篇 信息与通信工程
- 6 篇 电子科学与技术（可...
- 1 篇 仪器科学与技术
- 1 篇 航空宇航科学与技...
- 1 篇 生物医学工程（可授...
- 1 篇 生物工程
- 1 篇 安全科学与工程
19 篇 理学
- 14 篇 数学
- 3 篇 系统科学
- 2 篇 生物学
- 1 篇 物理学
- 1 篇 化学
- 1 篇 统计学（可授理学、...
13 篇 艺术学
- 13 篇 设计学（可授艺术学...
11 篇 管理学
- 8 篇 管理科学与工程(可...
- 3 篇 工商管理
- 2 篇 图书情报与档案管...

主题

40 篇 analytical model...
38 篇 computational mo...
31 篇 formal methods
25 篇 hardware
22 篇 software
16 篇 model checking
16 篇 state-space meth...
15 篇 semantics
15 篇 data models
14 篇 computer archite...
14 篇 mathematical mod...
13 篇 safety
13 篇 automata
12 篇 software enginee...
12 篇 clocks
12 篇 verification
12 篇 formal verificat...
11 篇 algorithm design...
11 篇 adaptation model...
10 篇 computer science

机构

3 篇 sri internationa...
3 篇 cyber-physical s...
3 篇 univ twente form...
3 篇 univ calif berke...
2 篇 johannes kepler ...
2 篇 sri int menlo pk...
2 篇 computer enginee...
2 篇 dfki gmbh cyber ...
2 篇 iit delhi
2 篇 berlin institute...
2 篇 agh university o...
2 篇 university of ca...
2 篇 johannes kepler ...
2 篇 department of el...
2 篇 univ twente ensc...
2 篇 department of co...
2 篇 eindhoven univ t...
2 篇 univ oxford dept...
2 篇 mit comp sci & a...
2 篇 software modelin...

作者

4 篇 schneider klaus
4 篇 zaytsev vadim
4 篇 teich juergen
3 篇 talpin jean-pier...
3 篇 nils przigoda
3 篇 robert wille
3 篇 rolf drechsler
3 篇 gupta rajesh
2 篇 ruchkin ivan
2 篇 t. basten
2 篇 umeno shinya
2 篇 lim hongping
2 篇 axel legay
2 篇 chao wang
2 篇 o. sarbishei
2 篇 hoe james c.
2 篇 nathan allen
2 篇 sanjiva prasad
2 篇 allison sullivan
2 篇 mitra sayan

语言

309 篇 英文

检索条件"任意字段=IEEE/ACM International Conference on Formal Methods and Models for Codesign"

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

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

详细简洁

排序：

Proof Automation with Large Language models 24

Proof Automation with Large Language Models

引用

39th acm/ieee international conference on Automated Software Engineering (ASE)

作者： Lu, Minghai Delaware, Benjamin Zhang, Tianyi Purdue Univ W Lafayette IN 47907 USA

ISBN: (数字)9798400712487

ISBN: (纸本)9798400712487

Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language models (LLMs) have shown promise in automatically generating informal proofs in natural language, they are less effective at generating formal proofs in interactive theorem provers. In this paper, we conduct a formative study to identify common mistakes made by LLMs when asked to generate formal proofs. By analyzing 520 proof generation errors made by GPT-3.5, we found that GPT-3.5 often identified the correct high-level structure of a proof, but struggled to get the lower-level details correct. Based on this insight, we propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. We evaluate PALM on a large dataset that includes more than 10K theorems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems. Moreover, PALM proves 1270 theorems beyond the reach of existing approaches. We also demonstrate the generalizability of PALM across different LLMs.

关键词： Backtracking Automation Large language models Natural languages Manuals Maintenance engineering Software Software engineering

来源：评论

学校读者我要写书评

暂无评论

Exploring the Fundamentals of Mutations in Deep Neural Networks 24

Exploring the Fundamentals of Mutations in Deep Neural Netwo...

引用

acm/ieee 27th international conference on Model Driven Engineering Languages and Systems: Companion Proceedings (models)

作者： Ahmed, Zaheed Makedonski, Philip Univ Goettingen Inst Comp Sci Lower Saxony Germany

ISBN: (纸本)9798400706226

The increasing popularity of deep neural networks (DNNs) has led to the adaptation of mutation analysis from classical software development to the machine learning (ML) paradigm. However, determining what to mutate and to what extent remains a challenge. To this aim, two questions are of importance: (i) which ML artifacts can be modified to generate acceptable mutations?, and (ii) what extent of change in a specific metric qualifies as a useful mutant? Addressing the first query, current research offers contradictory perspectives on suitable ML artifacts for mutations. In this paper, we argue that the ML development process resembles formal method-based development, drawing parallels between iterative refinement in ML and in formal specification-based development. This framing supports the injection of bugs into the training program, training data, and trained models. Regarding the second inquiry, existing ML mutant selection criteria focus on semantic aspects like prediction accuracy and error rates, neglecting the magnitude of syntactic changes. This oversight challenges the validity of foundational hypotheses for mutation analysis in ML, such as the competent programmer hypothesis and coupling effect. Our observations support addressing these fundamental tasks to enhance the realism of mutation analysis in ML contexts. We have outlined plans to tackle these identified challenges.

关键词： mutation analysis deep learning formal methods software testing

来源：评论

学校读者我要写书评

暂无评论

Logical square-driven and state-oriented generation of behavioural models 39

Logical square-driven and state-oriented generation of behav...

引用

39th acm/ieee international conference on Automated Software Engineering Workshops, ASEW 2024

作者： Klimek, Radoslaw AGH University of Krakow Krakow Poland

ISBN: (纸本)9798400712494

The accurate defining states in a newly designed state machine diagram can be a challenge, especially if we are not domain experts. There is an idea of the square of oppositionin classical logic, which is highly informative and can support analysts when shaping states for behavioural models. We proposed an identification method employing a square-driven and state-oriented approach, ideally suited for cases where analysts struggle with understanding the investigated domain or in applications that demand rigorous adherence to formal methodologies. State identification is augmented by the encoding of state variables representing particular states and predicates along with the analysis in a logical style. We have shown a simple yet inspiring example to illustrate the entire methodology in a satisfactory manner. © 2024 acm.

关键词： formal methods

来源：评论

学校读者我要写书评

暂无评论

Modelling of Cyber-Physical Systems through Domain-Specific Languages: Decision, Analysis, Design 24

Modelling of Cyber-Physical Systems through Domain-Specific ...

引用

acm/ieee 27th international conference on Model Driven Engineering Languages and Systems: Companion Proceedings (models)

作者： Gerhold, Marcus Kouzel, Aliaksei Mangal, Haroun Mehmed, Selin A. Zaytsev, Vadim Univ Twente Formal Methods & Tools Enschede Netherlands Univ Twente Tech Comp Sci Enschede Netherlands

ISBN: (纸本)9798400706226

Cyber-Physical Systems (CPS) integrate computational algorithms and physical components, requiring sophisticated modelling techniques to address complex interactions and dynamics. This paper explores the creation of Domain-Specific Languages (DSLs) tailored for CPS, focusing on the initial three critical phases: decision, analysis, design. We present four key aspects to address in the decision phase, design an ontology as a domain model for the analysis phase, and collect some advice for the design phase. By systematically addressing these phases, we provide a comprehensive framework for developing DSLs that can efficiently model CPS, facilitating improved design, verification, and deployment of these intricate systems.

关键词： Cyber-Physical Systems Ontological Analysis Domain-Specific Languages

来源：评论

学校读者我要写书评

暂无评论

Leveraging Large Language models to Boost Dafny's Developers Productivity 12

Leveraging Large Language Models to Boost Dafny's Developers...

引用

ieee/acm 12th international conference on formal methods in Software Engineering (formaliSE)

作者： Silva, Alvaro Mendes, Alexandra Ferreira, Joao F. Univ Porto INESC TEC HASLab Porto Portugal Univ Porto Fac Engn Porto Portugal Univ Lisbon INESC ID Lisbon Portugal Univ Lisbon IST Lisbon Portugal

ISBN: (纸本)9798400705892

This research idea paper proposes leveraging Large Language models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on using LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, we attempt to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.

关键词： Verification-Aware Languages Dafny Large Language models Generative AI Software Productivity Software Verification Lemma Inference Proof Inference Automated Program Repair

来源：评论

学校读者我要写书评

暂无评论

Design and formal Verification of a Copland-based Attestation Protocol 21

Design and Formal Verification of a Copland-based Attestatio...

引用

19th acm-ieee international conference on formal methods and models for System Design (MEMOCODE)

作者： Petz, Adam Jurgensen, Grant Alexander, Perry Univ Kansas Informat & Telecommun Technol Ctr Lawrence KS 66045 USA

ISBN: (纸本)9781450391276

We present the design and formal analysis of a remote attestation protocol and accompanying security architecture that generate evidence of trustworthy execution for legacy software. For formal guarantees of measurement ordering and cryptographic evidence strength, we leverage the Copland language and Copland Virtual Machine execution semantics. For isolation of attestation mechanisms we design a layered attestation architecture that leverages the seL4 microkernel. The formal properties of the protocol and architecture together serve to discharge assumptions made by an existing higher-level model-finding tool to characterize all ways an active adversary can corrupt a target and go undetected. As a proof of concept, we instantiate this analysis framework with a specific Copland protocol and security architecture to measure a legacy flight planning application. By leveraging components that are amenable to formal analysis, we demonstrate a principled way to design an attestation protocol and argue for its end-to-end correctness.

关键词： remote attestation formal methods verification

来源：评论

学校读者我要写书评

暂无评论

formal modelling of attack scenarios and mitigation strategies in ieee 1588 21

Formal modelling of attack scenarios and mitigation strategi...

引用

19th acm-ieee international conference on formal methods and models for System Design (MEMOCODE)

作者： Anto, Kelvin Roop, Partha S. Swain, Akshya K. Univ Auckland Auckland New Zealand

ISBN: (纸本)9781450391276

ieee 1588 is a time synchronization protocol that is extensively used by many Cyber-Physical Systems (CPSs). However, this protocol is prone to various types of attacks. We focus on a specific type of Man-in-the-Middle (MITM) attack, where the attacker introduces random delays to the messages being exchanged between a master and a slave. Such attacks have been modelled previously and some mitigation strategies have also been developed. However, the proposed methods work only under constant delay attacks and the developed mitigation strategies are ad-hoc. We propose the first formal framework for modelling and mitigating time delay attacks in JPRF 1588. Initially, the master, the slave and the communication medium are modelled as Timed Automata (TA) assuming the absence of any attacks. Subsequently, a generic attacker is modelled as a TA, which can formally represent various attacks including constant delay, linear delay and exponential delay. Finally, system identification methods of control theory is used to design proportional controllers for mitigating the effects of time delay attacks. We use model checking to ensure the resilience of protocol to time delay attacks using the proposed mitigation strategy.

关键词： ieee 1588 Clock Synchronization Time Delay Attacks Timed Automata System Identification

来源：评论

学校读者我要写书评

暂无评论

Challenges in Empirically Testing Memory Persistency models 46

Challenges in Empirically Testing Memory Persistency Models

引用

ieee/acm 46th international conference on Software Engineering - New Ideas and Emerging Results (ICSE-NIER)

作者： Klimis, Vasileios Donaldson, Alastair F. Vafeiadis, Viktor Wickerson, John Raad, Azalea Queen Mary Univ London London England Imperial Coll London London England MPI SWS Saarbrucken Germany

ISBN: (纸本)9798400705007

Memory persistency models provide the foundational rules for software engineers to develop applications that take advantage of non-volatile memory (NVM), dictating which (and when) writes to NVM are deemed persistent. Though formalised for Intel-x86 and Arm architectures, these models remain empirically unvalidated on actual machines. Conventional validation methods for memory consistency models fall short as test programs cannot differentiate between volatile cache reads and those from NVM. To address this, we employed a commercial device designed to intercept and log data on a system's memory bus in their order of arrival. We used this device to conduct a campaign using litmus tests-small programs designed to assess specific memory persistency behaviours-aimed at empirically validating Intel-x86 and Arm machine persistency guarantees. We noted out-of-order memory writes and ensured they were not merely artifacts of our test setup. Analysis revealed Intel-x86's architecture cannot be validated via memory bus interception due to legitimate early subsystem reordering. Intel engineers confirmed the absence of dependable validation methods for the persistency claims of their architectures. Meanwhile, an expert-recommended Arm machine did not align with the formal persistency model due to a specification loophole, and further investigation suggests that no market-available Arm machine fully supports NVM. Our finding for Intel highlights a major concern for software developers wishing to take advantage of NVM: currently there is, to our knowledge, no viable way to confirm the persistency guarantees claimed by Intel. Our results for Arm suggest that our interception-based approach is viable for reliably detecting reorderings in the memory subsystem, which will be valuable for empirical validation once NVM-supporting machines become available.

关键词： Application programs

来源：评论

学校读者我要写书评

暂无评论

2020 18th acm-ieee international conference on formal methods and models for System Design, MEMOCODE 2020

2020 18th ACM-IEEE International Conference on Formal Method...

引用

18th acm-ieee international conference on formal methods and models for System Design, MEMOCODE 2020

ISBN: (纸本)9781728191485

The proceedings contain 18 papers. The topics discussed include: efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions;dependence analysis and automated partitioning for scalable formal analysis of SystemC designs;Bayesian statistical model checking for continuous stochastic logic;safe and efficient collision avoidance control for autonomous vehicles;a contrastive plan explanation framework for hybrid system models;verifying absence of hardware-software data races using counting abstraction;security types for synchronous data flow systems;CROME: contract-based robotic mission specification;and specification-guided software fault localization for autonomous mobile systems.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Learning Optimal Decisions for Stochastic Hybrid Systems 21

Learning Optimal Decisions for Stochastic Hybrid Systems

引用

19th acm-ieee international conference on formal methods and models for System Design (MEMOCODE)

作者： Niehage, Mathis Hartmanns, Arnd Remke, Anne Westfalische Wilhelms Univ Munster Germany Univ Twente Enschede Netherlands

ISBN: (纸本)9781450391276

We apply reinforcement learning to approximate the optimal probability that a stochastic hybrid system satisfies a temporal logic formula. We consider systems with (non)linear continuous dynamics, random events following general continuous probability distributions, and discrete nondeterministic choices. We present a discretized view of states to the learner, but simulate the continuous system. Once we have learned a near-optimal scheduler resolving the choices, we use statistical model checking to estimate its probability of satisfying the formula. We implemented the approach using Q-learning in the tools HYPEG and modes, which support Petri net- and hybrid automata-based models, respectively. Via two case studies, we show the feasibility of the approach, and compare its performance and effectiveness to existing analytical techniques for a linear model. We find that our new approach quickly finds near-optimal prophetic as well as non-prophetic schedulers, which maximize or minimize the probability that a specific signal temporal logic property is satisfied.

关键词： Training Analytical models Q-learning Computational modeling Petri nets Buildings Stochastic processes

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：