Reachability of Patterned Conditional Pushdown Systems
- PDF / 2,309,856 Bytes
- 17 Pages / 595 x 842 pts (A4) Page_size
- 59 Downloads / 231 Views
Reachability of Patterned Conditional Pushdown Systems Xin Li1 , Patrick Gardy1 , Yu-Xin Deng1,∗ , and Hiroyuki Seki2 1 2
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China Graduate School of Informatics, Nagoya University, Nagoya 464-8601, Japan
E-mail: [email protected]; [email protected]; [email protected]; [email protected] Received April 11, 2020; revised October 9, 2020. Abstract 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. Keywords
1
conditional pushdown system, pattern, reachability, saturation algorithm
Introduction
Pushdown systems (PDSs) are widely used as abstract models for sequential programs with recursion. A PDS is formed by a finite set of states, a finite yet unbounded stack, and transition rules. The stack can be used to store the calling contexts of programs, whereby method calls and returns are correctly matched when encoding the programs as PDSs in program analysis and verification. Thanks to efficient saturation-based algorithms for computing the post-images and preimages of (possibly infinite) regular sets of system states [1] , quite a few pushdown model checking tools have been developed, notably Moped [1] , jMoped [2] , SLAM [3] , Weighted PDS [4] , PuMoC [5] , PDSolver [6] , etc., and these tools have been successfully applied to
analyze, test and verify Boolean, Java, C/C++, and Erlang programs. 1.1
Motivation
PDSs have been extended in various ways to model concurrent programs [7, 8] , real-time system behaviors [9, 10] , etc. A line of research extends PDSs with the power of man
Data Loading...
