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

model checking Linear Programs with Arrays

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第3期144卷 79-94页

作者： Armando, Alessandro Benerecetti, Massimo Mantovani, Jacopo Univ Genoa DIST AI Lab Genoa Italy Univ Naples Federico II Dipartimento Sci Fis Naples Italy

In previous work we proposed Linear Programs as a fine grained model for imperative programs, and showed how the model checking procedure used in SLAM can be generalised to a model checking procedure for Linear Programs. In this paper we show that our model checking procedure for linear programs can be extended in such a way to support the analysis of linear programs featuring a symbol for undefined values and conditional expressions. This extension is particularly important as it paves the way to the construction of model checking procedures for wider classes of imperative programs such as, e.g., linear programs with arrays. We provide a detailed account of a symbolic model checking procedure for this extended class of linear programs, discuss its implementation in the eureka tool, and present experimental results that confirm its effectiveness in the analysis of linear programs with arrays.

关键词： software model checking Linear Constraints Arrays Linear Arithmetic Decision Procedures

来源：评论

学校读者我要写书评

暂无评论

Dynamic partial-order reduction for model checking software 05

Dynamic partial-order reduction for model checking software

引用

32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Flanagan, C Godefroid, P Univ Calif Santa Cruz Santa Cruz CA 95064 USA

ISBN: (纸本)9781581138306

We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless.

关键词： algorithms verification reliability partial-order reduction software model checking

来源：评论

学校读者我要写书评

暂无评论

Transition predicate abstraction and fair termination 05

Transition predicate abstraction and fair termination

引用

32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Podelski, A Rybalchenko, A Max Planck Inst Informat Saarbrucken Germany

ISBN: (纸本)9781581138306

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 (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.

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

来源：评论

学校读者我要写书评

暂无评论

Formal verification of software source code through semi-automatic modeling

引用

software and Systems modeling 2005年第1期4卷 14-31页

作者： Eisner, Cindy IBM Haifa Research Laboratory Mount Carmel Haifa 31905 Haifa University Campus Israel

We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C cod... 详细信息

关键词： Functional verification Program verification software model checking software verification

来源：评论

学校读者我要写书评

暂无评论

Dynamic component substitutability analysis

引用

13th International Symposium of Formal Methods Europe

作者： Sharygina, N Chaki, S Clarke, E Sinha, N Carnegie Mellon Univ Pittsburgh PA 15213 USA

ISBN: (纸本)3540278826

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: 1) a technique based on simultaneous use of over and under approximations obtained via existential and universal abstractions;2) a dynamic assume-guarantee reasoning algorithm-previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the COMFORT model checking tool set and we report encouraging results on an industrial benchmark.

关键词： software model checking verification of evolving software learning regular sets assume/guarantee reasoning

来源：评论

学校读者我要写书评

暂无评论

Polymorphic predicate abstraction

引用

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2005年第2期27卷 314-343页

作者： Ball, T Millstein, T Rajamani, SK Microsoft Corp Redmond WA 98052 USA Univ Calif Los Angeles Dept Comp Sci Los Angeles CA 90095 USA

Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. We show how polymorphism, a well-known concept in programming languages and program analysis, can be incorporated in a predicate abstraction algorithm for C programs. The use of polymorphism in predicates, via the introduction of symbolic names for values, allows us to model the effect of a procedure independent of its calling contexts. Therefore, we can safely and precisely abstract a procedure once and then reuse this abstraction across multiple calls and multiple applications containing the procedure. Polymorphism also enables us to handle programs that need to be analyzed in an open environment, for all possible callers. We have proved that our algorithm is sound and have implemented it in the C2BP tool as part of the SLAM software model checking toolkit.

关键词： algorithms reliability verification software model checking predicate abstraction polymorphism

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Race checking by context inference

Race checking by context inference

引用

Conference on Programming Language Design and Implementation

作者： Henzinger, TA Jhala, R Majumdar, R Univ Calif Berkeley EECS Dept Berkeley CA 94720 USA Univ Calif Berkeley CS Dept Berkeley CA 94720 USA

software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives.

关键词： languages verification reliability software model checking race conditions

来源：评论

学校读者我要写书评

暂无评论

Abstractions from proofs 04

Abstractions from proofs

引用

31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Henzinger, TA Jhala, R Majumdar, R McMillan, KL Univ Calif Berkeley Dept EECS Berkeley CA 94720 USA Cadence Berkeley Labs Berkeley CA USA

ISBN: (纸本)9781581137293

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 refining 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 can 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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：