Predicate Abstraction
with Adjustable-Block Encoding
Dirk Beyer, M. Erkan Keremoglu,
and Philipp Wendler
Submitted to FMCAD 2010.
Abstract:
Several
successful software model checkers are based on a technique called
single-block encoding (SBE), which computes costly predicate
abstractions after every single program operation. Large-block encoding
(LBE) computes abstractions only after a large number of operations,
and it was shown that this significantly improved the verification
performance. In this work, we present adjustable-block encoding, a
unifying framework that allows to express both previous approaches. In
addition, it provides the flexibility to specify any block size between
SBE and LBE, and also beyond LBE, through the adjustment of several
parameters. Such a unification of different concepts makes it easier to
understand the fundamental properties of the analysis, and makes the
differences of the variants more explicit. We evaluate different
configurations on example C programs, in order to identify one that is
generally the fastest.
Download tarball including executable program,
benchmark programs, and source code of our ABE implementation.