## Efficient Predicate Abstraction of Program Summaries

**Arie Gurfinkel, Sagar Chaki, Samir
Sapra,** *Proceedings of the 3rd NASA Formal
Methods Symposium
(NFM),
page 131-145, April 18-20, 2011.*

**Abstract:** Predicate abstraction is an
effective technique for scaling Software Model
Checking to real programs. Traditionally, predicate
abstraction abstracts each basic block of a program P
to construct a small finite abstract model -- a
Boolean program BP, whose state-transition relation is
over some chosen (finite) set of predicates. This is
called Small-Block Encoding (SBE). A recent
advancement is Large-Block Encoding (LBE) where
abstraction is applied to a ``summarized'' program so
that the abstract transitions of BP correspond to
loop-free fragments of P. In this paper, we expand on
the original notion of LBE to promote flexibility. We
explore and describe efficient ways to perform CEGAR
bottleneck operations: generating and solving
predicate abstraction queries (PAQs). We make the
following contributions. First, we define a general
notion of program summarization based on loop cutsets.
Second, we give a linear time algorithm to construct
PAQs for a loop-free fragment of a program. Third, we
compare two approaches to solving PAQs: a classical
AllSAT-based one, and a new one based on Linear
Decision Diagrams (LDDs). The approaches are evaluated
on a large benchmark from open-source software. Our
results show that the new LDD-based approach
significantly outperforms (and complements) the AllSAT
one.