Hacker News new | ask | show | jobs
by rscho 2633 days ago
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.

2 comments

This is the most digestible intro to abstract interpretation that I've found, https://wiki.mozilla.org/Abstract_Interpretation.
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).