Lambda the Ultimate

Lifting Abstract Interpreters to Quantified Logical Domains. Sumit Gulwani, Bill McCloskey, Ashish Tiwari. July 2007.

Today, abstract interpretation is capable of inferring a wide variety of quantifier-free program invariants. In this paper, we describe a general technique for building powerful quantified abstract domains that leverage existing quantifier-free domains. For example, from a domain that abstracts facts like "a[1] = 0", we automatically construct a domain that can represent universally quantified facts like "Forall i: (0 <= i < n) => A[i]=0)". The principal challenge in building such a domain 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...

Using our generic construction, we build a number of abstract interpreters on top of domains for linear arithmetic, uninterpreted function symbols (used to model heap accesses), and pointer reachability. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.