what's means the W-arcs I think this is basically saying do a while loop where you keep advancing the state until it stays the same This is like electric current through circuits Env is a map from identifiers to values. 2^Env is a funny notation for a set of environments. (2^X means powerset, the set containing all possible X's). The Knaster-Tarski fixed point theorem is a fundamental result that shows order preserving lattice maps have fixed points. This is reformulating Cv (the possible states at a point) in an "incremental" fashion, defining it as a function of the possible states at previous points. This is describing the abstract syntax tree of the flowchart language So there are different modes of abstract interpretation, once where information flows forward through the program flow graph and ones where it goes backwards. we can use the rule of signs to figure out if a multiplication will be positive or negative without doing the difficult work of actually multiplying numbers.