Decomposing Image Computation for Symbolic Reachability Analysis Using Control Flow Information

The main challenge in BDD-based symbolic reachability analysis is represented by the sizes of the intermediate decision diagrams obtained during image computations. Methods proposed to mitigate this problem fall broadly into two categories: Search strategies that depart from breadth-first search, and efficient techniques for image computation. In this paper we present an algorithm that belongs to the latter category. It exploits define-use information along executable paths extracted from the control-flow graph of the model being analyzed; this information enables an effective constraining of the transition relation and a decomposition of the image computation process that often leads to much smaller intermediate BDDs. Our experiments confirm that this reduction in the size of the representation of state sets translates in significant decreases in CPU and memory requirements