To solve complex constraints in numerical analysis, and in program analysis, we can use approximation techniques.

We use partial orders to describe approximation.

In numerical analysis the order is order on real numbers.

In program analysis states often have discrete structures, so our orders are more like subset relations.

We introduce lattices as particular kinds of partial orders and we study convering sequences in lattices.

Basic plan:

• represent semantics as limits of sequences in partial orders
• approximate the semantics of a lattice with a simpler abstract lattice (used to represent space of loop invariants)
• compute limits of sequences in the simpler abstract lattice
• prove that approximation is conservative, a computed invariant is a always a true property (in worst case it is 'true')