This paper describes a symbolic algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. The fix-point is detected by projecting the state of the threads to the globally visible parts, which are finite. Our algorithm models recursion by over-approximating the call stack that contains the return locations of recursive function calls, as reachability is undecidable in this case. The algorithm may obtain spurious counterexamples, which are removed iteratively by means of an abstraction refinement loop. Experiments show that the symbolic algorithm for unbounded thread creation scales to large abstract models.
展开▼
