[mjn]

> Symbolic execution is also known as abstract interpretation

These aren't the same thing! They do both use abstraction of concrete values, but abstract interpretation solves for fixpoints in a lattice of abstract values, which is a fairly different process from how symbolic execution works. The answers here go into more detail: https://cstheory.stackexchange.com/questions/19708/symbolic-...

One way of digging into abstract interpretation non-theoretically is via this recently open-sourced framework: https://code.fb.com/open-source/sparta/

[rscho]

https://docs.racket-lang.org/tutorial/index.html

For a very non-theoretical forage into that.

BTW the guy you are answering to is a prolog expert.

[TACIXAT]

This is the most digestible intro to abstract interpretation that I've found, https://wiki.mozilla.org/Abstract_Interpretation.

[archi42]

I believe GP wanted to say that Symbolic Execution is a subset of Abstract Interpretation; because here the prolog expert is wrong: SE is not strictly equal to AI (though I'd gladly believe he didn't actually meant to say that).

AI itself boils down to "Build some lattices, construct a Galois Connection between them and add some abstract transfer function on top of it" (and make sure that all the necessary correctness equations hold; this is the difficult part). For SE you then choose the appropriate lattices and construct suitable transfer functions.

BTW: SE usually also needs a fixed-point iteration to produce meaningful results. At least when considering cyclic control flow graphs (loops & recursion).