Software Model Checking via Large-Block Encoding

Details Software Model Checking via Large-Block Encoding Software Model Checking via Large-Block Encoding

2009-04-29

arxiv.org/abs/0904.4709v1

Computer Science

Software Engineering

13 pages (11 without cover), 4 figures, 5 tables

Scientific paper

The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.

Affiliated with

Also associated with

No associations

Rating

Software Model Checking via Large-Block Encoding does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Software Model Checking via Large-Block Encoding, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Software Model Checking via Large-Block Encoding will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-442427