[SkiFire13]

To extend on this, while abstract interpretation may sound a bit "abstract" (pun not intended), it is the basis for many techniques for software verification and compiler optimizations. At its core it basically allows you to soundly approximate the set of reachable states in a program, which in turn can be used to check that no "bad" state can be reached (for software verification) or that e.g. some checks are useless and can be removed (for compiler optimizations). Other applications include the new borrow checker for the Rust programming language, which is built on various dataflow passes to determine at each program point which variable is "live" and/or "borrowed".