Lifting abstract interpreters to quantified logical domains

TLDR

Quantified abstract domains can encode universally quantified facts such as ∀i(0 ≤ i < n ⇒ α[i] = 0), but existing domains only provide over‑approximations for operations, making guard handling require under‑approximations. The paper proposes a general technique for constructing abstract interpreters over powerful universally quantified abstract domains that build on existing quantifier‑free domains. The authors devise an automatic method that transforms standard over‑approximation operations into sound under‑approximations and prove correctness by defining two lattices—one for soundness and one for precision. Experiments on programs with arrays and pointers, including sorting algorithms, show that the approach is feasible on challenging examples.

Abstract

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤ i < n ⇒ α[i] = 0). The principal challenge in this effort is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation. We present an automatic technique to convert the standard over-approximation operations provided with all domains into sound under-approximations. We establish the correctness of our abstract interpreters by identifying two lattices---one that establishes the soundness of the abstract interpreter and another that defines its precision, or completeness. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.