期刊文献+

Reachability of Patterned Conditional Pushdown Systems

原文传递
导出
摘要 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 run-time call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et 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 satura-tion algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying sim-ple 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 on pCPDSs with simple patterns.
出处 《Journal of Computer Science & Technology》 SCIE EI CSCD 2020年第6期1295-1311,共17页 计算机科学技术学报(英文版)
基金 This work was supported by the National Natural Science Foundation of China under Grant Nos.61802126,61672229,61832015 and 62072176 the Ministry of Science and Technology of the People’s Republic of China under Grant No.2018YFC0830400 Shanghai Pujiang Program under Grant No.17PJ1402200.
  • 相关文献

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部