Revisiting Underapproximate Reachability for Multipushdown Systems
Résumé
Boolean programs with multiple recursive threads can be captured as
pushdown automata with multiple stacks. This model is Turing complete, and
hence, one is often interested in analyzing a restricted class that still
captures useful behaviors. In this paper, we propose a new class of bounded
underapproximations for multi-pushdown systems, which subsumes most existing
classes. We develop an efficient algorithm for solving the under-approximate
reachability problem, which is based on efficient fix-point computations. We
implement it in our tool \trim{} and illustrate its applicability by
generating a set of relevant benchmarks and examining its performance. As an
additional takeaway \trim{} solves the binary reachability problem in pushdown
automata. To show the versatility of our approach, we then extend our
algorithm to the timed setting and provide the first implementation that can
handle timed multi-pushdown automata with closed guards.