Journal of Computer Science and Technology ›› 2020, Vol. 35 ›› Issue (6): 1295-1311.doi: 10.1007/s11390-020-0541-z

Special Issue: Software Systems

Previous Articles     Next Articles

Reachability of Patterned Conditional Pushdown Systems

Xin Li1, Patrick Gardy1, Yu-Xin Deng1,*, and Hiroyuki Seki2        

  1. 1 Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;
    2 Graduate School of Informatics, Nagoya University, Nagoya 464-8601, Japan
  • Received:2020-04-11 Revised:2020-10-09 Online:2020-11-20 Published:2020-12-01
  • Contact: Yu-Xin Deng
  • About author:Xin Li is a research associate professor in East China Normal University, Shanghai. She received her Ph.D. degree in information processing from Japan Advanced Institute of Science and Technology, Nomi, in 2007. Her research interests include formal methods and verification, especially about the theory and practice of model checking, and interdisciplinary machine learning research.
  • Supported by:
    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, and Shanghai Pujiang Program under Grant No. 17PJ1402200.

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. Esparza et al. proved that the reachability problem of CPDSs is EXPTIMEcomplete, 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 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 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 on pCPDSs with simple patterns.

Key words: conditional pushdown system; pattern; reachability; saturation algorithm;

[1] Schwoon S. Model-checking pushdown systems[Ph.D. Thesis]. Department of Computer Science, Technische Universität München, 2002.
[2] Suwimonteerabuth D, Berger F, Schwoon S, Esparza J. jMoped:A test environment for Java programs. In Proc. the 33rd International Conference on Computer-Aided Verification, July 2017, pp.164-167.
[3] Ball T, Rajamani S K. The SLAM project:Debugging system software via static analysis. In Proc. the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2002, pp.1-3.
[4] Reps T W, Schwoon S, Jha S, Melski D. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program., 2005, 58(1/2):206-263.
[5] Song F, Touili T. PuMoC:A CTL model-checker for sequential programs. In Proc. the 27th IEEE/ACM International Conference on Automated Software Engineering, September 2012, pp.346-349.
[6] Hague M, Ong C H L. Analysing mu-calculus properties of pushdown systems. In Proc. the 17th International SPIN Workshop on Model Checking Software, September 2010, pp.187-192.
[7] Bouajjani A, Müller-Olm M, Touili T. Regular symbolic analysis of dynamic networks of pushdown systems. In Proc. the 16th International Conference on Concurrency Theory, August 2005, pp.473-487.
[8] Cai X J, Ogawa M. Well-structured pushdown systems. In Proc. the 24th International Conference on Concurrency Theory, August 2013, pp.121-136.
[9] Abdulla P A, Atig M F, Stenman J. Dense-timed pushdown automata. In Proc. the 27th Annual IEEE Symposium on Logic in Computer Science, June 2012, pp.35-44.
[10] Abdulla P A, Atig M F, Stenman J. Computing optimal reachability costs in priced dense-timed pushdown automata. In Proc. the 8th International Conference Language and Automata Theory and Applications, March 2014, pp.62-75.
[11] Esparza J, Kucera A, Schwoon S. Model-checking LTL with regular valuations for pushdown systems. In Proc. the 4th International Symposium on Theoretical Aspects of Computer Software, October 2001, pp.316-339.
[12] Li X, Ogawa M. Conditional weighted pushdown systems and applications. In Proc. the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, January 2010, pp.141-150.
[13] Minamide Y, Mori S. Reachability analysis of the HTML5 parser specification and its application to compatibility testing. In Proc. the 18th International Symposium on Formal Methods, August 2012, pp.293-307.
[14] Johnson J I, Sergey I, Earl C, Might M, van Horn D. Pushdown flow analysis with abstract garbage collection. Journal of Functional Programming, 2014, 24(2/3):218-283.
[15] Nitta N, Takata Y, Seki H. An efficient security verification method for programs with stack inspection. In Proc. the 8th ACM Conference on Computer and Communications Security, November 2001, pp.68-77.
[16] Shivers O G. Control-flow analysis of higher order languages or taming lambda[Ph.D. Thesis]. Carnegie Mellon University, 1991.
[17] Bravenboer M, Smaragdakis Y. Strictly declarative specification of sophisticated points-to analyses. In Proc. the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, October 2009, pp.243-262.
[18] Lhoták O, Hendren L. Context-sensitive points-to analysis:Is it worth it? In Proc. the 15th International Conference on Compiler Construction, March 2006, pp.47-64.
[19] Thanh H V L, Li X. An on-the-fly algorithm for conditional weighted pushdown systems. Journal of Information Processing, 2014, 22(4):1-7.
[20] Uezato Y, Minamide Y. Pushdown systems with stack manipulation. In Proc. the 11th International Symposium on Automated Technology for Verification and Analysis, October 2013, pp.412-426.
[21] Song F, Miao W K, Pu G G, Zhang M. On reachability analysis of pushdown systems with transductions:Application to Boolean programs with call-by-reference. In Proc. the 26th International Conference on Concurrency Theory, September 2015, pp.383-397.
[22] Esparza J, Ganty P. Complexity of pattern-based verification for multithreaded programs. In Proc. the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2011, pp.499-510.
[1] Que-Ping Kong, Zi-Yan Wang, Yuan Huang, Xiang-Ping Chen, Xiao-Cong Zhou, Zi-Bin Zheng, and Gang Huang. Characterizing and Detecting Gas-Inefficient Patterns in Smart Contracts [J]. Journal of Computer Science and Technology, 2022, 37(1): 67-82.
[2] Feng Wang, Guo-Jie Luo, Guang-Yu Sun, Yu-Hao Wang, Di-Min Niu, Hong-Zhong Zheng. Area Efficient Pattern Representation of Binary Neural Networks on RRAM [J]. Journal of Computer Science and Technology, 2021, 36(5): 1155-1166.
[3] Zeynep Banu Ozger, Nurgul Yuzbasioglu Uslu. An Effective Discrete Artificial Bee Colony Based SPARQL Query Path Optimization by Reordering Triples [J]. Journal of Computer Science and Technology, 2021, 36(2): 445-462.
[4] Bin-Bin Liu, Wei Dong, Jia-Xin Liu, Ya-Ting Zhang, Dai-Yan Wang. ProSy: API-Based Synthesis with Probabilistic Model [J]. Journal of Computer Science and Technology, 2020, 35(6): 1234-1257.
[5] Dong Liu, Zhi-Lei Ren, Zhong-Tian Long, Guo-Jun Gao, He Jiang. Mining Design Pattern Use Scenarios and Related Design Pattern Pairs: A Case Study on Online Posts [J]. Journal of Computer Science and Technology, 2020, 35(5): 963-978.
[6] Monidipa Das, Soumya K. Ghosh. Data-Driven Approaches for Spatio-Temporal Analysis: A Survey of the State-of-the-Arts [J]. Journal of Computer Science and Technology, 2020, 35(3): 665-696.
[7] Wen-Yan Chen, Ke-Jiang Ye, Cheng-Zhi Lu, Dong-Dai Zhou, Cheng-Zhong Xu. Interference Analysis of Co-Located Container Workloads: A Perspective from Hardware Performance Counters [J]. Journal of Computer Science and Technology, 2020, 35(2): 412-417.
[8] Jiu-Ru Gao, Wei Chen, Jia-Jie Xu, An Liu, Zhi-Xu Li, Hongzhi Yin, Lei Zhao. An Efficient Framework for Multiple Subgraph Pattern Matching Models [J]. Journal of Computer Science and Technology, 2019, 34(6): 1185-1202.
[9] Zhe Liu, Cheng-Jian Qiu, Yu-Qing Song, Xiao-Hong Liu, Juan Wang, Victor S. Sheng. Texture Feature Extraction from Thyroid MR Imaging Using High-Order Derived Mean CLBP [J]. Journal of Computer Science and Technology, 2019, 34(1): 35-46.
[10] Aakash Ahmad, Claus Pahl, Ahmed B. Altamimi, Abdulrahman Alreshidi. Mining Patterns from Change Logs to Support Reuse-Driven Evolution of Software Architectures [J]. Journal of Computer Science and Technology, 2018, 33(6): 1278-1306.
[11] Xin Xu, Jiaheng Lu, Wei Wang. Hierarchical Clustering of Complex Symbolic Data and Application for Emitter Identification [J]. , 2018, 33(4): 807-822.
[12] Lei Guo, Yu-Fei Wen, Xin-Hua Wang. Exploiting Pre-Trained Network Embeddings for Recommendations in Social Networks [J]. , 2018, 33(4): 682-696.
[13] Guo-Wei Wang, Jin-Dou Zhang, Jing Li. Complete Your Mobility: Linking Trajectories Across Heterogeneous Mobility Data Sources [J]. , 2018, 33(4): 792-806.
[14] Guochen Cai, Kyungmi Lee, Ickjai Lee. Mining Semantic Trajectory Patterns from Geo-Tagged Data [J]. , 2018, 33(4): 849-862.
[15] Shi-Ming Guo, Hong Gao. HUITWU: An Efficient Algorithm for High-Utility Itemset Mining in Transaction Databases [J]. , 2016, 31(4): 776-786.
Full text



[1] Li Wanxue;. Almost Optimal Dynamic 2-3 Trees[J]. , 1986, 1(2): 60 -71 .
[2] C.Y.Chung; H.R.Hwa;. A Chinese Information Processing System[J]. , 1986, 1(2): 15 -24 .
[3] Zhang Cui; Zhao Qinping; Xu Jiafu;. Kernel Language KLND[J]. , 1986, 1(3): 65 -79 .
[4] Huang Xuedong; Cai Lianhong; Fang Ditang; Chi Bianjin; Zhou Li; Jiang Li;. A Computer System for Chinese Character Speech Input[J]. , 1986, 1(4): 75 -83 .
[5] Shi Zhongzhi;. Knowledge-Based Decision Support System[J]. , 1987, 2(1): 22 -29 .
[6] Gong Zhenhe;. On Conceptual Model Specification and Verification[J]. , 1987, 2(1): 35 -50 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Xia Peisu; Fang Xinwo; Wang Yuxiang; Yan Kaiming; Zhang Tingjun; Liu Yulan; Zhao Chunying; Sun Jizhong;. Design of Array Processor Systems[J]. , 1987, 2(3): 163 -173 .
[10] Qiao Xiangzhen;. An Efficient Parallel Algorithm for FFT[J]. , 1987, 2(3): 174 -190 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
  Copyright ©2015 JCST, All Rights Reserved