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

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

来源：评论

学校读者我要写书评

暂无评论

Semantics-based generation of verification conditions by program specialization 15

Semantics-based generation of verification conditions by pro...

引用

17th International Symposium on Principles and Practice of Declarative Programming (PPDP)

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G dAnnunzio DEC Chieti Italy Univ Roma Tor Vergata DICII Rome Italy CNR IASI Rome Italy

ISBN: (纸本)9781450335164

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it specializes, by using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics. We define a multi-step operational semantics for a fragment of the C language and compare the verification conditions obtained by using this semantics with those obtained by using a more traditional small-step semantics. The flexibility of the approach is further demonstrated by showing that it is possible to easily take into account alternative operational semantics definitions for modeling new language features. Finally, we provide an experimental evaluation of the method by generating verification conditions using the multi-step and the small-step semantics for a few hundreds of programs taken from various publicly available benchmarks, and by checking the satisfiability of these verification conditions by using state-of-the-art Horn clause solvers. These experiments show that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice.

关键词： software model checking program verification program specialization semantics of programming languages verification conditions constraint logic programming Horn clauses

来源：评论

学校读者我要写书评

暂无评论

Polyhedra to the rescue of array interpolants 15

Polyhedra to the rescue of array interpolants

引用

30th ACM Symposium on Applied Computing (SAC)

作者： Alberti, Francesco Monniaux, David Univ Lugano Via G Buffi 13 CH-6900 Lugano Switzerland Univ Grenoble Alpes VERIMAG F-38000 Grenoble France CNRS VERIMAG F-38000 Grenoble France

ISBN: (纸本)9781450331968

We propose a new approach to the automated verification of the correctness of programs handling arrays. An abstract interpreter supplies auxiliary numeric invariants to an interpolation-based refinement procedure suited to array programs. Experiments show that this combination approach, implemented in an enhanced version of the BOOSTER software model-checker, performs better than the pure interpolation-based approach, at no additional cost.

关键词： software model checking Quantified invariants Arrays Abstract Interpretation

来源：评论

学校读者我要写书评

暂无评论

Cardinality of UDP Transmission Outcomes 1st

Cardinality of UDP Transmission Outcomes

引用

1st International Symposium on Dependable software Engineering - Theories, Tools and Applications (SETTA)

作者： Weitl, Franz Sebih, Nazim Artho, Cyrille Hagiya, Masami Tanabe, Yoshinori Yamagata, Yoriyuki Yamamoto, Mitsuharu Chiba Univ Chiba Japan AIST RISEC Amagasaki Hyogo Japan Univ Tokyo Tokyo Japan Tsurumi Univ Yokohama Kanagawa Japan

ISBN: (纸本)9783319259420;9783319259413

This paper examines the cost of testing network applications using the User Datagram Protocol (UDP). Such applications must deal with packet loss, duplication, and reordering. Ideally, a UDP application should be tested against all possible outcomes of unreliable UDP transmissions. Their number, however, grows at least exponentially in the number of transmitted packets. To estimate the cost of the exhaustive testing of UDP applications, we determine the number of UDP transmission outcomes analytically. Based on this combinatorial analysis, we derive a sound, complete, and optimal algorithm for generating outcomes of unreliable UDP transmissions. The algorithm is implemented in the net-iocache extension of the software model checker Java Pathfinder (JPF). Experimental results confirm the consistency of the implementation with the analytical results. In addition, we found that JPF's state matching reduces the explored state space significantly and ensures the practicability of the approach despite of its exponential complexity.

关键词： User datagram protocol software model checking Java Pathfinder Combinatorial analysis

来源：评论

学校读者我要写书评

暂无评论

Towards automated software model checking using graph transformation systems and Bogor

引用

Journal of Zhejiang University-Science A(Applied Physics & Engineering) 2009年第8期10卷 1093-1105页

作者： Vahid RAFE Adel T.RAHMANI Department of Computer Engineering Iran University of Science and Technology

Graph transformation systems have become a general formal modeling language to describe many models in software development *** modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software *** even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their *** this paper,we present a new solution to verify graph transformation systems using the Bogor model *** attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph *** results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.

关键词： Graph transformation Verification Bogor Attributed graph grammars （AGG） software model checking

来源：评论

学校读者我要写书评

暂无评论

Towards automatic software model checking of thousands of Linux modules-a case study with Avinux

引用

software TESTING VERIFICATION & RELIABILITY 2009年第2期19卷 155-172页

作者： Post, Hendrik Sinz, Carsten Kuechlin, Wolfgang Univ Tubingen Symbol Computat Grp Tubingen Germany

Modular software model checking of large real-world systems is known to require extensive manual effort in environment modelling and preparing source code for model checking. Avinux is a tool chain that facilitates the automatic analysis of Linux and especially of Linux device drivers. The tool chain is implemented as a plugin for the Eclipse IDE, using the source code bounded model checker CBMC as its backend. Avinux supports a verification process for Linux that is built upon specification annotations with SLICx (an extension of the SLIC language), automatic data environment creation, source code transformation and simplification, and the invocation of the verification backend. In this paper technical details of the verification process are presented: Using Avinux on thousands of drivers from various Linux versions led to the discovery of six new errors. In these experiments, Avinux also reduced the immense overhead of manual code preprocessing that other projects incurred. Copyright (C) 2008 John Wiley & Sons, Ltd.

关键词： software model checking integration and application of formal methods operating systems software verification model checking case study

来源：评论

学校读者我要写书评

暂无评论

Program verification via iterated specialization

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年第Part2期95卷 149-175页

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G DAnnunzio DEC I-65127 Pescara Italy Univ Roma Tor Vergata DICII I-00133 Rome Italy CNR IASI I-00185 Rome Italy

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of imperative programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from any initial configuration. We introduce a CLP program I that encodes the interpreter of the language and defines a predicate unsafe equivalent to the negation of the safety property to be verified. Then, we specialize the CLP program I with respect to the given imperative program and the given initial and error configurations, with the objective of deriving a new CLP program I-sp that either contains the fact unsafe (and in this case the imperative program is proved unsafe) or contains no clauses with head unsafe (and in this case the imperative program is proved safe). If Isp enjoys neither of these properties, we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating information (either propagating forward from an initial configuration to an error configuration, or propagating backward from an error configuration to an initial configuration) and different operators (such as the widening and the convex hull operators) for generalizing predicate definitions. Each specialization step is guaranteed to terminate, but due to the undecidability of program safety, the iterated specialization process may not terminate. By an experimental evaluation carried out on a significant set of examples taken from the literature, we show that our method improves the precision of program verification with respect to state-of-the-art software model checkers. (C) 2014 Elsevier B.V. All rights reserved.

关键词： software model checking Constraint logic programming Program specialization Program transformation

来源：评论

学校读者我要写书评

暂无评论

BDD-based software verification Applications to event-condition-action systems

引用

INTERNATIONAL JOURNAL ON software TOOLS FOR TECHNOLOGY TRANSFER 2014年第5期16卷 507-518页

作者： Beyer, Dirk Stahlbauer, Andreas Univ Passau D-94032 Passau Germany

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space;BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable's domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.

关键词： Binary decision diagram BDD Symbolic model checking software model checking Program analysis Event-condition-action system RERS challenge Configurable software verification CPA

来源：评论

学校读者我要写书评

暂无评论

Abstractions from Proofs

引用

ACM SIGPLAN NOTICES 2014年第4期49卷 79-91页

作者： Henzinger, Thomas A. Jhala, Ranjit Majumdar, Rupak McMillan, Kenneth L. Univ Calif Berkeley Dept EECS Berkeley CA 94720 USA Cadence Berkeley Labs Berkeley CA USA

The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically relining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace, At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location, It cart be found by a linear scan of the proof of infeasibility of the trace. We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker BLAST with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions.

关键词： software model checking predicate abstraction counterexample analysis

来源：评论

学校读者我要写书评

暂无评论

Optimal Dynamic Partial Order Reduction 14

Optimal Dynamic Partial Order Reduction

引用

41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

作者： Abdulla, Parosh Aronis, Stavros Jonsson, Bengt Sagonas, Konstantinos Uppsala Univ Dept Informat Technol Uppsala Sweden

ISBN: (纸本)9781450325448

Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.

关键词： dynamic partial oder reduction software model checking systematic testing concurrency source sets wakeup trees

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：