Verification of Boolean programs with unbounded thread creation

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S. K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol. 1885, Springer, 2000, pp. 113–130] are the most popular representation for these abstractions. Unfortunately, today’s symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in Boolean programs with unbounded thread creation is undecidable. We address this limitation with a novel algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. Although the Boolean programs are not of finite state, the algorithm always reaches a fix-point. The fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite.

Authors

• Byron Cook
• Daniel Kroening
• Natasha Sharygina

Keywords

• Program verification
• Model checking
• Boolean programs
• Reachability