Predicate abstraction is an established technique for reducing the size of the state space during verification. In this paper, we extend predication abstraction with block-abstraction memoization (BAM), 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 analyses and reusing them upon next entry into a block. In addition to function bodies, BAM also performs well for nested loops. To further increase effectiveness, block memoization has been integrated with lazy abstraction adopting a lazy strategy for cache refinement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis framework CPAchecker) has won the Competition on Software Verification 2012 in the category "Overall". © 2012 Springer-Verlag.
CITATION STYLE
Wonisch, D., & Wehrheim, H. (2012). Predicate analysis with block-abstraction memoization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7635 LNCS, pp. 332–347). https://doi.org/10.1007/978-3-642-34281-3_24
Mendeley helps you to discover research relevant for your work.