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.

Qirun Zhang is an assistant professor in the School of Computer Science at Georgia Institute of Technology. His general research interests are in programming languages and software engineering, focusing on developing new static program-analysis frameworks to improve software reliability. He received his Ph.D. in Computer Science from The Chinese University of Hong Kong in 2013. He received a PLDI 2020 Distinguished Paper Award and an Amazon Research Award in Automated Reasoning.