PaperlayerView exact revision on arXiv

Source-linked AI summary

Software Model Checking via Large-Block Encoding

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani

arXiv:0904.4709v1cs.SEcs.PL

TL;DR

Software model checking based on ARTs can suffer from huge numbers of independently explored paths under single-block encoding. The paper introduces large-block encoding with richer predicate abstractions and symbolic SMT-based successor computation, and experiments report that LBE outperforms SBE and BLAST on the evaluated benchmarks.

  • Problem

    Single-block encoding can induce huge numbers of ART paths and nodes that are explored independently, creating an efficiency and scalability concern for software model checking.

  • Method

    Large-block encoding represents larger program fragments in ART transitions and combines this with Boolean predicate abstraction and SMT-based symbolic successor computation.

  • Results

    Experiments show that LBE outperforms SBE on correct and defective programs and outperforms the evaluated BLAST configurations.

  • Takeaways & Limitations

    LBE trades many explicit program-path enumerations for more involved symbolic successor computations and yields significantly smaller ARTs.

Abstract

from arXiv · show

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.

I. Introduction

Traditional single-block encoding can generate huge numbers of independently explored ART paths, limiting efficiency and scalability. Large-block encoding summarizes larger program portions in single ART edges, potentially reducing paths and successor computations exponentially while requiring richer abstractions and symbolic SMT reasoning.

  • Motivation: SBE represents each program operation as a separate ART edge, so control flow can induce huge numbers of independently explored paths and nodes.This creates a fundamental source of inefficiency in ART-based verification.
  • Large-block encoding: LBE encodes entire program portions in one edge, producing a more compact abstract space and potentially an exponential reduction in ART nodes.The approach replaces explicit enumeration of many paths with larger symbolic transitions.
  • Abstraction tradeoffs: LBE requires arbitrary Boolean combinations of predicates because conjunctions are insufficient for abstract states summarizing large control-flow portions.The generalization from SBE to LBE therefore changes both state representation and successor abstraction requirements.
  • Implementation: The approach relies on SMT solvers for efficient Boolean reasoning, abstraction computation, and interpolation-based predicate extraction.These capabilities support symbolic computation of abstract large-block successors.
  • Abstraction tradeoffs: LBE reduces successor computations dramatically, possibly exponentially, whereas Boolean abstraction is more expensive because it enumerates satisfiable predicate assignments.This creates a tradeoff between fewer symbolic successor computations and more expensive abstraction computation.
  • Evaluation: The work evaluates LBE experimentally and reports that its implementation outperforms the previous approach, with comparisons involving BLAST and SBE.The paper positions LBE within lazy abstraction and contrasts it with established model-checking approaches.

A. Programs and Control-Flow Automata

The paper models programs as control-flow automata with locations, operations, variables, and designated entry and error locations. Concrete execution is represented by integer-valued states and strongest-postcondition semantics over paths.

  • Program model: The presentation restricts programs to assignments and assume operations over integer-valued variables.The implementation is based on CPACHECKER and supports C programs in the CIL intermediate language.
  • Control-flow automata: A control-flow automaton consists of program locations and labeled edges whose operations execute when control flows between locations.A program additionally designates an initial location and an error location.
  • Concrete semantics: A concrete data state assigns an integer value to every program variable, and a formula represents a set of such assignments.Concrete program states pair a control-flow location with a concrete data state.
  • Concrete semantics: The semantics of a program path is the successive application of strongest-postcondition operators for its operations.A program path is a syntactical walk through the control-flow automaton.

B. Predicate Abstraction

Predicate abstraction represents concrete regions with formulas over a finite predicate precision. Cartesian abstraction keeps entailed conjunctions, whereas Boolean abstraction preserves arbitrary satisfiable combinations and is more expensive to compute.

  • Predicate abstractions: A precision is a finite subset of predicates drawn from a quantifier-free theory over program variables.Predicate abstraction uses selected predicates to represent regions of concrete program states.
  • Cartesian abstraction: Cartesian predicate abstraction is the strongest conjunction of predicates from the precision entailed by the concrete formula.It can be computed using one SMT-solver query per predicate.
  • Tradeoff: Cartesian abstraction is cheaper to compute, while Boolean abstraction is more precise but requires enumeration of satisfiable predicate assignments.This cost difference motivates using Cartesian abstraction in traditional SBE implementations and investigating Boolean abstraction with LBE.
  • Boolean abstraction: Boolean predicate abstraction is the strongest Boolean combination of predicates from the precision entailed by the concrete formula.It enumerates satisfying assignments of propositional variables linked to the predicates, then forms a disjunction of corresponding conjunctions.

C. ART-based Software Model Checking with SBE

ART-based software model checking constructs a tree of abstract states and successor states under a location-dependent precision. Traditional SBE performs one successor computation per program operation and commonly uses coarse Cartesian abstraction for scalability.

  • ART construction: An ART contains nodes labeled with program locations and abstract states, with children generated by strongest-postcondition and predicate-abstraction operations.A complete ART supports correctness checking when it has no error node; an error path is checked for feasibility or infeasibility.
  • ART construction: A location-dependent precision assigns a finite predicate set to each program location and guides construction of the ART.Nodes may be covered when another node at the same location entails them.
  • Single-block encoding: SBE represents each program operation with a single ART edge and therefore performs an abstract-successor computation for every operation.This produces many successor computations as the ART follows individual control-flow steps.
  • Abstraction choice: BLAST and SLAM use Cartesian abstraction because it is simpler and cheaper to compute than Boolean abstraction, despite potential imprecision.The paper states that Cartesian abstraction has nevertheless been successful on many real-world programs.

A. Summarization of Control-Flow Automata

LBE summarizes loop-free control-flow subgraphs into single edges with formulas, using rewriting rules whose result preserves error reachability. The summarization can be computed in polynomial time.

  • CFA summarization: LBE replaces each large loop-free control-flow subgraph with one edge whose formula represents the removed subgraph.This summarization is obtained by repeatedly applying control-flow rewriting rules until none remains applicable.
  • Rewriting rules: Rule 0 makes the error location a sink by removing all outgoing edges from it.
  • Rewriting rules: Rule 1 merges a sequence by removing an intermediate location and composing its operations into one edge.The composed strongest-post operation applies the first operation followed by the subsequent operation.
  • Rewriting rules: Rule 2 merges parallel edges between two locations into one edge representing their disjunction.The resulting strongest-post operation is the disjunction of the two branch results.
  • Correctness and complexity: Error reachability is preserved exactly: the summarized CFA reaches the error location if and only if the original program does.The initial and error locations are retained in the summarized CFA.
  • Correctness and complexity: The summarization runs in polynomial time, with rule applications bounded by the number of CFA edges.The stated rule-selection procedure uses O(|V| · k) time, where k is the maximum location out-degree.

B. LBE versus SBE for Software Model Checking

LBE keeps the ART-based model-checking algorithm but represents larger path sets per edge and abstract state, producing smaller ARTs through more expensive symbolic computations. It uses Boolean representations and SMT capabilities to handle the resulting formulas.

  • Representation: LBE preserves the ART and CEGAR-based model-checking algorithm but removes the one-to-one correspondence between ART paths and syntactical program paths.A single CFA edge can represent multiple program paths, and an ART path can represent a set of program paths.
  • Benefits and costs: LBE can produce exponentially smaller ARTs than SBE, reducing successor computations and refinement steps for infeasible error paths.
  • Benefits and costs: LBE makes individual successor computations more expensive because the formulas are larger and more structurally complex.
  • Symbolic abstraction: LBE represents abstract states with arbitrary Boolean combinations of predicates because one state may cover regions reachable through several paths.
  • Symbolic abstraction: LBE trades explicit path enumeration for symbolic successor computation, using modern SMT solvers for Boolean reasoning, Boolean abstraction, and interpolation-based analysis.These capabilities are especially useful for handling large Boolean combinations and complex formulas.

IV. Performance Evaluation

The evaluation compares LBE with SBE and BLAST on safe and unsafe benchmark programs using controlled implementations and multiple configurations. LBE successfully completed all benchmarks in the reported experiment classes and generally outperformed SBE and BLAST.

  • Benchmark Programs: The benchmark suite includes synthetic programs designed to cause exponential ART growth, BLAST device-driver programs, and SSH client and server verification problems.Experiments also include versions of the second and third benchmark groups with artificial defects.
  • Experimental Configurations: The experiments use BLAST, a CPACHECKER-based SBE implementation, and a CPACHECKER-based LBE implementation for controlled performance comparisons.The SBE and LBE implementations share the same environment, while BLAST is evaluated across search and predicate-discovery configurations.
  • Experimental Configurations: SBE does not benefit from Boolean abstraction, while LBE with Cartesian abstraction fails because of loss of precision; the reported successful configurations are SBE with Cartesian abstraction and LBE with Boolean abstraction.The experiments therefore report the two configurations that successfully completed the relevant cases.
  • Results: SBE and BLAST can exhibit time complexity that grows exponentially with nested conditional statements, while LBE reduces the loop-free branching structure to a few edges and keeps the ART size constant in the tested pattern.LBE runtime increases slightly with program size as the formulas submitted to the SMT solver grow.
  • Results: LBE successfully completes all benchmarks in the two other experiment classes and shows significant performance gains over SBE, which solves only about one third of them.LBE also outperforms every BLAST configuration in the reported Table I comparison and performs best for finding error paths in Table III.
  • Results: Across correct and defective programs, the experiments show that LBE outperforms SBE, with the comparison also including BLAST to address concerns about the SBE implementation.The authors note that BLAST was the result of several years of fine-tuning.

V. Conclusion and Future Work

The paper concludes that LBE is an effective alternative to SBE by representing larger program fragments in ART transitions. It reports smaller ARTs and experimental advantages, while identifying dynamic block sizing and intermediate successor abstractions as future directions.

  • Conclusion: LBE represents larger program fragments in abstract-space transitions and produces significantly smaller ARTs than SBE.The approach trades many explicit program-path enumerations for more involved symbolic successor computations.
  • Conclusion: A thorough evaluation reports advantages of LBE over both the authors’ SBE implementation and the state-of-the-art BLAST system.
  • Future Work: Future work includes implementing interpolation-based lazy abstraction and comparing its SBE and LBE versions.
  • Future Work: The authors plan to construct large blocks on-the-fly with adjustable precision to dynamically tune the amount of work delegated to the SMT solver.
  • Future Work: They also plan to investigate abstract-successor techniques more precise than Cartesian abstraction but less expensive than Boolean abstraction.

A. Proof of Theorem 3.1

The proof establishes the theorem through auxiliary lemmas about how summarizing a control-flow automaton preserves relationships between paths and strongest-postcondition formulas. It then applies these lemmas by induction over summarization rules and path structure.

  • Auxiliary lemmas: The proof introduces auxiliary lemmas to relate paths and strongest-postcondition formulas before proving Theorem 3.1.The lemmas are established for summarized control-flow automata and then used in the theorem proof.
  • Auxiliary lemmas: Lemma A.2 maps a path in the original automaton to a summarized path with the same endpoints and a weaker strongest-postcondition result.For every formula ϕ, the original path's strongest postcondition entails that of the summarized path.
  • Inductive cases: The lemma proofs handle unchanged and rule-generated edges by induction, combining paths when summarization removes locations or merges edges.The construction uses the incoming-edge structure and unions of path sets for alternative rule cases.
  • Auxiliary lemmas: Lemma A.3 expands a summarized path into original paths with the same endpoints whose strongest-postcondition disjunction is equivalent to the summarized path's result.The proof proceeds by induction over the summarization rules and the length of the summarized path.
  • Theorem conclusion: Theorem 3.1 follows from the auxiliary lemmas and the fact that the initial and final locations cannot be removed by the summarization rules.The proof explicitly derives the two directions of the theorem from Lemmas A.2 and A.3.
Loading 0904.4709v1…