Symbolic Execution is a case of Abstract Interpretation? This is written in the wiki entry of Symbolic Execution, but I can't find any reference for it. Can anyone show me a pointer? Thank you.
I am not aware of a paper concerned with the comparison between symbolic execution and abstract interpretation. Nor do I think one is needed. Reading the original descriptions of these two techniques should be enough.


King, Symbolic Execution and Program Testing, 1976
Cousot, Cousot, Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixpoints, 1977


(Conversely, if there would be some unexpected connection, then that would be worth describing. But I very much doubt this is the case.)

The main idea of symbolic execution is that, at an arbitrary point in execution, you can express the values of all variables as functions of the initial values. The main idea of abstract interpretation is that you can systematically explore all executions of a program by a series of over-approximations. (I can hear several AI enthusiasts groaning at the previous approximation.)

Thus, at least in the original formulation, symbolic execution was not concerned with exploring all possible executions. You can see this even in the title: it includes the word ‘testing’. But here's more from Section 8: "For programs with infinite execution trees, the symbolic testing cannot be exhaustive and no absolute proof of correctness can be established."

In contrast, abstract interpretation aims to explore all executions. To do so, it uses several ingredients, one of which is very similar to the main idea of symbolic execution. These ingredients are (1) abstract states, (2) joining and widening (hence, ‘lattice’ in the title).

Abstract states. The concrete state of a program at a particular point in time is basically a snapshot of the memory content (including the program code itself and the program counter). This has a lot of detail, which is hard to track. When you analyze a particular property, you may want to ignore large parts of the concrete state. Or you may want to care only whether a particular variable is negative, zero, or positive, but not care about its exact value. In general, you want to consider an abstract version of the concrete state. For this to work out, you must have a commutativity property: If you take a concrete state, execute a statement, and then abstract the resulting state, you should obtain the same result as if you abstract the initial state, and then execute the same statement but on the abstract state. This commutativity diagram appears in both papers. This is the common idea. Again, abstract interpretation is more general, for it does not dictate how to abstract a state -- it just says there should be a way to do it. In contrast, symbolic execution says that you use (symbolic) expressions that mention the initial values.

Joining and Widening. If program execution reaches a certain statement in two different ways, symbolic execution does not try to merge the two analyzes. That is why the quote above talks about execution trees, rather than dags. But, remember that abstract interpretation wants to cover all executions. Thus, it asks for a way to merge the analyses of two executions at the point where they have the same program counter. (The join could be very dumb ({a} join {b} = {a,b}) such that it amounts to what symbolic execution does.) In general, joining itself is not sufficient to guarantee that you'll eventually finish analyzing all executions. (In particular, the dumb join mentioned earlier won't work.) Consider a program with a loops: "n=input(); for i in range(n): dostuff()". How many times should you go around the loop and keep joining? No fixed answer works. Thus, something else is needed, and that is widening, which can be seen as a heuristic. Suppose you went around the loop 3 times and you learned that "i=0 or i=1 or i=2". Then you say: hmmm, ... let's widen, and you get "i>=0". Again abstract interpretation does not say how to do widening -- it just says what properties widening should have to work out.

(Sorry for this long answer: I really didn't have time to make it shorter.)