Undecidability of static analysis

TLDR

Static analysis is essential for compile‑time program semantics, yet the rise of languages with dynamic storage and recursive data structures has made it a challenging field that relies on simplifying assumptions and approximate solutions. The study examines two core static‑analysis problems: may‑alias and must‑alias. Even under common simplifying assumptions, may‑alias is undecidable and must‑alias is uncomputable, demonstrating that such analyses are harder than previously recognized.

Abstract

Static analysis of programs is indispensable to any software tool, environment, or system that requires compile-time information about the semantics of programs. With the emergence of languages like C and LISP, static analysis of programs with dynamic storage and recursive data structures has become a field of active research. Such analysis is difficult, and the static-analysis community has recognized the need for simplifying assumptions and approximate solutions. However, even under the common simplifying assumptions, such analyses are harder than previously recognized. Two fundamental static-analysis problems are may alias and must alias . The former is not recursive (is undecidable), and the latter is not recursively enumerable (is uncomputable), even when all paths are executable in the program being analyzed for languages with if statements, loops, dynamic storage, and recursive data structures.