Sumit Gulwani, Bill McCloskey, and Ashish Tiwari. 2008. Lifting abstract interpreters to quantified logical domains. SIGPLAN Not. 43, 1 (January 2008), 235–246. https://doi.org/10.1145/1328897.1328468
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.