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

8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018

作者： Schlick, Rupert Felderer, Michael Majzik, Istvan Nardone, Roberto Raschke, Alexander Snook, Colin Vittorini, Valeria Center for Digital Safety and Security AIT Austrian Institute of Technology GmbH Vienna Austria Department of Computer Science University of Innsbruck Innsbruck Austria Department of Software Engineering Blekinge Institute of Technology Karlskrona Sweden Department of Measurement and Information Systems Budapest University of Technology and Economics Budapest Hungary University of Naples Federico II Naples Italy Institute of Software Engineering and Programming Languages Ulm University Ulm Germany Electronics and Computer Science University of Southampton Southampton United Kingdom

ISBN: (纸本)9783030034269

Formal methods (in a broad sense) have been around almost since the beginning of computer science. Nonetheless, there is a perception in the formal methods community that take-up by industry is low considering the potential benefits. We take a look at possible reasons and give candidate explanations for this effect. To address the issue, we propose a repository of industry-relevant example problems with an accompanying open data storage for experiment results in order to document, disseminate and compare exemplary solutions from formal model based methods. This would allow potential users from industry to better understand the available solutions and to more easily select and adopt a formal method that fits their needs. At the same time, it would foster the adoption of open data and good scientific practice in this research field. © Springer Nature Switzerland AG 2018.

关键词： Formal methods

来源：评论

学校读者我要写书评

暂无评论

Collaborative Filtering Method with the use of Production Rules

Collaborative Filtering Method with the use of Production Ru...

引用

International Conference on Computational Intelligence and Knowledge Economy (ICCIKE)

作者： Amin Salih Mohammed Yelyzaveta Meleshko Saravana Balaji B Semenov Serhii Dept of Computer Engineering Lebanese French University Salahaddin University Erbil KR-Iraq Dept of Cyber Security & Software Central Ukrainian National Technical University Kropyvnytskyi Ukraine Dept of Information Technology Lebanese French University Erbil KR-Iraq Dept of Computer Science and Programming National Technical University (Kharkiv Polytechnic Institute) Ukraine

ISBN: (数字)9781728137780

ISBN: (纸本)9781728137797

this paper proposes a new collaborative filtering method with the calculation of unknown similarity coefficients between users via the application of production rules, which aims to improve the work quality of recommendation systems, to develop of production rules for the developed system. The methods used are: graph theory, the theory of algorithms, mathematical statistics, object-oriented programming, and fuzzy logic. The developed systems are new collaborative filtering method with the definition of unknown similarity coefficients between users through the application of production rules was developed, software for the implementation and testing of this method was developed, experiments on the developed software was conducted. The production rules to determine unknown similarity coefficients in recommendation systems was proposed. The new method of collaborative filtering with the application of production rules has been developed to find unknown similarity coefficients between users that may be possibly used to improve the work quality of the recommendation system. The conducted experiments showed that the developed method enhances the quality indicators of the recommendation system, such as item space coverage and the total number of predicted preferences of users.

关键词： Collaboration Production Information filters Computational intelligence software

来源：评论

学校读者我要写书评

暂无评论

Lemma Functions for Frama-C: C Programs as Proofs

Lemma Functions for Frama-C: C Programs as Proofs

引用

Ivannikov ISPRAS Open Conference (ISPRAS)

作者： Grigoriy Volkov Mikhail Mandrykin Denis Efremov Faculty of Computer Science Higher School of Economics Moscow Russia Software Engineering Department Ivannikov Institute for System Programming of the Russian Academy of Sciences Moscow Russia

ISBN: (纸本)9781728112763;9781728112756

This paper describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel. We illustrate the benefits our approach can bring concerning the effort required to prove lemmas, compared to the approach based on interactive provers such as Coq. Current limitations of the method and its implementation are discussed.

关键词： Tools Manuals Contracts Linux Kernel Economics

来源：评论

学校读者我要写书评

暂无评论

An investigation of technical debt in automatic production systems 17

An investigation of technical debt in automatic production s...

引用

2017 XP Scientific Workshops, XP 2017

作者： Besker, Terese Martini, Antonio Bosch, Jan Tichy, Matthias Chalmers University of Technology Computer Science and Engineering Gothenburg Sweden Ulm University Institute of Software Engineering and Programming Languages Ulm Germany

ISBN: (纸本)9781450352642

Technical Debt is a recent concept, borrowed from the financial domain. It has been recently used in software development to describe technical sub-optimal solutions that have short-term benefits but long-term extra-costs. However, no body of literature investigates how Automatic Production Systems companies deal with Technical Debt. We investigated how Technical Debt is known, how much it hurts and how is managed in an automatic production systems company. Results from one in-depth investigation show that the automatic production systems company spend quite a lot of resources because of Technical Debt, both in the extra-costs (interest) and in its management. The company presents moderate awareness of what Technical Debt is and how much is present in its systems. However, the tracking level is quite low. We, therefore, claim that Technical Debt needs more research in this domain, as it is a source of substantial extracosts and the current practices to manage it are not suitable. © 2017 Association for Computing Machinery.

关键词： software design

来源：评论

学校读者我要写书评

暂无评论

Challenges and research directions for successfully applying MBE tools in practice

Challenges and research directions for successfully applying...

引用

2017 MODELS Satellite Event: Workshops (ModComp, ME, EXE, COMMitMDE, MRT, MULTI, GEMOC, MoDeVVa, MDETools, FlexMDE, MDEbug), Posters, Doctoral Symposium, Educator Symposium, ACM Student Research Competition, and Tools and Demonstrations, MODEL-SSE 2017

作者： Bordeleau, Francis Liebel, Grischa Raschke, Alexander Stieglbauer, Gerald Tichy, Matthias CMind Inc. Canada Software Engineering Division Chalmers University of Gothenburg Sweden Institute of Software Engineering and Programming Languages Ulm University Germany AVL List Gmbh Graz Austria

Model Based engineering aims to improve efficiency and effectiveness of software engineering. Success in industrial practice of MBE does not only depend on the modeling languages and constructive or analytical approaches, like code generation or model checking. It is also heavily influenced by the quality and, particularly, usability of the selected tools. In this position paper, we discuss challenges experienced in applying MBE in practice both from academic as well as industrial viewpoints. Based on the research challenges, we discuss future research directions to improve the chances for the success of MBE in industrial practice.

关键词： Modeling languages

来源：评论

学校读者我要写书评

暂无评论

Lemma functions for frama-C: C programs as proofs

arXiv

引用

arXiv 2018年

作者： Volkov, Grigoriy Mandrykin, Mikhail Efremov, Denis Faculty of Computer Science National Research University Higher School of Economics Moscow Russia Software Engineering Department Ivannikov Institute for System Programming Russian Academy of Sciences Moscow Russia

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

The SCIP optimization suite 8.0

arXiv

引用

arXiv 2021年

作者： Bestuzheva, Ksenia Besançon, Mathieu Chen, Wei-Kun Chmiela, Antonia Donkiewicz, Tim Van Doornmalen, Jasper Eifler, Leon Gaul, Oliver Gamrath, Gerald Gleixner, Ambros Gottwald, Leona Graczyk, Christoph Halbig, Katrin Hoen, Alexander Hojny, Christopher Van Der Hulst, Rolf Koch, Thorsten Lübbecke, Marco Maher, Stephen J. Matter, Frederic Mühmer, Erik Müller, Benjamin Pfetsch, Marc E. Rehfeldt, Daniel Schlein, Steffan Schlösser, Franziska Serrano, Felipe Shinano, Yuji Sofranac, Boro Turner, Mark Vigerske, Stefan Wegscheider, Fabian Wellner, Philipp Weninger, Dieter Witzig, Jakob Zuse Institute Berlin Department AIS2T Takustr. 7 Berlin14195 Germany School of Mathematics and Statistics Beijing Institute of Technology Beijing100081 China RWTH Aachen University Lehrstuhl für Operations Research Kackertstr. 7 Aachen52072 Germany Technische Universiteit Eindhoven Department of Mathematics and Computer Science P.O. Box 513 Eindhoven5600 MB Netherlands I2DAMO GmbH Englerallee 19 Berlin14195 Germany Friedrich-Alexander Universität Erlangen-Nürnberg Department of Data Science Cauerstr. 11 Erlangen91058 Germany University of Twente Department of Discrete Mathematics and Mathematical Programming P.O. Box 217 Enschede7500 AE Netherlands Technische Universität Berlin Software and Algorithms for Discrete Optimization Straße des 17. Juni 135 Berlin10623 Germany Zuse Institute Berlin Department A2IM Takustr. 7 Berlin14195 Germany University of Exeter College of Engineering Mathematics and Physical Sciences Exeter United Kingdom Technische Universität Darmstadt Fachbereich Mathematik Dolivostr. 15 Darmstadt64293 Germany Technische Universität Berlin Straße des 17. Juni 135 Berlin10623 Germany Software and Algorithms for Discrete Optimization Institute of Mathematics Technische Universität Berlin Straße des 17. Juni 135 Berlin10623 Germany GAMS Software GmbH C/o Zuse Institute Berlin Department AIS2T Takustr. 7 Berlin14195 Germany

The SCIP Optimization Suite provides a collection of software packages for mathematical optimization centered around the constraint integer programming framework SCIP. This paper discusses enhancements and extensions contained in version 8.0 of the SCIP Optimization Suite. Major updates in SCIP include improvements in symmetry handling and decomposition algorithms, new cutting planes, a new plugin type for cut selection, and a complete rework of the way nonlinear constraints are handled. Additionally, SCIP 8.0 now supports interfaces for Julia as well as Matlab. Further, UG now includes a unified framework to parallelize all solvers, a utility to analyze computational experiments has been added to GCG, dual solutions can be postsolved by PaPILO, new heuristics and presolving methods were added to SCIP-SDP, and additional problem classes and major performance improvements are available in *** Codes 90C05, 90C10, 90C11, 90C30, 90C90, 65Y05 Copyright © 2021, The Authors. All rights reserved.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

Design and Development of a Mobile Robotic Complex

Design and Development of a Mobile Robotic Complex

引用

International Conference on Recent Innovations in Electrical, Electronics & Communication engineering (ICRIEECE)

作者： Aigul Adamova Tamara Zhukabayeva Laula Zhumabayeva Zhanna Mukanova Khu Ven-Tsen Department of Computer engineering and software Saken Seifullin Kazakh Agrotechnical University Astana Kazakhstan Department of Computing Engineering L.N. Gumilyov Eurasian National University Astana Kazakhstan Department of Information Systems and Power Engineering S. Yessenov Caspian State University of Technology and Engineering Aktau Kazakhstan Department of Information and Computing Systems Karaganda Economic University of Kazpotrebsoyuz Karaganda Kazakhstan Department of Computer engineering and software programming M. Auezov South Kazakhstan State University Shymkent Kazakhstan

ISBN: (数字)9781538659953

ISBN: (纸本)9781538659960

Development of the mobile robot can be executed in two different ways. Firstly, this creation of the built-in system, secondly, the use of "ready to use" industrial components. With distribution of the industrial mobile robots in the market there are more and more components which can be used for creation of all control system and sensors of the robot mobile platform. Use of the ready components doesn't demand the hardware development that accelerates time of development and reduces cost. The chassis of the Belarus-132 mini-tractor is used as a platform of robotic system in the research, "creation" of the program for traffic control is required. Results of the practical research on design and model development of a mobile robotic complex are given.

关键词： Control systems Robot kinematics Mobile robots Navigation Robot sensing systems

来源：评论

学校读者我要写书评

暂无评论

A decidable confluence test for cognitive models in ACT-R

arXiv

引用

arXiv 2017年

作者： Gall, Daniel Frühwirth, Thom Institute of Software Engineering and Programming Languages Ulm University Ulm89069 Germany

Computational cognitive modeling investigates human cognition by building detailed computational models for cognitive processes. Adaptive Control of Thought – Rational (ACT-R) is a rule-based cognitive architecture that offers a widely employed framework to build such models. There is a sound and complete embedding of ACT-R in Constraint Handling Rules (CHR). Therefore analysis techniques from CHR can be used to reason about computational properties of ACT-R models. For example, confluence is the property that a program yields the same result for the same input regardless of the rules that are applied. In ACT-R models, there are often cognitive processes that should always yield the same result while others e.g. implement strategies to solve a problem that could yield different results. In this paper, a decidable confluence criterion for ACT-R is presented. It allows to identify ACT-R rules that are not confluent. Thereby, the modeler can check if his model has the desired behavior. The sound and complete translation of ACT-R to CHR from prior work is used to come up with a suitable invariant-based confluence criterion from the CHR literature. Proper invariants for translated ACT-R models are identified and proven to be decidable. The presented method coincides with confluence of the original ACT-R models. Copyright © 2017, The Authors. All rights reserved.

关键词： Computability and decidability

来源：评论

学校读者我要写书评

暂无评论

Highlights in systems verification

引用

Queue 2017年第4期15卷

作者： Kwon, Albert Wilcox, James EECS Department MIT United States University of Washington Programming Languages and Software Engineering Lab United States

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：