Adjustable-Block Encoding: Towards a Unified Framework for Software Verification
- 11:30 14th October 2010 ( week 1, Michaelmas Term 2010 )Room 147, Oxford University Computing Laboratory
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. Adjustable-block encoding (ABE) is implemented as a configurable program analysis (CPA) in the verification framework CPAchecker.