[POPL'22 Tutorial] Program Analysis via Graph Reachability: Past, Present, and Future

Qirun Zhang and Thomas Reps

Introduction

Many program-analysis problems can be formulated as a formal-language reachability (L-reachability) problem. In the literature, the best-known L-reachability problem is context-free language reachability (CFL-reachability). Specifically, the CFLs can be used to capture well-balanced program properties, such as field accesses (i.e., reads and writes), pointer indirections (i.e., references and dereferences), and context-sensitivity (i.e., function calls and returns). The purpose of this tutorial is to provide an overview of various graph-reachability frameworks, discuss recent algorithmic and complexity developments, and teach participants how to design efficient program analyses based on graph reachability. The first part of the tutorial will provide background on program analysis via graph reachability, focusing on the origin, fundamentals, and practical development of CFL-reachability. The second part of the tutorial will cover recent developments that extend CFL-reachability. We will focus on discussing asymptotically faster algorithms for Dyck-reachability and frameworks that are more expressive than CFL-reachability.

Presentation Files


Last Updated: 2022-02.