Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem . Despite years of efforts, there are no known truly sub-cubical algorithms for this problem . We study the related certification task: given aninstance of CFL reachability, are there small and efficiently checkablecertificates 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 thesize of the problem) and these certificates can be checked in subcubic (matrix multiplication) time . The certificates are based on grammar-based compressionof paths (for positive instances) and on invariants represented as matrixconstraints (for negative instances) Thus, CFL reachabilities lies innondeterministic and co-nondeterished subcUBic time . We also extract a new hardest 2NPDA language, which we also extract from related problems: pushdownreachability and two-way nondeterministic pushdown automata (2NPDA) languagerecognition

Author(s) : Dmitry Chistikov, Rupak Majumdar, Philipp Schepper

Links : PDF - Abstract

Code :

Keywords : cfl - certificates - reachability - subcubic - problem -

Leave a Reply

Your email address will not be published. Required fields are marked *