Revisiting Underapproximate Reachability for
Multipushdown Systems
S. Akshay
1 , Paul Gastin
2 , S Krishna
1 , and Sparsa Roychowdhury
1
1 IIT Bombay, Mumbai, India
2 ENS Paris-Saclay, Paris, France
Abstract 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 BHIM
and illustrate its applicability by generating a set of relevant benchmarks
and examining its performance. As an additional takeaway BHIM 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 multipushdown automata with closed guards.
Keywords: Multipushdown Systems · Underapproximate Reachability
· Timed pushdown automata.
1 Introduction
The reachability problem for pushdown systems with multiple stacks is known
to be undecidable. However, multi-stack pushdown automata (MPDA hereafter)
represent a theoretically concise and analytically useful model of multi-threaded
recursive programs with shared memory. As a result, several previous works
in the literature have proposed different under-approximate classes of behaviors of MPDA that can be analyzed effectively, such as Round Bounded, Scope
Bounded, Context Bounded and Phase Bounded [18,19,27,14,20,28]. From a practical point of view, these underapproximations have led to efficient tools including, GetaFix [21], SPADE [23]. It has also been argued (e.g., see [24]) that such
bounded underapproximations suffice to find several bugs in practice. In many
such tools efficient fix-point techniques are used to speed-up computations.
We extend known fix-point based approaches by developing a new algorithm that can handle a larger class of bounded underapproximations than
the well-known bounded context and bounded scope underapproximations for
Partly supported by UMI ReLaX, DST/CEFIPRA/INRIA project EQuaVe & TCS.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 387–404, 2020.
https://doi.org/10.1007/978-3-030-45190-5 21
TACAS
Evaluation
Artifact
2020
Accepted
Multipushdown Systems
S. Akshay
1 , Paul Gastin
2 , S Krishna
1 , and Sparsa Roychowdhury
1
1 IIT Bombay, Mumbai, India
2 ENS Paris-Saclay, Paris, France
Abstract 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 BHIM
and illustrate its applicability by generating a set of relevant benchmarks
and examining its performance. As an additional takeaway BHIM 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 multipushdown automata with closed guards.
Keywords: Multipushdown Systems · Underapproximate Reachability
· Timed pushdown automata.
1 Introduction
The reachability problem for pushdown systems with multiple stacks is known
to be undecidable. However, multi-stack pushdown automata (MPDA hereafter)
represent a theoretically concise and analytically useful model of multi-threaded
recursive programs with shared memory. As a result, several previous works
in the literature have proposed different under-approximate classes of behaviors of MPDA that can be analyzed effectively, such as Round Bounded, Scope
Bounded, Context Bounded and Phase Bounded [18,19,27,14,20,28]. From a practical point of view, these underapproximations have led to efficient tools including, GetaFix [21], SPADE [23]. It has also been argued (e.g., see [24]) that such
bounded underapproximations suffice to find several bugs in practice. In many
such tools efficient fix-point techniques are used to speed-up computations.
We extend known fix-point based approaches by developing a new algorithm that can handle a larger class of bounded underapproximations than
the well-known bounded context and bounded scope underapproximations for
Partly supported by UMI ReLaX, DST/CEFIPRA/INRIA project EQuaVe & TCS.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 387–404, 2020.
https://doi.org/10.1007/978-3-030-45190-5 21
TACAS
Evaluation
Artifact
2020
Accepted