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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

详细简洁

排序：

Modelling Program Verification Tools for Software Engineers 22

Modelling Program Verification Tools for Software Engineers

引用

acm/ieee 25th international conference on Model Driven Engineering Languages and Systems (models)

作者： Lathouwers, Sophie Zaytsev, Vadim Univ Twente Enschede Netherlands

ISBN: (纸本)9781450394666

In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://***/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.

关键词： formal methods Program Verification Megamodelling

来源：评论

学校读者我要写书评

暂无评论

Automating Cryptographic Protocol Language Generation from Structured Specifications 10

Automating Cryptographic Protocol Language Generation from S...

引用

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

作者： Metere, Roberto Arnaboldi, Luca Newcastle Univ Newcastle Upon Tyne Tyne & Wear England Univ Edinburgh Edinburgh Midlothian Scotland Alan Turing Inst London England

ISBN: (纸本)9781450392877

Security of cryptographic protocols can be analysed by creating a model in a formal language and verifying the model in a tool. All such tools focus on the last part of the analysis, verification, and the interpretation of the specification is only explained in papers. Rather, we focus on the interpretation and modelling part by presenting a tool to aid the cryptographer throughout the process and automatically generating code in a target language. We adopt a data-centric approach where the protocol design is stored in a structured way rather than as textual specifications. Previous work shows how this approach facilitates the interpretation to a single language (for Tamarin) which required aftermath modifications. By improving the expressiveness of the specification data structure we extend the tool to export to an additional formal language, ProVerif, as well as a C++ fully running implementation. Furthermore, we extend the plugins to verify correctness in ProVerif and executabiity lemmas in Tamarin. In this paper we model the Diffie-Hellman key exchange, which is traditionally used as a case study;a demo is also provided for other commonly studied protocols, Needham-Schroeder and Needham-Schroeder-Lowe.

关键词： Protocol Design Automated Software Development formal Security models

来源：评论

学校读者我要写书评

暂无评论

Proceedings - 25th acm/ieee international conference on Model Driven Engineering Languages and Systems, models 2022

Proceedings - 25th ACM/IEEE International Conference on Mode...

引用

25th acm/ieee international conference on Model Driven Engineering Languages and Systems, models 2022

ISBN: (纸本)9781450394666

The proceedings contain 35 papers. The topics discussed include: incremental causal connection for self-adaptive systems based on relational reference attribute grammars;addressing the uncertainty interaction problem in software-intensive systems: challenges and desiderata;precomputing reconfiguration strategies based on stochastic timed game automata;system architecture synthesis for performability by logic solvers;digital twin as risk free experimentation aid for techno-socio-economic systems;reactive links across multi-domain engineering models;modelling program verification tools for software engineers;automatic test amplification for executable models;feedback on the formal verification of UML models in an industrial context: the case of a smart device life cycle management system;validating the correctness of reactive systems specifications through systematic exploration;and machine learning methods for model classification: a comparative study.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Proceedings - acm/ieee 25th international conference on Model Driven Engineering Languages and Systems, models 2022: Companion Proceedings

Proceedings - ACM/IEEE 25th International Conference on Mode...

引用

25th acm/ieee international conference on Model Driven Engineering Languages and Systems, models 2022

ISBN: (纸本)9781450394673

The proceedings contain 133 papers. The topics discussed include: towards the practical adoption of LIDL: A toolchain for modeling human-machine interface software interactions;digital TwinCity: a holistic approach towards comparative analysis of business processes;a tool for the automation of efficient multi-robot choreography planning and execution;graphical projectional editing in gentleman;a diagram-centric modeling tool for systems of systems;Picto Web: a tool for complex model exploration;using the modelset dataset to support machine learning in model-driven engineering;modeling tool for managing canvas-based models traceability in ML system development;contract-based product-assembly co-design;ORM ontologies with executable derivation rules to support semantic search in large-scale data applications;and a lightweight approach to the concurrent use and integration of SysML and formal methods in systems design.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Summary of Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa'21) 24

Summary of Workshop on Model Driven Engineering, Verificatio...

引用

24th international acm/ieee conference on Model-Driven Engineering Languages and Systems (models)

作者： Bin Abid, Saad Oliveira, Raquel Ober, Iulian Huawei MRC Munich Germany Univ Toulouse IRIT Toulouse France

The 18th edition of the workshop on Model Driven Engineering, Verification and Validation was held October 2021, virtually. The motivation, scope, objectives, and results of the workshop are summarized.

ISBN: (纸本)9781665424844

关键词： model-driven engineering verification validation formal methods model transformations

来源：评论

学校读者我要写书评

暂无评论

Validation Obligations: A Novel Approach to Check Compliance between Requirements and their formal Specification 43

Validation Obligations: A Novel Approach to Check Compliance...

引用

43rd ieee/acm international conference on Software Engineering - Software Engineering in Practice (ICSE-SEIP) / 43rd acm/ieee international conference on Software Engineering - New Ideas and Emerging Results (ICSE-NIER)

作者： Mashkoor, Atif Leuschel, Michael Egyed, Alexander Johannes Kepler Univ Linz Linz Austria Heinrich Heine Univ Dusseldorf Germany

ISBN: (纸本)9780738133249

Traditionally, practitioners use formal methods predominately for one half of the quality-assurance process: verification (do we build the software right?). The other half - validation (do we build the right software?) - has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach - "validation obligations" - is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system.

关键词： formal methods refinement specification validation obligations

来源：评论

学校读者我要写书评

暂无评论

Automatic Generation of Logical Specifications for Behavioural models

Automatic Generation of Logical Specifications for Behaviour...

引用

ieee/acm international conference on Automated Software Engineering - Workshops (ASE Workshops)

作者： Radoslaw Klimek Julia Witek AGH University of Krakow Krakow Poland

ISBN: (数字)9798400712494

ISBN: (纸本)9798331523169

Logical specifications for behavioural models are crucial for the formal analysis of complex system designs. The automation of obtaining such a specification is essential particularly for promoting logical and deductive methods in software development. This article replicates earlier methods for automatically generating logical specifications equivalent to behavioural models, while also extending the approach to include workflow mining processes. Various and effective interactions with existing theorem provers are also proposed. We conducted straightforward, yet comprehensive, experiments covering multiple stages, which include workflow extraction, automatic logical specification generation, and theorem prover based analysis and the evaluation of these *** CONCEPTS• Theory of computation → Logic and verification, • Information systems → Information systems applications.

关键词： Analytical models Automation Computational modeling conferences Data mining Logic Complex systems Information systems Software engineering Software development management

来源：评论

学校读者我要写书评

暂无评论

Multi-layered Model-based Design Approach towards System Safety and Security Co-engineering 24

Multi-layered Model-based Design Approach towards System Saf...

引用

24th international acm/ieee conference on Model-Driven Engineering Languages and Systems (models)

作者： Quamara, Megha Pedroza, Gabriel Hamid, Brahim Univ Paris Saclay List CEA F-91120 Palaiseau France IRIT Univ Toulouse 118 Route Narbonne F-31062 Toulouse 9 France

ISBN: (纸本)9781665424844

The integration of safety and security concerns in critical domains (e.g., Cyber-Physical Systems (CPSs)) is of utmost importance, and should be conducted in early design phases of system engineering process. Within a Model-Based System Engineering (MBSE) context, safety and security requirements cascade-down across models and views, thus contributing to the detailed missions, functions, and lastly, the architecture. Such enrichment process is often complex and lacks guidance to consistently breakdown high-level mission-centric system specifications into the detailed architecture. In particular, non-savvy safety and security engineers require support to facilitate integration and verification of stringent safety constraints and security exigencies. In this regard, we propose a multi-layered design approach that leverages existing techniques like Model-Driven Engineering (MDE) and formal methods, to facilitate integrated verification of high-level safety and security objectives that can be further specialized across different representations (i.e. mission, functional, and architectural) of the system. The overall approach is validated based upon a Connected Driving Vehicles (CDVs) case study, and using Eclipse Papyrus and Rodin as experimentation tools.

关键词： safety security co-engineering design model-driven engineering formal methods connected driving vehicles

来源：评论

学校读者我要写书评

暂无评论

Vision Paper: Proof-Carrying Code Completions

Vision Paper: Proof-Carrying Code Completions

引用

ieee/acm international conference on Automated Software Engineering - Workshops (ASE Workshops)

作者： Parnian Kamran Premkumar Devanbu Caleb Stanford University of California Davis USA

ISBN: (数字)9798400712494

ISBN: (纸本)9798331523169

Code completions produced by today’s large language models (LLMs) offer no formal guarantees. We propose proof-carrying code completions (PC 3 ). In this paradigm, a high-resourced entity (the LLM provided by the server) must provide a code completion together with a proof of a chosen safety property which can be independently checked by a low-resourced entity (the user). In order to provide safety proofs without requiring the user to write specifications in formal logic, we statically generate preconditions for all dangerous function calls (i.e., functions that may violate the safety property) which must be proved by the *** demonstrate the main ideas, we provide a prototype implementation in the program verification language Dafny, and a case study focusing on file system vulnerabilities. Unlike Python code generated by GPT-4, Dafny code generated by PC 3 provably avoids a common weakness related to path traversal (CWE-35), using a single generation attempt (k = 1) and a modest number of tokens (3, 350). Our tool is available as an open source repository at https://***/DavisPL/*** Concepts• Software and its engineering → formal software verification; Software development techniques; formal methods.

关键词： Codes Large language models Prototypes Software Safety Servers Logic Software engineering Software development management Python

来源：评论

学校读者我要写书评

暂无评论

AI-Assisted Autoformalization of Combinatorics Problems in Proof Assistants

AI-Assisted Autoformalization of Combinatorics Problems in P...

引用

ieee/acm international conference on Software Engineering: New Ideas and Emerging Technologies Results Track (ICSE-NIER)

作者： Long Doan ThanhVu Nguyen Department of Computer Science George Mason University Fairfax VA USA

ISBN: (数字)9798331537111

ISBN: (纸本)9798331537128

Proof assistants such as Coq and LEAN have been increasingly used by renowned mathematicians to formalize and prove mathematical theorems. Despite their growing use, writing formal proofs is challenging, and even the first step of stating the problem formally is difficult as it requires a deep understanding of these systems’ languages. Recent advancements in AI, especially large language models (LLMs), have shown promise in automating this formalization task. However, domains such as combinatorics pose significant challenges for AI-assisted proof assistant systems due to their cryptic nature and the lack of existing data to train AI models. We introduce AutoForm4Lean, a system designed to leverage LLMs to aid in formalizing combinatorics problems for LEAN. By combining LLMs with techniques from software engineering and formal methods such as validation and synthesis, AutoForm4Lean generates formalizations of combinatorics problems more effectively than the current state-of-the-art LLMs. Moreover, this project seeks to provide a comprehensive collection of formalized combinatorics problems, theorems, and lemmas, which would enrich the LEAN library and provide valuable training data for LLMs. Preliminary results demonstrate the effectiveness of AutoForm4Lean in formalizing combinatorics problems in LEAN, making a step forward in AI-based theorem proving.

关键词： Large language models Training data Writing Libraries Data models Software engineering

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：