IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2023 > Subcubic certificates for the CFL reachability problem

Dmitry Chistikov

Tuesday, January 31, 2023

11:00am Lecture hall 1 & Zoom3 (pass: @s3)

Dmitry Chistikov, Associate Professor, University of Warwick, United Kingdom

Subcubic certificates for the CFL reachability problem


The context-free language (CFL) reachability problem on graphs (as well as a closely related problem of language emptiness for pushdown automata) is a core problem for interprocedural program analysis and model checking. It can be solved in cubic time but, despite years of efforts, there is no truly sub-cubic algorithm known for it.

We study the related certification task: given a problem instance, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that there exist succinct certificates, of quadratic size, which can be checked in subcubic (matrix multiplication) time.

In this talk, I will introduce CFL reachability and standard algorithms for it and discuss our certification results. I will also discuss the question of whether faster algorithms for CFL reachability could lead to faster algorithms for other combinatorial problems such as SAT (a “fine-grained complexity” question).