Subcubic certificates for CFL reachability

Add to your list(s) Download to your calendar using vCal

• Dmitry Chistikov, University of Warwick
• Friday 04 November 2022, 14:00-15:00
• SS03.

If you have a question about this talk, please contact Jamie Vicary.

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).

Joint work with Rupak Majumdar and Philipp Schepper.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.