Abstract Interpretation

A method of Formal Verification that involves verifying a system over a given behavioral property via fixed point computations. Can be represented as a Lattice.