Graph Reachability Algorithms for Program Analysis
COM1 Level 3
MR1, COM1-03-19
Abstract:
Program analysis automatically reasons about program runtime behavior and provides mechanisms to determine whether a program’s execution will satisfy certain properties. Program analysis offers a rich spectrum of methods for improving software reliability. A variety of program analysis problems can be formulated as graph reachability problems in edge-labeled graphs. Over the years, we have witnessed the tremendous success of various graph-reachability-based program-analysis techniques. In this talk, I will discuss our work in the past three years on CFL-reachability, Dyck-reachability, and InterDyck-reachability.
Bio:
Qirun Zhang is an Assistant Professor in Computer Science at Georgia Tech. His research focuses on programming languages and software engineering, particularly in developing static program analysis frameworks to enhance software reliability. He has received a PLDI 2020 Distinguished Paper Award, an OOPSLA 2022 Distinguished Artifact Award, an NSF CAREER Award, and an Amazon Research Award in Automated Reasoning. He has also served on program committees of FSE, ICSE, ISSTA, OOPSLA, PLDI, and POPL.