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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

详细简洁

排序：

MEMOCODE 2019 - 17th acm-ieee international conference on formal methods and models for System Design

MEMOCODE 2019 - 17th ACM-IEEE International Conference on Fo...

引用

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

ISBN: (纸本)9781450369978

The proceedings contain 17 papers. The topics discussed include: a novel compositional semantics of Simulink/state?ow based on quantized state hybrid automata;further sub-cycle and multi-cycle scheduling support for Bluespec Verilog;securing implantable medical devices with runtime enforcement hardware;a timeless model for the veri?cation of quasi-periodic distributed systems;encoding and monitoring responsibility sensitive safety rules for automated vehicles in signal temporal logic;a compositional approach for real-time machine learning;and polyhedral fragments: an e?cient representation for symbolically generating code for processor arrays.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Finite Automata synthesis from interactions

Finite Automata synthesis from interactions

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Erwan Mahe Boutheina Bannour Christophe Gaston Arnault Lapitre Pascale Le Gall CEA List Université Paris-Saclay Palaiseau France Centrale Supélec Université Paris-Saclay Gif-sur-Yvette France

ISBN: (数字)9798400705892

ISBN: (纸本)9798350353662

Interactions are graphical models representing communication flows between actors. Well-known interaction languages include UML Sequence Diagrams or Message Sequence Charts. Even though interactions allow for concise and intuitive specifications, their use remains limited in formal verification, partly because the subsets of formalized languages often lack expressiveness. As many verification methods, such as model-checking or runtime verification, are routinely available for finite automata, we propose a new approach to generate finite automata from an expressive interaction language with operators such as the concurrent region. Our approach leverages an operational semantics to compute derivatives of an interaction and assimilate them to states of a finite automata. In addition, we use term rewriting to merge states on-the-fly so as to obtain small automata without relying on costly a-posteriori minimization techniques.

关键词： Sequential analysis Runtime Graphical models Instruments Computational modeling Unified modeling language Semantics

来源：评论

学校读者我要写书评

暂无评论

SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation

SolSearch: An LLM-Driven Framework for Efficient SAT-Solving...

引用

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

作者： Junjie Sheng Yanqiu Lin Jiehao Wu Yanhong Huang Jianqi Shi Min Zhang Xiangfeng Wang School of Computer Science and Technology East China Normal University Shanghai China Software Engineering Institute East China Normal University Shanghai China School of Computer Science and Technology Shanghai Formal-Tech Information Technology Co. Lt East China Normal University Shanghai China

ISBN: (数字)9798331537111

ISBN: (纸本)9798331537128

The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering, including automated testing, configuration management, and program verification. This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically. Leveraging a curriculum-based, trial-and-error process, SolSearch enables the LLM to iteratively modify and generate SAT solver code, thereby improving solving efficiency and performance. This automated SAT-solving paradigm has the advantage of being plug-and-play, allowing integration with any SAT solver and accelerating the development or design process of new SAT solvers (new methods). Our preliminary experimental results are encouraging by demonstrating that the LLM-powered paradigm improves state-of-the-art SAT solvers on general SAT benchmarks and significantly enhances the performance of the widely used Z3 solver (11% on PAR-2 score). These results highlight the potential for using LLM-driven methods to advance solver adaptability and effectiveness in real-world software engineering challenges. Future research directions are discussed to further refine and validate this approach, offering a promising avenue for integrating AI with traditional software engineering tasks.

关键词： Codes Large language models Configuration management Benchmark testing Software engineering

来源：评论

学校读者我要写书评

暂无评论

Llm-Based Generation of Weakest Preconditions and Precise Array Invariants

Llm-Based Generation of Weakest Preconditions and Precise Ar...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Daragh King Vasileios Koutavas Laura Kovács School of Computer Science and Statistics Trinity College Dublin Dublin Ireland Lero Research Ireland Centre for Software School of Computer Science and Statistics Trinity College Dublin Dublin Ireland Faculty of Informatics TU Wien Vienna Austria

ISBN: (数字)9798331537944

ISBN: (纸本)9798331501761

The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas such as software verification and runtime error-checking. For programs containing loops, WP generation critically depends upon synthesizing loop invariants that are inductive in nature; these WPs then essentially embed the inductive properties required for program verification. This paper investigates the use of Large Language models (LLMs) to generate WPs (and accompanying loop invariants) in order to prove the correctness of nondeterministic programs containing arrays, loops, and arithmetic. Specifically, we employ several models of ChatGPT to derive the WPs and invariants for the aforementioned programs. We then compare these LLM-derived WPs and invariants to their provable counterparts obtained by the MaxPrANQ tool. We find that the quality of the LLM-derived results can vary greatly and is highly dependent on the underlying model used by ChatGPT. This variance in performance propels us to outline directions for future work and discuss how LLMs and formal-tools can complement one another in generating valid WPs and strong invariants.

关键词： Runtime Large language models Propulsion Benchmark testing Chatbots Software Arithmetic

来源：评论

学校读者我要写书评

暂无评论

Cps Falsification Using Autoencoded Input models

Cps Falsification Using Autoencoded Input Models

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Youssef Gordon Zahar Sanjai Rayadurgam Department of Computer Science and Engineering University of Minnesota Minneapolis Minnesota

ISBN: (数字)9798331537944

ISBN: (纸本)9798331501761

Modern Cyber-Physical Systems (CPS) increasingly utilize AI-enabled controllers with deep neural networks (DNNs). As these systems grow in complexity, traditional verification methods become less effective. A practical alternative is falsification, a search for inputs that cause the system to violate specified properties. Falsification techniques can be categorized into black-box methods, which are implementation agnostic and rely on general heuristics to guide the search, and white-box methods, which utilize implementation-specific information to better direct the search, but their applicability may be limited to specific controller types. This paper introduces an input-model-driven falsification approach, a novel black-box technique that leverages a learned representation of the input domain for better directing the search without relying on the internals of the system model being falsified. By utilizing a Variational Autoencoder (VAE) to encode inputs into low-dimensional embeddings, this approach captures useful problem-domain-specific information to guide the falsification process without sacrificing the generality of blackbox techniques. Evaluations on CPS models from the autonomous driving domain show a falsification success rate of 60.18 %, outperforming Breach, a well-known black-box tool, and being competitive with FalsifAI, a state-of-the-art white-box framework specifically targeting DNN controllers.

关键词： Manifolds Runtime Autoencoders Closed box Encoding Safety Reliability Monitoring Glass box Overfitting

来源：评论

学校读者我要写书评

暂无评论

Robustness Verification of Video Classification Neural Networks

Robustness Verification of Video Classification Neural Netwo...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Samuel Sasaki Diego Manzanas Lopez Preston K. Robinette Taylor T. Johnson Department of Computer Science Vanderbilt University Nashville USA Institute for Software Integrated Systems Vanderbilt University Nashville USA

ISBN: (数字)9798331537944

ISBN: (纸本)9798331501761

Deep neural networks (DNNs) have shown impressive performance in computer vision tasks, driven by the availability of large datasets and advanced deep learning techniques. This success has prompted the formal methods community to explore ways of evaluating and improving the reliability and correctness of these models. These verification efforts, however, have primarily focused on neural networks that process image or feature data, overlooking architectures designed for video data. This oversight hinders the deployment of advanced computer vision techniques for safety-critical tasks such as video surveillance, self-driving, and industrial automation, where reliable performance is required. In this work, we develop a formal verification approach for video classification tasks. This includes a novel abstract convex set definition that can represent video data (image data with a temporal component), as well as new reachability methods for layers commonly used by video classification neural networks such as three-dimensional convolutional and three-dimensional pooling layers. Additionally, we construct 3 datasets: Zoom In MNIST, Zoom Out MNIST, and GTRSB Video. These are built upon common datasets from image classification (MNIST, GTSRB). These three datasets and the ST-MNIST dataset are used to train a video classification neural network and then formally verify their robustness against $\mathrm{L}_{\infty}$ norm perturbations. Our results show the scalability of our approach to different input sizes and where the main challenges in this domain are.

关键词： Deep learning Computer vision Perturbation methods Computer network reliability Scalability Computer architecture Video surveillance Robustness Image classification formal verification

来源：评论

学校读者我要写书评

暂无评论

Challenges in Empirically Testing Memory Persistency models

Challenges in Empirically Testing Memory Persistency Models

引用

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

作者： Vasileios Klimis Alastair F. Donaldson Viktor Vafeiadis John Wickerson Azalea Raad Queen Mary University of London Imperial College London MPI-SWS

ISBN: (数字)9798400705007

ISBN: (纸本)9798350352139

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.

关键词： Out of order Nonvolatile memory Computer architecture Software Software reliability Testing Software engineering

来源：评论

学校读者我要写书评

暂无评论

Compositional Analysis of Parametric Cooperative Cyber-Physical Systems

Compositional Analysis of Parametric Cooperative Cyber-Physi...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Raniah A. Alghamdi Richard Trefler University of Waterloo Canada King Abdulaziz University Saudi Arabia

ISBN: (数字)9798400705892

ISBN: (纸本)9798350353662

This paper studies the parameterized compositional model checking problem (PCMCP) for analyzing global safety properties of cooperative Cyber-Physical Systems modeled as networks of hybrid automata. We develop the modular verification technique of PCMCP to analyze global safety properties of parametric models of distributed cooperative agents, where each agent is modeled as a hybrid I/O automaton (HIOA). Combining local symmetry amongst the agents, compositionality, and parametric analysis can avoid the computational cost associated with global analysis of the hybrid system’s state space. PCMCP involves analyzing the local symmetry of the agent networks and the agents’ continuous interfering interactions with their neighboring agents. This analysis identifies a representative agent (HIOA) from each locally symmetric equivalent class of the system. A key step in this analysis is the calculation of overapproximations of the reachable states set for representative agents in a small cutoff instance of the system that then generalizes to arbitrarily sized HIOA networks. We illustrate this technique by outlining its application to compute a compositional local invariant for a platoon of N cooperative adaptive cruise control (CACC) vehicles. We establish a platoon cutoff and show that our simplified CACC model is collision-free, which then generalizes to the entire platoon family.

关键词： Analytical models Adaptation models Computational modeling Automata Cyber-physical systems Cognition Safety

来源：评论

学校读者我要写书评

暂无评论

Model Assisted Refinement of Metamorphic Relations for Scientific Software

Model Assisted Refinement of Metamorphic Relations for Scien...

引用

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

作者： Clay Stevens Katherine Kjeer Ryan Richard Edward Valeev Myra B. Cohen Dept. of Computer Science Iowa State University Ames IA USA Dept. of Chemistry Iowa State University Ames IA USA Dept. of Chemistry Virginia Tech Blacksburg VA USA

ISBN: (数字)9798331537111

ISBN: (纸本)9798331537128

Ensuring the correctness of scientific software is challenging due to the need to represent and model complex phenomenon in a discrete form. Many dynamic approaches for correctness have been developed for numerical overflow or imprecision, which may manifest as program crashes or hangs. Less effort has been spent on functional correctness, where one of the most widely proposed technique is metamorphic testing. Metamorphic testing often requires deep domain expertise to design meaningful relations. In this vision paper we ask if we can utilize the process of abstraction and refinement, a traditionally formal approach, to guide the development of metamorphic relations. We have built an iterative approach we call Model Assisted Refinements (or MARS). It starts with domain-agnostic relations and a set of input-output relations created via a dynamic analysis. We then use a model checker to identify missing input/output patterns and potential passing and failing relations. We augment our dynamic analysis, and obtain domain expertise to verify and refine our relations. At the end we have a set of domain-specific metamorphic relations and test cases. We demonstrate our approach on a high-performance chemistry library. Within three refinements we discover several domain specific relations, and increase our behavioral coverage.

关键词： Quantum chemistry Model checking Software Libraries Data models Numerical models Iterative methods Data mining Testing Software engineering

来源：评论

学校读者我要写书评

暂无评论

Leveraging Large Language models to Boost Dafny’s Developers Productivity

Leveraging Large Language Models to Boost Dafny’s Developer...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Álvaro Silva Alexandra Mendes João F. Ferreira Independent Researcher Porto Portugal HASLab / INESC TEC & Faculty of Engineering University of Porto Porto Portugal INESC-ID & IST University of Lisbon Lisbon Portugal

ISBN: (数字)9798400705892

ISBN: (纸本)9798350353662

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 *** 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 *** CONCEPTS• Software and its engineering → Software notations and tools; Software verification and validation.

关键词： Productivity Costs Manuals Maintenance engineering Syntactics Software formal specifications

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：