Re:Symbolic Execution: Intuition and Implementation
by int3 on Friday March 09, 2018 @05:44AM
(#16550963)
Type inference is a special case of abstract interpretation: https://www.irif.fr/~mellies/mpri/mpri-ens/articles/cousot-t...
(Not that I've read that paper in detail, mind you...)
Re:Symbolic Execution: Intuition and Implementation
by UncleMeat on Friday March 09, 2018 @02:12PM
(#16554073)
"Abstract values" and "symbolic values" mean different things. Abstract interpretation and symbolic execution are both powerful static analysis techniques, but they are not (classically) equivalent in function.
"First, as we step through this program, we don’t think about specific values of x like 13. Instead, we think about the set of possible values x might take on. At different points in the program, x might be an element of all integers, negative integers, or positive integers plus 0. In other words, we think of x as a symbolic value (i.e., a set of possible values) rather than a concrete value (i.e., a particular element of that set of possible values)."
vs:
"We expound a view of type checking as evaluation with ‘abstract values’."
http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf