SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Tue 24 Oct 2023 12:00 - 12:30 at Room I - Session 10 Chair(s): Jerome Feret

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 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Session 10SAS 2023 at Room I
Chair(s): Jerome Feret INRIA Paris
11:00
60m
Keynote
Verifying Infinitely Many Programs at OnceKeynote
SAS 2023
I: Loris D'Antoni University of Wisconsin-Madison
Pre-print
12:00
30m
Talk
Mutual Refinements of Context-Free Language Reachability
SAS 2023
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
Pre-print