Wed 19 Jan 2022 15:55 - 16:20 at Salon I - Algorithmic Verification 1 Chair(s): Qirun Zhang

Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem on graphs and can be solved in cubic time. Despite years of efforts, there are no known truly sub-cubic algorithms for this problem. We study the related \emph{certification} task: given an instance of CFL reachability, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates ($O(n^2)$ in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. The certificates are based on grammar-based compression of paths (for reachability) and on invariants represented as matrix inequalities (for non-reachability). Thus, CFL reachability lies in nondeterministic and co-nondeterministic \emph{subcubic} time.

A natural question is whether faster algorithms for CFL reachability will lead to faster algorithms for combinatorial problems such as Boolean satisfiability (SAT). As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability for a conditional lower bound stronger than $n^\omega$, unless the nondeterministic strong exponential time hypothesis (NSETH) fails. In a nutshell, reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability.

Our results extend to related subcubic equivalent problems: pushdown reachability and 2NPDA recognition; as well as to all-pairs CFL reachability. For example, we describe succinct certificates for pushdown non-reachability (inductive invariants) and observe that they can be checked in matrix multiplication time. We also extract a new hardest 2NPDA language, capturing the hard core'' of all these problems.

#### Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

 15:05 - 16:20 Algorithmic Verification 1POPL at Salon I Chair(s): Qirun Zhang Georgia Institute of Technology 15:0525mResearch paper Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemotePOPLYuanbo Li Georgia Institute of Technology, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI Media Attached 15:3025mResearch paper The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemotePOPLAdam Husted Kjelstrøm Aarhus University, Andreas Pavlogiannis Aarhus University DOI Media Attached 15:5525mResearch paper Subcubic Certificates for CFL ReachabilityRemotePOPLDmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA DOI Media Attached