Entangled abstract domains for higher-order programs

Relational abstract domains are a cornerstone of static analysis for first-order programs. We explore challenges in generalizing rela-tional abstract domains to higher-order program analysis. We find two reasonable, orthogonal and complementary interpretations of relational domains in a higher-order setting. The first technique, locally relational abstract domains, are relational abstract domains that travel with the environments found within closures. These ab-stract domains record invariants discovered within a given scope. The second technique, globally entangled abstract domains, al-lows relational abstract domains to quantify over the concrete con-stituents of an abstract resource. This approach enables the discov-ery of interprocedural, interstructural and intrastructural program invariants. We develop the techniques for a lambda calculus en-riched with structs. We structurally abstract the concrete semantics; we develop a logic for both the local and global generalizations; and then we integrate both logics into the abstraction. By restricting the logics, existing relational abstract domains (or their entangled, higher-order generalizations) are recoverable. To demonstrate the applicability of the framework, higher-order variants of both oc-tagon and polyhedral domains are formulated as such restrictions. 1. Introduction: Relatin