This is my note for presentation in CS590 Computer-Aided Program Reasoning seminar on 09/27/2016. We are reading ξ12 of book The Calculus of Computation: Decision Procedures with Applications to Verification to elaborate the intuition and formalization of abstract interpretation, and how that can be used for invariant generation. This seems a relatively easy reading, the chapter is well written.
Please do not hesitate to correct me if I am wrong anywhere. 😁