Skip to main content

Deciding kCFA is complete for EXPTIME

David Van Horn, Harry G. Mairson

DOI 10.1145/1411204.1411243 dblp BibTeX

Abstract

We give an exact characterization of the computational complexity of the kCFA hierarchy. For any k> 0, we prove that the con-trol flow decision problem is complete for deterministic exponen-tial time. This theorem validates empirical observations that such control flow analysis is intractable. It also provides more general insight into the complexity of abstract interpretation.

Related papers

On exponential-time completeness of the circularity problem for attribute grammars TOPLAS 2004
Robust Almost-Sure Reachability in Multi-Environment MDPs TACAS 2023
Model checking for symbolic-heap separation logic with inductive predicates POPL 2016
A Logical Approach to Deciding Semantic Subtyping TOPLAS 2015
Relating complexity and precision in control flow analysis ICFP 2007
Types and higher-order recursion schemes for verification of higher-order programs POPL 2009
Parametric polymorphism and semantic subtyping: the logical connection ICFP 2011
Regular expression types for XML ICFP 2000