Predicate Abstraction with Block Abstraction Memoization∗

Abstract. Predicate abstraction is an established technique for reduc-ing the size of the state space during verification. In this paper, we ex-tend predication abstraction with block abstraction memoization (ABM), which exploits the fact that blocks are often executed several times in a program. The verification can thus benefit from caching the values of previous block analysis ’ and reusing them upon next entry into a block. In addition to function bodies, ABM also pays off well for nested loops. To further increase effectiveness, block memoization has been in-tegrated with lazy abstraction adopting a lazy strategy for cache re-finement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis tool CPAchecker) has won the Competition on Software Verification 201