LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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'​)