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

27th International Conference on Fundamental Approaches to software Engineering (FASE)

作者： Barth, Max Dietsch, Daniel Heizmann, Matthias Jakobs, Marie-Christine Ludwig Maximilians Univ Munchen Munich Germany Univ Freiburg Freiburg Germany

ISBN: (纸本)9783031572586;9783031572593

We introduce Ultimate TestGen, a novel tool for automatic test-case generation. Like many other test-case generators, Ultimate Test-Gen builds on verification technology, i.e., it checks the (un)reachability of test goals and generates test cases from counterexamples. In contrast to existing tools, it applies trace abstraction, an automata-theoretic approach to software model checking, which is implemented in the successful verifier Ultimate Automizer. To avoid that the same test goal is reached again, Ultimate TestGen extends the automata-theoretic model checking approach with error automata.

关键词： Ultimate Automizer Test-case generation software testing Test Coverage software model checking Automata

来源：评论

学校读者我要写书评

暂无评论

software model checking with Uninterpreted Functions

Software Model Checking with Uninterpreted Functions

引用

作者： Bueno, Denis University of Michigan

学位级别：博士

software model checkers attempt to algorithmically synthesize an inductive proof that a piece of software is safe. Such proofs are composed of complex logical assertions about program variables and control structures, and are computationally expensive to produce. Our unifying motivation is to increase the efficiency of verifying software control behavior despite its dependency on data. Control properties include important topics such as mutual exclusion, safe privilege elevation, and proper usage of networking and other APIs. These concerns motivate our techniques and evaluations. Our approach integrates an efficient abstraction procedure based on the logic of equality with uninterpreted functions (EUF) into the core of a modern model checker. Our checker, called euforia, targets control properties by treating a program’s data operations and relations as uninterpreted functions and predicates, respectively. This reduces the cost of building inductive proofs, especially for verifying control relationships in the presence of complex but irrelevant data processing. We show that our method is sound and terminates. We provide a ground-up implementation and evaluate the abstraction on a variety of software verification benchmarks. We show how to extend this abstraction to memory-manipulating programs. By judicious abstraction of array operations to EUF, we show that we can directly reason about array reads and adaptively learn lemmas about array writes leading to significant performance improvements over existing approaches. We show that our abstraction of array operations completely eliminates much of the array theory reasoning otherwise required. We report on experiments with and without abstraction and compare our checker to the state of the art. Programs with procedures pose unique difficulties and opportunities. We show how to retrofit a model checker not supporting procedures so that it supports modular analysis of programs with non-recursive procedures. This t

关键词： software model checking Equality with uninterpreted functions Thesis

来源：评论

学校读者我要写书评

暂无评论

A Novel RVFL-Based Algorithm Selection Approach for software model checking 15th

A Novel RVFL-Based Algorithm Selection Approach for Software...

引用

15th International Conference on Knowledge Science, Engineering, and Management (KSEM)

作者： Cao, Weipeng Wu, Yuhao Wang, Qiang Zhang, Jiyong Zhang, Xingjian Qiu, Meikang Civil Aviat Univ China CAAC Key Lab Civil Aviat Wide Surveillance Safe operat Management & Control Technol Tianjin Peoples R China Shenzhen Univ Coll Comp Sci & Software Engn Shenzhen Peoples R China Chinese Acad Mil Sci Inst Syst Engn Beijing Peoples R China Hangzhou Dianzi Univ Sch Automat Hangzhou Peoples R China Texas A&M Univ Commerce Dept Comp Sci Commerce TX USA

ISBN: (纸本)9783031109898;9783031109881

software model checking is the technique that automatically verifies whether software meets the given correctness properties. In the past decades, a large number of model checking techniques and tools have been developed, reaching a point where modern model checkers are sophisticated enough to handle large-scale software systems. However, due to the fact that the software model checkering techniques are diverse and each of them is designed and optimized for a specific type of software system, it remains a hard problem for engineers to efficiently combine them to verify the complex software systems in practice. To alleviate this problem, we propose a novel algorithm selection approach based on Random Vector Functional Link net (RVFL) for software model checking, namely Kaleidoscopic RVFL (K-RVFL). The novel design of feature hybridization and fusion enables K-RVFL to extract more diverse and multi-level features. We have also carried out a thorough experimental evaluation on a publicly available data set and compared K-RVFL with a number of neural networks, including RVFL, Extreme Learning Machine (ELM), Stochastic Configuration Network (SCN), Back Propagation algorithm (BP), and Supporting Vector Machine (SVM). The experimental results demonstrate the usefulness and effectiveness of K-RVFL.

关键词： software verification software model checking Algorithm selection Random vector functional link Neural networks

来源：评论

学校读者我要写书评

暂无评论

IC3 software model checking

引用

INTERNATIONAL JOURNAL ON software TOOLS FOR TECHNOLOGY TRANSFER 2020年第2期22卷 135-161页

作者： Lange, Tim Neuhaeusser, Martin R. Noll, Thomas Katoen, Joost-Pieter Rhein Westfal TH Aachen Aachen Germany Siemens AG Munich Germany

In recent years, the inductive, incremental verification algorithm IC3 had a major impact on hardware model checking. Also for software model checking, a number of adaptations of Boolean IC3 and combinations with CEGAR and ART-based techniques have been developed. However, most of them exploit the peculiarities of software programs, such as the explicit representation of control flow, only to a limited extent. In this paper, we present an approach that supports this explicit representation in the form of control-flow automata, and integrates it with symbolic reasoning about the data state space of the program. By maintaining reachability information specifically for each control location, we arrive at a "two-dimensional" extension of IC3, which provides a true lifting from hardware to software model checking. Moreover, we address the problem of generalization in this setting, an essential feature to ensure the scalability of IC3. We introduce several improvements that range from efficient caching of generalizations over variable reductions to syntax-oriented generalization by means of weakest preconditions. Using a prototypical implementation, we evaluate our approach on a number of case studies, including a significant subset of the SV-COMP 2018 benchmarks, and compare the outcomes with results obtained from other IC3 software model checkers.

关键词： Program verification Safety properties software model checking IC3

来源：评论

学校读者我要写书评

暂无评论

An improved method of k-induction combined with predicate abstraction and CEGAR for software model checking

引用

CLUSTER COMPUTING-THE JOURNAL OF NETWORKS software TOOLS AND APPLICATIONS 2019年第3-Sup期22卷 S6219-S6229页

作者： Wang, Shun Du, Ye Han, Zhen Beijing Jiaotong Univ Sch Comp & Informat Technol Beijing 100044 Peoples R China

K-induction and predicate abstraction are well known techniques for unbounded software model checking. However, these methods are always treated as completely different in previous works. In the paper, we develop a combined method that merges k-induction and predicate abstraction into a CEGAR-based general abstraction method, which divides the target program into blocks that can be explored separately and extends k-induction in an abstract domain. Experiment results show that the combined method balances effectiveness and efficiency on k-induction and predicate abstraction implementations.

关键词： Abstract-refinement software model checking Optimization algorithm Predicate analysis Interpolation Shape analysis

来源：评论

学校读者我要写书评

暂无评论

Review of software model-checking Techniques for Dealing with Error Detection in Program Codes

引用

Journal of software Engineering and Applications 2023年第6期16卷 170-192页

作者： Ednah Olubunmi Aliyu Department of Computer Science Adekunle Ajasin University Akungba-Akoko Nigeria

Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.

关键词： software model checking Symbolic Execution State Explosion Abstraction Test Case Generations

来源：评论

学校读者我要写书评

暂无评论

software model checking for resources race

引用

CLUSTER COMPUTING-THE JOURNAL OF NETWORKS software TOOLS AND APPLICATIONS 2017年第1期20卷 179-193页

作者： Wang, Hong Zhang, Tao North China Elect Power Univ Sch Control & Comp Rd Beinong 2 Beijing 100206 Peoples R China Chinese Acad Sci Technol & Engn Ctr Space Utilizat Beijing 100096 Peoples R China

The difficulty of finding resources race is well known. Such errors are hard to be detected, because they often happen irregularly and reproduce difficultly. Especially, the kind race conflicts exist among processes, threads, and interrupts. This paper provided a novel approach to detect the resources race, namely software model checking. It constructed Boolean program and Promela models for resources race. Furthermore, the Promela models have been tested by using the model checker, SPIN. software model checking can detect resources race in concurrent program without running, although the program had used timing control or mutual exclusion lock to avoid the race. Furthermore, it can find deadlock also, if the program use the mutual locks in a wrong way.

关键词： Resources race software model checking Predicate abstraction Boolean program Premela SPIN

来源：评论

学校读者我要写书评

暂无评论

Verifying Cyber-Physical Systems by Combining software model checking with Hybrid Systems Reachability 13

Verifying Cyber-Physical Systems by Combining Software Model...

引用

16th International Conference on Embedded software (EMSOFT)

作者： Bak, Stanley Chaki, Sagar

ISBN: (纸本)9781450344852

Cyber-physical systems (CPS) span the communication, computation and control domains. Creating a single, complete, and detailed model of a CPS is not only difficult, but, in terms of verification, probably not useful;current verification algorithms are likely intractable for such allencompassing models. However, specific CPS domains have specialized formal reasoning methods that can successfully analyze certain aspects of the integrated system. To prove overall system correctness, however, care must be taken to ensure the interfaces of the proofs are consistent and leave no gaps, which can be difficult since they may use different model types and describe different aspects of the CPS. This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability. A contract automation (CA) expresses both (1) the restrictions on the interactions between the application and the controller, and (2) the desired system invariants. A sound assume-guarantee style compositional proof rule decomposes the verification into two parts - one verifies the application against the CA using software model checking, and another verifies the controller against the CA using hybrid systems reachability analysis. In this way, the proposed method avoids state-space explosion due to the composition of discrete (application) and continuous (controller) behavior, and can leverage verification tools specialized for each domain. The power of the approach is demonstrated by verifying collision avoidance using models of a distributed group of communicating quadcopters, where the provided models are software code and continuous 2-d quadcopter dynamics.

关键词： verification cyber-physical systems compositionality assume-guarantee hybrid systems software model checking

来源：评论

学校读者我要写书评

暂无评论

On-the-Fly Decomposition of Specifications in software model checking 24

On-the-Fly Decomposition of Specifications in Software Model...

引用

24th ACM SIGSOFT International Symposium on Foundations of software Engineering (FSE)

作者： Apel, Sven Beyer, Dirk Mordan, Vitaly Mutilin, Vadim Stahlbauer, Andreas Univ Passau Passau Germany Ludwig Maximilians Univ Munchen Munich Germany ISP RAS Moscow Russia

ISBN: (纸本)9781450342186

Major breakthroughs have increased the efficiency and effectiveness of software model checking considerably, such that this technology is now applicable to industrial-scale software. However, verifying the full formal specification of a software system is still considered too complex, and in practice, sets of properties are verified one by one in isolation. We propose an approach that takes the full formal specification as input and first tries to verify all properties simultaneously in one run of the verifier. Our verification algorithm monitors itself and detects situations for which the full set of properties is too complex. In such cases, we perform an automatic decomposition of the full set of properties into smaller sets, and continue the verification seamlessly. To avoid state-space explosion for large sets of properties, we introduce on-the-fly property weaving : properties get weaved into the program's transition system on the fly, during the analysis;which properties to weave and verify is determined dynamically during the verification process. We perform an extensive evaluation based on verification tasks that were derived from 4 336 Linux kernel modules, and a set of properties that define the correct usage of the Linux API. checking several properties simultaneously can lead to a significant performance gain, due to the fact that abstract models share many parts among different properties.

关键词： software model checking Program Analysis Multi-Property Verification Specification Formal Methods Decomposition

来源：评论

学校读者我要写书评

暂无评论

Reducing State Explosion for software model checking with Relaxed Memory Consistency models 1

引用

2nd International Symposium on Dependable software Engineering - Theories, Tools and Applications (SETTA)

作者： Abe, Tatsuya Ugawa, Tomoharu Maeda, Toshiyuki Matsumoto, Kousuke Chiba Inst Technol STAIR Lab Narashino Chiba Japan Kochi Univ Technol Kami Japan

ISBN: (数字)9783319476773

ISBN: (纸本)9783319476773;9783319476766

software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.

关键词： software model checking Relaxed memory consistency models State explosion Reordering of instructions Integration of states Concurrent copying garbage collection

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：