Mutual Refinements of Context-Free Language Reachability
Context-free language (CFL) reachability is an important program analysis framework. Due to the hardness of program analysis, the exact problems can be intractable or even undecidable, and CFL-reachability only approximates such problems. For the same problem, there could be many CFL-reachability formulations based on different CFLs, each of which over-approximates the problem from a different angle. Given multiple such CFLs $C_1,ldots ,C_n$, suppose the reachability result of each $C_i$ produces a set $P_i$ of reachable vertex pairs. We can straightforwardly intersect all reachability results $bigcap_{i=1}^n P_i$ to achieve better precision. But is it possible to achieve even better precision?
This paper gives an affirmative answer from an interesting perspective: although CFLs are not closed under intersections, in CFL-reachability we can ``intersect'' the graphs. Specifically, we propose emph{mutual refinement} to combine different CFL-reachability-based over-approximations. Our key insight is that the standard CFL-reachability algorithm can be slightly modified to trace the edges that contribute to the reachability results of $C_1$, and $C_2$-reachability only need to consider contributing edges of $C_1$, which can, in turn, trace the edges that contribute to $C_2$-reachability results, etc. We prove that there exists a unique optimal refinement result (fix-point). Experimental results show that mutual refinement can achieve better precision than the straightforward combination with reasonable extra cost.
Tue 24 OctDisplayed time zone: Lisbon change
11:00 - 12:30 | |||
11:00 60mKeynote | Verifying Infinitely Many Programs at OnceKeynote SAS 2023 Pre-print | ||
12:00 30mTalk | Mutual Refinements of Context-Free Language Reachability SAS 2023 Pre-print |