Block Abstraction Memoization for CPAchecker (Competition Contribution)
Daniel Wonisch · 2015
Abstract. Block Abstraction Memoization (ABM) is a technique in software model checking that exploits the modularity of programs dur-ing verification by caching. To this end, ABM records the results of block analyses and reuses them if possible when revisiting the same block again. In this paper we present an implementation of ABM into the predicate-analysis component of the software-verification framework CPAchecker. With our participation at the Competition on Software Verification we aim at providing evidence that ABM can not only sub-stantially increase the efficiency of predicate analysis but also enables verification of a wider range of programs. 1 Verification Approach Currently, software model checking is getting more and more successful and is getting applied to industrial-size programs. Yet, scalability of the applied meth-ods is still an issue. One approach to improve the scalability of model check-ing is block abstraction memoization (ABM). ABM exploits the modularity of