Reachability of Patterned Conditional Pushdown Systems
Reachability of Patterned Conditional Pushdown Systems
复制标题
模式化条件下推系统的可达性
DOI：
10.1007/s11390-020-0541-z
复制
发表时间：
2020-11
影响因子：
0.7
通讯作者：
Hiroyuki Seki
中科院分区：
文献类型：
--
作者：
Xin Li;Patrick Gardy;Yuxin Deng;Hiroyuki Seki
条件下推系统（CPDS）通过将每个转换规则与堆栈字母表上的正则语言相关联来扩展下推系统。目标是对需要检查程序的运行时调用堆栈的程序验证问题进行建模。例子包括使用堆栈检查的程序的安全属性检查，HTML5解析器规范的兼容性检查等。Esparzaet al.证明了CPDS的可达性问题是EXPTIME-完全的，这阻止了一般情况下存在对所有实例都可处理的算法。在CPDS实际应用的驱动下，我们研究了CPDS的一个重要子类模式CPDS（pCPDS）的可达性，其中每个转换规则都携带一个遵循一定模式的正则表达式.首先，我们提出了新的饱和算法求解状态和配置的可达性pCPDS。在最坏情况下，该算法在原子模式的大小上表现出指数时间复杂度。接下来，我们证明了携带简单模式的pCPDS的可达性在固定参数多项式时间和空间中是可解的。这回答了是否存在易于处理的可达性分析算法的CPDS量身定制的那些实际情况下，承认有效的解决方案，如堆栈检查没有异常处理的问题。我们已经评估了所提出的方法，我们的实验表明，模式驱动的算法稳定的规模上pCPDS与简单的模式。
Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the runtime call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparzaet al.proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new saturation algorithms for solving state and configuration reachability ofpCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability ofpCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales onpCPDSs with simple patterns.
登录
查看更多内容
DOI：
10.1007/978-3-642-16164-3_14
发表时间：
2010-09
期刊：
--
影响因子：
--
作者：
M. Hague;C. Ong
通讯作者：
M. Hague;C. Ong
DOI：
10.4230/lipics.concur.2015.383
发表时间：
2015
期刊：
--
影响因子：
--
作者：
Fu Song;Weikai Miao;G. Pu;Min Zhang-
通讯作者：
Fu Song;Weikai Miao;G. Pu;Min Zhang-
DOI：
10.1007/978-3-540-73368-3_19
发表时间：
2007-07
期刊：
--
影响因子：
--
作者：
Dejvuth Suwimonteerabuth;F. Berger;Stefan Schwoon;J. Esparza
通讯作者：
Dejvuth Suwimonteerabuth;F. Berger;Stefan Schwoon;J. Esparza
DOI：
10.1007/11539452_36
发表时间：
2005-08
期刊：
--
影响因子：
--
作者：
A. Bouajjani;M. Müller-Olm;Tayssir Touili
通讯作者：
A. Bouajjani;M. Müller-Olm;Tayssir Touili
DOI：
10.1016/j.scico.2005.02.009
发表时间：
2003-06
期刊：
--
影响因子：
--
作者：
T. Reps;Stefan Schwoon;S. Jha
通讯作者：
T. Reps;Stefan Schwoon;S. Jha