Abstract interpretation is a static program analysis technique that can be used to reason over programs and their behavior. It consists of building an interpreter that works with abstract values:  concrete values are approximated by sets of values (e.g., 5 can be approximated by the interval [0, 10], or by its type: Int). A frequently used approach to perform abstract interpretation is to describe the interpreter as an abstract state machine, and to abstract this machine. This is the AAM (Abstracting Abstract Machines) approach [1].

In an abstract interpreter following the AAM approach, the interpreter explores a graph where each state approximates a possible state of the concrete evaluation. A transition function is defined, allowing the interpreter to transition from one state to its successors. The abstract interpretation therefore consists of exploring the successors of each state, starting from an
initial state containing the program to analyze. This builds up a state graph that over-approximates every possible behavior of the program.

However, abstract interpretation does not scale well to analyze large programs. Because each transition represent a small increment in the evaluation of the program, many states have to be explored, and the state graph computed can be complex and contain many cycles. In order to support larger programs, it is important to improve performance of such abstract interpreters. Some work exists on improving the efficiency of abstract machines [2], but not much research has been done in parallelizing these abstract machines. A notable exception is [3].