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

Scalable and scope-bounded software verification in VARVEL

AUTOMATED software ENGINEERING 2015年第4期22卷 517-559页

作者： Ivancic, Franjo Balakrishnan, Gogul Gupta, Aarti Sankaranarayanan, Sriram Maeda, Naoto Imoto, Takashi Pothengil, Rakesh Hussain, Mustafa NEC Labs Amer Princeton NJ 08540 USA Univ Colorado Boulder CO 80309 USA NEC Corp Ltd Kawasaki Kanagawa Japan NEC Technol India Noida UP India

software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply in industry practice. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to address the issue of scalability, while retaining enough precision to avoid false alarms in practice. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions;(b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope;and (c) automatic refinement of pre- and post-conditions using counterexamples that are deemed to be false alarms by a user. The techniques enable DC2 to perform iterative reasoning over the calling environment of functions, to find non-trivial bugs and fewer false alarms. Based on the DC2 framework, we have developed a software model checking tool for C/C++ programs called Varvel, which has been in industrial use at NEC for a number of years. In addition to DC2, we describe other scalability and usability improvements in Varvel that have enabled its successful application on numerous large software projects. These include model simplifications, support for witness understanding to improve debugging assistance, and handling of C++ programs. We present experimental evaluations that demonstrate the effectiveness of DC2 and report on the usage of Varvel in NEC.

关键词： software model checking Program analysis Abstract interpretation Scope bounding Bug detection Witness presentation

来源：评论

学校读者我要写书评

暂无评论

Effective Stateless model checking for C/C++ Concurrency

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2018年第POPL期2卷 1-32页

作者： Kokologiannakis, Michalis Lahav, Ori Sagonas, Konstantinos Vafeiadis, Viktor Natl Tech Univ Athens Athens Greece Tel Aviv Univ Tel Aviv Israel Uppsala Univ Uppsala Sweden Max Planck Inst Software Syst MPI SWS Saarbrucken Germany

We present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C/C++11 memory model without dependency cycles. Unlike most previous approaches, which enumerate thread interleavings up to sonic partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and applied it to a number of challenging concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools, and is also more resilient to small changes in the benchmarks.

关键词： software model checking weak memory models C/C++11 RC11

来源：评论

学校读者我要写书评

暂无评论

MMC: the Mono model Checker

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期190卷 149-160页

作者： Ruys, Theo C. Aan de Brugh, Niels H. M. Univ Twente Fac EEMCS Formal Methods & Tools Grp Enschede Netherlands

The Mono model Checker (MMC) is a software model checker for CIL bytecode programs. MMC has been developed on the Mono platform. MMC is able to detect deadlocks and assertion violations in CIL programs. The design of MMC is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MMC is comparable to JPF. This paper introduces MMC and presents its main architectural characteristics.

关键词： software model checking verification MMC MONO,. NET CLI bytecode

来源：评论

学校读者我要写书评

暂无评论

Optimal Stateless model checking under the Release-Acquire Semantics

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2018年第OOPSLA期2卷 1–29页

作者： Abdulla, Parosh Aziz Atig, Mohamed Faouzi Jonsson, Bengt Tuan Phong Ngo Uppsala Univ Uppsala Sweden

We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially significant source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool TRACER. Experiments show that TRACER can be significantly faster than state-of-the-art tools that can handle the RA semantics.

关键词： software model checking weak memory models C/C++11 Release-Acquire

来源：评论

学校读者我要写书评

暂无评论

Introductory paper

引用

International Journal on software Tools for Technology Transfer 2004年第4期6卷 257-259页

作者： Dwyer, Matthew Leue, Stefan Department of Computer Science and Engineering University of Nebraska 256 Avery Hall Lincoln NE 68588-0115 United States Department of Computer and Information Science University of Konstanz 78457 Konstanz Germany

来源：评论

学校读者我要写书评

暂无评论

Design and implementation of a fine-grained software inspection tool

引用

IEEE TRANSACTIONS ON software ENGINEERING 2003年第8期29卷 721-733页

作者： Anderson, P Reps, T Teitelbaum, T GammaTech Inc Ithaca NY 14850 USA Univ Wisconsin GammaTech Inc Madison WI 53706 USA Univ Wisconsin Dept Comp Sci Madison WI 53706 USA Cornell Univ Dept Comp Sci Ithaca NY 14850 USA

Although software inspection has led to improvements in software quality, many software systems continue to be deployed with unacceptable numbers of errors, even when software inspection is part of the development process. The difficulty of manually verifying that the software under inspection conforms to the rules is partly to blame. We describe the design and implementation of a tool designed to help alleviate this problem. The tool provides mechanisms for fine-grained inspection of software by exposing the results of sophisticated whole-program static analysis to the inspector. The tool computes many static-semantic representations of the program, including an accurate call graph and dependence graph. Whole-program pointer analysis is used to make sure that the representation is precise with respect to aliases induced by pointer usage. Views on the dependence graph and related representations are supported. Queries on the dependence graph allow an inspector to answer detailed questions about the semantics of the program. Facilities for openness and extensibility permit the tool to be integrated with many software-development processes. The main challenge of the approach is to provide facilities to navigate and manage the enormous complexity of the dependence graph.

关键词： software inspection dependence graphs program understanding slicing chopping software model checking

来源：评论

学校读者我要写书评

暂无评论

Transition predicate abstraction and fair termination

引用

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2007年第3期29卷 1.1-1.31页

作者： Podelski, Andreas Rybalchenko, Andrey Max Planck Inst Informat Saarbrucken Germany Ecole Polytech Fed Lausanne Max Planck Inst Informat Saarbrucken Germany

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to transition predicate abstraction. Transition predicate abstraction goes beyond the idea of finite abstract-state programs (and checking the absence of loops). Instead, our abstraction algorithm transforms a program into a finite abstract-transition program. Then a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (impartiality;justice, and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties.

关键词： software model checking transition predicate abstraction fair termination liveness

来源：评论

学校读者我要写书评

暂无评论

A model-extraction approach to verifying concurrent C programs with CADP

引用

SCIENCE OF COMPUTER PROGRAMMING 2012年第3期77卷 375-392页

作者： Gallardo, M. M. Joubert, C. Merino, P. Sanan, D. Univ Politecn Valencia Valencia Spain Univ Malaga E-29071 Malaga Spain

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account;(2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system;(3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs. Published by Elsevier B.V.

关键词： software model checking Data flow analysis Labeled transition system Boolean equation system CADP verification toolbox

来源：评论

学校读者我要写书评

暂无评论

Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs

引用

FORMAL METHODS IN SYSTEM DESIGN 2004年第2-3期25卷 199-240页

作者： Dwyer, MB Hatcliff, J Robby Ranganath, VP Kansas State Univ Dept Comp & Informat Sci Manhattan KS 66506 USA

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored ( and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on ( a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program ( building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL-X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.

关键词： software model checking software verifcation partial order reduction escape analysis locking discipline

来源：评论

学校读者我要写书评

暂无评论

Cache-based model checking of Networked Applications: From Linear to Branching Time 09

Cache-based Model Checking of Networked Applications: From L...

引用

24th IEEE/ACM International Conference on Automated software Engineering

作者： Artho, Cyrille Leungwattanakit, Watcharin Hagiya, Masami Tanabe, Yoshinori Yamamoto, Mitsuharu AIST Res Ctr Informat Secur Tokyo Japan Univ Tokyo Dept Comp Sci Tokyo Japan Chiba Univ Dept Math & Informat Chiba Japan

ISBN: (纸本)9780769538914

Many applications are concurrent and communicate over a network. The non-determinism in the thread and communication schedules makes it desirable to model check such systems. However, a simple state space exploration scheme is not applicable, as backtracking results in repeated communication operations. A cache-based approach solves this problem by hiding redundant communication operations from the environment. In this work, we propose a change from a linear-time to a branching-time cache, allowing us to relax restrictions in previous work regarding communication traces that differ between schedules. We successfully applied the new algorithm to real-life programs where a previous solution is not applicable.

关键词： software model checking software verification networking input/output caching

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：