Differences
This shows you the differences between two versions of the page.
sav08:idea_of_partial_orders_and_approximation [2008/04/30 09:09] vkuncak created |
sav08:idea_of_partial_orders_and_approximation [2008/04/30 09:13] (current) vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
In program analysis states often have discrete structures, so our orders are more like subset relations. | 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. | + | 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') | ||