3 ms·

> Symbolic execution is also known as abstract interpretation These aren't the same thing! They do both use abstraction of concrete values, but abstract interp

by mjn 8y ago

> 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-execution-is-a-case-of-abstract-interpretation 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/ https://code.fb.com/open-source/sparta/

rscho 8y ago
https://docs.racket-lang.org/tutorial/index.html 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 8y ago
  This is the most digestible intro to abstract interpretation that I've found, https://wiki.mozilla.org/Abstract_Interpretation https://wiki.mozilla.org/Abstract_Interpretation.
- archi42 8y ago
  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).

by mjn 8y ago

rscho 8y ago

https://docs.racket-lang.org/tutorial/index.html 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 8y ago
This is the most digestible intro to abstract interpretation that I've found, https://wiki.mozilla.org/Abstract_Interpretation https://wiki.mozilla.org/Abstract_Interpretation.
archi42 8y ago
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).