Software Model Checking Via Large-Block Encoding

Date Added: Apr 2009
Format: PDF

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, the authors 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. They propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; they call this approach Large-Block Encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially.