论文标题
重新访问多峰系统的不适当可达性
Revisiting Underapproximate Reachability for Multipushdown Systems
论文作者
论文摘要
带有多个递归线程的布尔程序可以作为带有多个堆栈的下降自动机捕获。该模型已经完成了，因此，人们通常有兴趣分析仍然可以捕获有用行为的限制类。在本文中，我们提出了一类新的界限，在多孔系统的近似值下，该类别包含大多数现有类。我们开发了一种有效的算法，用于解决较低的可及性问题，该问题基于有效的固定点计算。我们在工具BHIM中实现它，并通过生成一组相关基准并检查其性能来说明其适用性。作为额外的外卖，Bhim解决了下降自动机中的二进制可及性问题。为了显示我们的方法的多功能性，然后我们将算法扩展到定时设置，并提供第一个可以使用封闭防护装置来处理定时的多点式自动机的实现。
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 under approximations 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 multi-pushdown automata with closed guards.
