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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

1,551 篇 会议
50 篇 期刊文献
35 册 图书

馆藏范围

1,634 篇 电子文献
2 种 纸本馆藏

日期分布

学科分类号

1,175 篇 工学
- 870 篇 计算机科学与技术...
- 557 篇 软件工程
- 135 篇 电气工程
- 123 篇 控制科学与工程
- 94 篇 信息与通信工程
- 91 篇 土木工程
- 88 篇 机械工程
- 76 篇 建筑学
- 61 篇 安全科学与工程
- 58 篇 材料科学与工程（可...
- 41 篇 交通运输工程
- 37 篇 动力工程及工程热...
- 33 篇 化学工程与技术
- 29 篇 生物工程
- 28 篇 仪器科学与技术
- 25 篇 力学（可授工学、理...
- 23 篇 生物医学工程（可授...
330 篇 理学
- 226 篇 数学
- 75 篇 统计学（可授理学、...
- 68 篇 系统科学
- 44 篇 物理学
- 42 篇 生物学
- 28 篇 化学
218 篇 管理学
- 155 篇 管理科学与工程(可...
- 87 篇 图书情报与档案管...
- 79 篇 工商管理
32 篇 医学
- 24 篇 基础医学(可授医学...
- 24 篇 临床医学
30 篇 法学
- 27 篇 社会学
24 篇 经济学
- 23 篇 应用经济学
17 篇 教育学
15 篇 文学
10 篇 农学
6 篇 艺术学
5 篇 军事学

主题

68 篇 model checking
43 篇 tools
35 篇 algorithm design...
28 篇 software enginee...
28 篇 static analysis
26 篇 data mining
23 篇 stochastic syste...
20 篇 real time system...
20 篇 computational mo...
20 篇 analytical model...
17 篇 hybrid systems
17 篇 real-time system...
17 篇 machine learning
17 篇 testing
16 篇 software tools
16 篇 optimization
16 篇 computers
16 篇 sentiment analys...
16 篇 software
16 篇 data models

机构

26 篇 rhein westfal th...
13 篇 ludwig maximilia...
8 篇 univ penn philad...
7 篇 univ twente ensc...
7 篇 univ twente form...
7 篇 tech univ munich...
6 篇 univ illinois ur...
5 篇 saarland univ sa...
5 篇 rhein westfal th...
5 篇 chinese acad sci...
5 篇 suny stony brook...
5 篇 univ calif berke...
5 篇 univ texas austi...
4 篇 radboud univ nij...
4 篇 verimag ctr equa...
3 篇 university of wa...
3 篇 vienna universit...
3 篇 univ colorado bo...
3 篇 tu wien austria
3 篇 carnegie mellon ...

作者

22 篇 katoen joost-pie...
14 篇 beyer dirk
10 篇 junges sebastian
9 篇 parker david
8 篇 quatmann tim
8 篇 hermanns holger
7 篇 kwiatkowska mart...
6 篇 van de pol jaco
6 篇 yi w
6 篇 hartmanns arnd
5 篇 majumdar rupak
5 篇 podelski andreas
5 篇 bozga marius
5 篇 alur rajeev
5 篇 pettersson p
5 篇 cimatti alessand...
5 篇 norman gethin
4 篇 behrmann gerd
4 篇 latella diego
4 篇 ruys theo c.

语言

1,520 篇 英文
86 篇 其他
14 篇 德文
10 篇 中文
4 篇 葡萄牙文
3 篇 俄文
1 篇 捷克文

检索条件"任意字段=11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems"

共 1636 条记录，以下是341-350 订阅

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

详细简洁

排序：

Structural Invariants for the Verification of systems with Parameterized Architectures 26th

Structural Invariants for the Verification of Systems with P...

引用

26th international conference on tools and algorithms for construction and analysis of systems (TACAS)

作者： Bozga, Marius Esparza, Javier Iosif, Radu Sifakis, Joseph Welzel, Christoph Univ Grenoble Alpes Verimag Grenoble INP CNRS St Martin Dheres France Tech Univ Munich Munich Germany

ISBN: (纸本)9783030451899;9783030451905

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology of the system (e.g. pipeline, ring). the logic can be easily embedded in monadic second order logic of >= 1 successors (WS kappa S), and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems, including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Research and Application of Big Data Correlation analysis in Education 11th

Research and Application of Big Data Correlation Analysis in...

引用

11th international conference on Intelligent Networking and Collaborative systems (INCoS) / 22nd international conference on Network-Based Information systems (NBiS)

作者： Bo, Du Ai, Li Chen, Yuan Engn Univ PAP Xian Shanxi Peoples R China

ISBN: (纸本)9783030290351;9783030290344

How to adjust the training and construction plan for the college faculty and improve their capacity or education and instruction in Chinese universities is an urgent problem to be explored and solved under the background of education big data. In the era of big data, relevant analysis has received extensive attention because of its ability to discover the intrinsic associations between things quickly and efficiently, and has been effectively applied to various fields. In this paper, we are based on the data of 2018 senior professional title defense in several Chinese universities to analyze the correlation between the respondent's grades and ages, education and majors by using big data correlation mining technology. the purpose is to explore the status quo and problems of teachers' talent team construction, and then find a suitable way for the construction and training of college teachers in the era of big data.

关键词： Correlation analysis Education big data Teachers team construction Senior title defense

来源：评论

学校读者我要写书评

暂无评论

Endicheck: Dynamic analysis for Detecting Endianness Bugs 26th

Endicheck: Dynamic Analysis for Detecting Endianness Bugs

引用

26th international conference on tools and algorithms for construction and analysis of systems (TACAS)

作者： Kapl, Roman Parizek, Pavel Charles Univ Prague Fac Math & Phys Dept Distributed & Dependable Syst Prague Czech Republic

ISBN: (纸本)9783030452360;9783030452377

Computers store numbers in two mutually incompatible ways: little-endian or big-endian. they differ in the order of bytes within representation of numbers. this ordering is called endianness. When two computer systems, programs or devices communicate, they must agree on which endianness to use, in order to avoid misinterpretation of numeric data values. We present Endicheck, a dynamic analysis tool for detecting endianness bugs, which is based on the popular Valgrind framework. It helps developers to find those code locations in their program where they forgot to swap bytes properly. Endicheck requires less source code annotations than existing tools, such as Sparse used by Linux kernel developers, and it can also detect potential bugs that would only manifest if the given program was run on computer with an opposite endianness. Our approach has been evaluated and validated on the Radeon SI Linux OpenGL driver, which is known to contain endianness-related bugs, and on several open-source programs. Results of experiments show that Endicheck can successfully identify many endianness-related bugs and provide useful diagnostic messages together with the source code locations of respective bugs.

关键词： Linux

来源：评论

学校读者我要写书评

暂无评论

An O(m log n) algorithm for branching bisimilarity on labelled transition systems 26th

An O(m log n) algorithm for branching bisimilarity on labell...

引用

26th international conference on tools and algorithms for construction and analysis of systems (TACAS)

作者： Jansen, David N. Groote, Jan Friso Keiren, Jeroen J. A. Wijs, Anton Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Eindhoven Univ Technol Dept Math & Comp Sci Eindhoven Netherlands

ISBN: (纸本)9783030452360;9783030452377

Branching bisimilarity is a behavioural equivalence relation on labelled transition systems (LTSs) that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than ones for other weak behavioural equivalences, especially weak bisimilarity. With m the number of transitions and n the number of states, the classic O(mn) algorithm was recently replaced by an O(m(log |Act | + log n)) algorithm [9], which is unfortunately rather complex. this paper combines its ideas with the ideas from Valmari [20], resulting in a simpler O(mlog n) algorithm. Benchmarks show that in practice this algorithm is also faster and often far more memory efficient than its predecessors, making it the best option for branching bisimulation minimisation and preprocessing for calculating other weak equivalences on LTSs.

关键词： Branching bisimilarity Algorithm Labelled transition systems

来源：评论

学校读者我要写书评

暂无评论

Development of Indirect Determination Model Based on Neural Networks for the Process of Iron Ore Beneficiation 5

Development of Indirect Determination Model Based on Neural ...

引用

5th international conference on Computational Linguistics and Intelligent systems (COLINS)

作者： Senko, Anton Kupin, Andrey Osadchuk, Yuriy Kryvyi Rih Natl Univ Vitaliy Matusevych Str 11 UA-50027 Kryvyi Rih Ukraine

the object of research is the processes of beneficiation of iron ore in the conditions of a mining and processing plant. the technology of operative forecasting of data of monitoring of production processes provides integration in the SCADA-systems of the specialized means of computer modeling operating at the industrial enterprises for the purpose of operative forecasting of technological indicators of production process. One of the main tasks of technology is to determine the formal connections between the components of the process input space. the large amount of process monitoring data provided by SCADA systems suggests that positive results can be obtained by using Data Mining methods, which allow not only to identify implicit relationships in the data, but also significantly reduce the dimensionality of the problem. the application of fuzzy logic and neural network methods for the construction of models of rapid analysis and forecasting of production process parameters based on current monitoring data can also be promising within the framework of the considered technology. this assumption is confirmed by the fact that the fuzzy logic device is already included in the libraries of the following SCADA-systems: DELTAV, TRACE MODE, SIMATIC WINCC, LABVIEW DSC and others. In the study of common intelligent computing architectures, it was found that the greatest prospects have counter-spread neural networks. Networks of this type have less learning time than reverse distribution networks. therefore, such a network will respond quickly to changes in the conditions of the benefication process associated with fluctuations in the characteristics of raw materials. the following algorithms are combined in the counter-propagation neural network: the Kohonen self-organizing map and the Grossberg star.

关键词： Classification Model Computer Support System For Solutions Neural Network Ore Beneficiation

来源：评论

学校读者我要写书评

暂无评论

Comparative analysis of linear electromechanical steering drives with an autonomous hydraulic drive 11

Comparative analysis of linear electromechanical steering dr...

引用

11th international Scientific and Technical conference on Robotic and Intelligent Aircraft systems Improving Challenges, RIASIC 2020

作者： Abdulin, R.R. Bolshakov, V.V. Podshibnev, V.A. Rozhnin, N.B. Samsonovich, S.L. Joint Stock Company Avionica 7 ul. Obraztsova Moscow127055 Russia Moscow Aviation Institute National Research University 4 Volokolamskoe shosse Moscow125993 Russia

the work is devoted to the topical problem of choosing a scheme of a linear electromechanical drive, developed as an alternative to an autonomous electro-hydraulic drive. Mass characteristics of the main functional elements of the actuators: electric motors and ball screws are considered. Synchronous motors and a collector motors were considered in this work as an electric motor. Ball-screw transmissions with separator and ball-screw transmissions with recirculation of balls were considered in this work as a ball-screw transmission. Comparison was made according to functional, technological and economic criteria of two schemes for construction of linear electromechanical drives: with intermediate mechanical transmission based on a collector motor and based on a permanent magnet synchronous motor without an intermediate mechanical transmission. the comparison showed that the scheme with an intermediate mechanical transmission has better mass characteristics compared to the scheme without an intermediate mechanical transmission with similar dynamic characteristics. the presented comparison results can be useful in solving the problem of choosing schemes for newly developed electric electromechanical steering drives. © Published under licence by IOP Publishing Ltd.

关键词： Permanent magnets

来源：评论

学校读者我要写书评

暂无评论

Uncertainty, Modeling and Safety Assurance: Towards a Unified Framework 1

引用

11th international Working conference on Verified Software - theories, tools, and Experiments (VSTTE)

作者： Chechik, Marsha Kokaly, Sahar Rahimi, Mona Salay, Rick Viger, Torin Univ Toronto Toronto ON Canada

ISBN: (数字)9783030416003

ISBN: (纸本)9783030416003;9783030415990

Uncertainty occurs naturally in software systems, including those that are model-based. When such systems are safety-critical, they need to be assured, e.g., by arguing that the system satisfies its safety goals. But how can we rigorously reason about assurance in the presence of uncertainty? In this paper, we propose a vision for a framework for managing uncertainty in assurance cases for software systems, and in particular, for model-based software systems, by systematically identifying, assessing and addressing it. We also discuss a set of challenges that need to be addressed to realize this framework.

关键词： Uncertainty analysis

来源：评论

学校读者我要写书评

暂无评论

On Application of Combined Pile-Raft Foundations for Road Structures 11th

On Application of Combined Pile-Raft Foundations for Road St...

引用

11th international conference on Environmental Engineering (ICEE)

作者： Leppla, Steffen Norkus, Arnoldas Ingenieursozietat Prof Dr Ingn Katzenbach GmbH Darmstadt Germany Vilnius Gediminas Tech Univ Lab Geotech Vilnius Lithuania

ISBN: (纸本)9786094762321

Roads and road infrastructure systems are designed to satisfy ultimate and serviceability conditions under long-term actions caused by transport loadings and environmental effects. Selected design solutions must be safe and rational in terms of construction and maintenance costs. In cases when weak or soft soil layers of natural soil profiles are shallow and/or the traffic loads are very large, the Combined Pile-Raft Foundation (CPRF) is the economical road and railway structure design solution. Application of CPRF is cheaper geotechnical solution comparing with soil change or usual piled foundation alternatives. the development of this system is based on the analysis of relevant mechanical properties of soil layers and the evaluation of the soil-structure interaction. the soil-structure interaction is of highest importance allowing proper evaluation of load bearing resistance and deformation transmitted by raft and piles to soil layers. the soil and foundation system usually is subjected by loadings, resulting elastic-plastic resistance range. therefore, relevant nonlinear physical laws due to the stress levels are used. the paper purpose is summarizing the experience of application of Combined Pile-Raft Foundations used in road and railway construction and bridge engineering.

关键词： road structure soil-structure interaction Combined Pile-Raft Foundations performance analysis

来源：评论

学校读者我要写书评

暂无评论

Learning One-Clock Timed Automata 26th

Learning One-Clock Timed Automata

引用

26th international conference on tools and algorithms for construction and analysis of systems (TACAS)

作者： An, Jie Chen, Mingshuai Zhan, Bohua Zhan, Naijun Zhang, Miaomiao Tongji Univ Sch Software Engn Shanghai Peoples R China Rhein Westfal TH Aachen Lehrstuhl Informat 2 Aachen Germany Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Univ Chinese Acad Sci Beijing Peoples R China

ISBN: (纸本)9783030451899;9783030451905

We present an algorithm for active learning of deterministic timed automata with a single clock. the algorithm is within the framework of Angluin's L* algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each transition whether it resets the clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the teacher is assumed to be smart in the sense of being able to provide the reset information. We show that this simpler setting yields a polynomial complexity of the learning process. Both of the algorithms are implemented and evaluated on a collection of randomly generated examples. We furthermore demonstrate the simpler algorithm on the functional specification of the TCP protocol.

关键词： Automaton learning Active learning One-clock timed automata Timed language Reset-logical-timed language.

来源：评论

学校读者我要写书评

暂无评论

Scenario-Based Verification of Uncertain MDPs 26th

Scenario-Based Verification of Uncertain MDPs

引用

26th international conference on tools and algorithms for construction and analysis of systems (TACAS)

作者： Cubuktepe, Murat Jansen, Nils Junges, Sebastian Katoen, Joost-Pieter Topcu, Ufuk Univ Texas Austin Austin TX 78712 USA Radboud Univ Nijmegen Nijmegen Netherlands Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9783030451899;9783030451905

We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. the probability distributions for these random parameters are unknown. the problem is to compute the probability to satisfy a temporal logic specification within any MDP that corresponds to a sample from these unknown distributions. In general, this problem is undecidable, and we resort to techniques from so-called scenario optimization. Based on a finite number of samples of the uncertain parameters, each of which induces an MDP, the proposed method estimates the probability of satisfying the specification by solving a finite-dimensional convex optimization problem. the number of samples required to obtain a high confidence on this estimate is independent from the number of states and the number of random parameters. Experiments on a large set of benchmarks show that a few thousand samples suffice to obtain high-quality confidence bounds with a high probability.

关键词： MDP Uncertainty Verification Scenario optimisation

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共164页 << < 31 32 33 34 35 36 37 38 39 40 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：